SPECA とは
SPECA (Specification-to-Property Agentic Auditing) は、仕様書からセキュリティプロパティを導出し、証明ベース監査によって実装がそれらを満たすかどうかを検証する自動セキュリティ監査フレームワークです。
パイプラインは大きく 2 つに分かれます。Knowledge Structuring (仕様を読み、グラフを抽出し、型付きプロパティを生成する) と、Systematic Auditing (プロパティを実装コードに対応づけ、証明を試み、機械的に誤検出をフィルタする) です。
なぜ仕様書から始めるのか
コードベースのスキャンに特化したセキュリティツールは、既知のバグパターンやデータフローの異常を検出できます。しかし、仕様で規定されたシステム (プロトコル実装・暗号ライブラリ・コンセンサスエンジンなど) では、脆弱性の原因が「コードの書き方」ではなく「仕様が要求すること」にある場合があります。コードを見るだけのツールは、仕様レベルの不変条件を表現する手段を持たないため、そういった欠陥を検出できません。
SPECA は逆方向から考えます。仕様書を読み、形式的なセキュリティプロパティを導出したうえで、実装がそれらを証明できるかを問います。
アプローチの概要
- 仕様書からプロパティを導出 — 仕様書をプログラムグラフに分解し、STRIDE (脅威モデリング手法) と CWE Top 25 を適用して型付きセキュリティプロパティを生成します。
- 証明試行ベースの監査 — 各プロパティが実装で成立するか証明を試みます。証明できない部分 (proof gap) を候補検出として報告します。
- 3 ゲートの誤検出フィルタ — Dead Code・Trust Boundary・Scope Check の 3 段階で誤検出を間引きます。recall-safe (真陽性を落とさない) 設計です。
実績
- Sherlock Ethereum Fusaka — 対象 15 件の H/M/L 脆弱性を全件検出。366 件の投稿にも含まれない新規バグ 4 件を発見 (開発者の修正コミットで確認済み)。
- RepoAudit C/C++ ベンチマーク (ICML 2025) — 精度 88.9% を達成しつつ、既知のグラウンドトゥルースを超える 12 件の新規バグ候補を検出。
主要な数字とチャートは 結果ハイライト を参照してください。
対応言語
仕様書で規定されたシステムであれば言語を問いません。Go / Rust / Nim / TypeScript / C / Solidity などで動作実績があります。
次に進む先
目的別の入り口は次のとおりです。
| やりたいこと | 始めるページ |
|---|---|
| 自分のリポジトリで監査を走らせる | とりあえず動かしてみる → CLI リファレンス |
| SPECA の仕組みを理解する | どのように動くか → パイプライン概要 |
| エージェント / ハーネス設計を読む | エージェント設計の概要 |
| 論文の数値を再現する | 運用ガイド |