NyxFoundation/speca

何を解決するか

SPECAは、既知のバグパターンに依存する従来のコード駆動型セキュリティオーディットツールの限界を克服します。一般的なミスを検索するのではなく、実装が意図された設計に実際に従っているかに焦点を当てることで、人間のオーディットやパターンベースのツールが見逃しがちな、新しい脆弱性（たとえば暗号学的不変性の違反）を発見できます。

動作方法

SPECAはエージェント型パイプラインを用いて「仕様に anchored された」オーディットを実行します。自然言語仕様から明示的で型付きのセキュリティ特性を導出し、その後、実装が構造化された証明試行の論理でこれらの不変性を「証明」することを要求します。このプロセスは以下のフェーズで構成されます：

1. 仕様発見：仕様から要件を抽出する。
2. 部分グラフ抽出：システムの関連する部分を特定する。
3. 特性生成：仕様に基づいてセキュリティ特性の語彙を生成する。
4. コード解決：これらの特性を実際のコードにマッピングする。
5. レビュー：ゲートレビュープロセスを通じて結果を検証する。

対象ユーザー

複雑な実装（スマートコントラクトやC/C++プロジェクトなど）が技術仕様を厳密に遵守しているかどうかを検証する必要があるセキュリティ研究者、バグバンティーハンター、ソフトウェアオーディタ向けに設計されています。

主な特徴

• 高い検出率：Sherlock Ethereum Fusakaオーディットコンテストで既知のすべての脆弱性を回収し、開発者によって確認された新しいバグを発見。
• 高い正確性：RepoAudit C/C++ベンチマークにおいて、Sonnet 4.5で公開された最高精度（88.9%）を達成。
• 解釈可能な結果：誤検出は特定のパイプラインフェーズに追跡可能であり、モデルの幻覚のような不透明な結果ではない。
• 拡張性：BUG_BOUNTY_SCOPE.json および TARGET_INFO.json といった設定ファイルを提供するだけで、コアコードを変更せずに新しいターゲットを導入可能。