目次を開く
結論
証明の有無ではなく、どのモデル・実装・前提について何を確かめたかを開発の各段階に結び付ける。
背景
認証・認可基盤では、状態遷移、権限、プロトコルの前提が異なる層に存在する。単一のテスト手法へ集約せず、各層で確認する性質を明示する必要がある。
設計と検証の論点
構成を検討するときは、次の責任と境界を分けて確認します。
- ユニットテストとプロパティベーステストの役割
- Kaniのハーネスと探索境界
- Tamarinのプロトコルモデル
- 実装との対応関係
- 保証範囲の境界
判断理由
テストで具体例の振る舞いを確認し、KaniではRust実装をハーネスと探索条件の下で調べ、Tamarinではプロトコルを抽象化したモデルの性質を調べる。これらは対象も前提も異なるため、同じ「verified」の一語へまとめない。変更時にどの根拠を再確認するかまで対応付ける。
トレードオフ
モデルやハーネスを小さくすると実行と理解は容易になるが、対象外の振る舞いが増える。抽象化、ループ境界、暗号の理想化を明示し、実装変更時に証明や対応表を維持する費用と比較する。
制約
対象コミット、ツール版、実行コマンド、ハーネス、補題、反例、未検証範囲を揃える。無制限の安全性や本番保証へ拡張しない。
関連事例
関連事例の担当範囲や設計判断を参照します。記事で提案する実験・構成を、その事例で実施済みとするものではありません。