仕様駆動監査の考え方

コード駆動型ツールの限界

従来のセキュリティツールは既知のバグパターンを検出します:

• CWE-89: SQL インジェクション (テンプレート: query = "SELECT * FROM users WHERE id=" + user_input)
• CWE-22: パストラバーサル (テンプレート: open(userpath) without sanitize)
• メモリ破損、レース条件、等

しかし仕様で規定されたシステムでは、脆弱性が仕様レベルの不変式違反として生じます。コードのローカルパターンマッチングでは表現不可能:

• 暗号プロトコル: 「メッセージ認証が成立する」「乱数の独立性」等の数学的不変式
• 状態機械: 「この状態では X 状態への遷移が禁止」という要件
• コンセンサス: 「このブロックの検証は必ず safety invariant を保つ」

仕様駆動アプローチ

SPECA は逆向きに分析します:

1. 仕様から型付きプロパティを導出

   • 不変式 (Invariant): 常に成立すべき条件
   • 前置条件 (Precondition): 関数実行前の要件
   • 後置条件 (Postcondition): 実行後の保証
   • 仮定 (Assumption): 外部システムへの依存

2. 実装に「このプロパティを証明してみろ」と問う

   • Proof gap (証明の隙間) = 脆弱性の候補

3. 回収安全 (recall-safe) な FP フィルタリング

   • 3 ゲート review: Dead Code / Trust Boundary / Scope
   • 検出率を保ちながら FP を系統的に削減

利点

観点	メリット
検出	仕様レベルでのみ定義される脆弱性を発見
溯及可能性	各検出は property → subgraph → spec section に遡及可能
比較分析	N 個の実装を同じ property 語彙で評価可能
FP 診断	FP が 3 つの根拠ある原因 (信頼境界 / コード読み間違い / 仕様誤解) に分解

詳細は 証明試行ベースの監査 を参照。