コードではなく仕様書からバグを見つける AIセキュリティ監査フレームワーク SPECAが日本発 OSSとして公開|セキュリティニュースのセキュリティ対策Lab

投稿日時: 2026年05月08日更新日時: 2026年05月08日

日本のセキュリティ研究組織Nyx Foundationは、AIエージェント型セキュリティ監査フレームワーク「SPECA（Specification-to-Checklist Agentic Auditing Framework）」をMITライセンスでGitHub上に公開しました。

SPECAは従来のコード駆動型のバグ発見ツールとは根本的に異なる「仕様駆動（Specification-driven）」アプローチを採用しており、EIPやコンセンサス仕様書などの自然言語で書かれた仕様書を起点にセキュリティプロパティを抽出・整理し、実装との乖離を検出します。Anthropic社のClaude Code CLI＋MCPサーバー上で動作し、GitHub Actionsによる全フェーズの自動実行にも対応しています。

この記事のサマリー

Nyx Foundationが「仕様書からバグを見つける」AIセキュリティ監査フレームワークSPECAをMITライセンスでOSS公開しました。
仕様駆動（Specification-driven）の独自アプローチにより、コードパターンだけでは拾えない「仕様レベルの脆弱性」を検出できます。
実績：Sherlock Ethereum Fusaka監査コンテストデータで既知の脆弱性15件すべてを検出し、さらに追加バグ4件を独立に発見。RepoAudit C/C++ベンチマークでも最高水準の精度で12件の新規候補バグを報告。
過去の実績対象はIntmax ZK実装・SP1 zkVM実装・Ethereumクライアント実装20件以上・DeFiプロトコル多数。
Claude Code CLI＋MCPサーバーで動作し、Go・Rust・Nim・TypeScript・C等のマルチ言語に対応。GitHub Actionsで全フェーズを自動実行できます。
バグバウンティのスコープ・ルールをBUG_BOUNTY_SCOPE.jsonとして読み込み、実践的な脆弱性だけを抽出する設計。ホワイトハッカーのバグバウンティ活動に直接活用できます。
コマンド一つで即起動可能なPythonオーケストレータ付き。

1 SPECAとは何か—「仕様駆動」というアプローチの革新性
- 1.1 従来のコード駆動型ツールの限界
- 1.2 SPECAの仕様駆動アプローチ
2 3つの主要な価値
3 発見した脆弱性と検証結果
4 アーキテクチャの詳細——開発者・研究者向け
5 なぜ今OSSとして全公開するのか
6 クイックスタート
7 セキュリティ担当者・開発者へのポイント
8 よくある質問（FAQ）
9 参考情報

SPECAとは何か—「仕様駆動」というアプローチの革新性

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

従来のセキュリティ静的解析・バグ発見ツールのほとんどはコードを直接分析します。パターンマッチング・シンボリック実行・ファジングなどの手法は、コード上に存在するバグを見つけることに特化しています。

しかしこのアプローチには構造的な盲点があります。「仕様書にはこう書かれているが、実装がそれを満たしていない」という仕様と実装の乖離は、コードだけを見ていても発見できません。仕様レベルの脆弱性——例えば「EIPにはこの条件を検証すると書かれているが、実装が検証していない」というバグは、コードパターン上は「正常な実装」として処理されてしまうのです。

SPECAの仕様駆動アプローチ

SPECAは以下の3ステップで動作します。

ステップ1：仕様書からセキュリティプロパティを抽出として、EIPやコンセンサス仕様書などの自然言語で書かれた仕様から、明示的な型付きセキュリティプロパティを抽出します。プロパティの型はInvariant（不変条件）・Precondition（事前条件）・Postcondition（事後条件）・Assumption（前提条件）の4種類です。

ステップ2：STRIDE＋CWE Top25に基づく脅威モデルで整理として、抽出したプロパティをSTRIDE（なりすまし・改ざん・否認・情報漏洩・サービス拒否・権限昇格）とCWE Top 25の枠組みで整理・分類します。

ステップ3：proof-attempt reasoning（証明試行）として、各実装に対して「このプロパティが成立することを証明してみろ」と構造的に問いかけます。証明できない場合、そのギャップが仕様と実装の乖離＝脆弱性の候補として特定されます。

3つの主要な価値

価値1：仕様レベルでしか表現できない脆弱性の検出として、コードパターンだけでは拾えない、仕様由来のバグを検出できます。これは特にEIPのような詳細な技術仕様が存在するブロックチェーン・ZK分野で威力を発揮します。

価値2：複数実装間の横断比較として、同じプロパティ辞書で複数の実装を一律に評価できます。Ethereumクライアントのように複数の独立した実装が存在する場合、同一の仕様チェックリストで20件以上の実装を横断的に審査できる点は従来ツールにない強みです。

価値3：偽陽性の原因分析として、根拠を完全にトレースし、偽陽性を根本原因ごとに分解できます。全ステップのログ・出力がJSONで構造化されており、監査可能・解釈可能な設計になっています。

発見した脆弱性と検証結果

Nyx Foundationは以下の対象でSPECAを実際に使用し脆弱性を発見してきました。

過去の監査対象として、Intmax ZK実装・SP1 zkVM実装・Ethereumクライアント実装20件以上・その他多数のDeFiプロトコル・OSSプロジェクトが挙げられます。

ベンチマーク実績として、直近のSherlock Ethereum Fusaka監査コンテストデータを用いた再実験では、既知の脆弱性15件すべてを検出し、さらに追加バグ4件を独立に発見しました。RepoAudit C/C++ベンチマークでも他のバグ発見AIと比較して最高水準の精度を維持しつつ、12件の新規候補バグを報告しています。

アーキテクチャの詳細——開発者・研究者向け

AIエージェントの設計

SPECAのAIエージェント設計の核心はproof-attemptプロンプト設計です。「このプロパティを証明せよ」という問いかけ形式にすることで、AIのハルシネーション（幻覚出力）を徹底的に抑制します。証明できない場合は証明できないとAIが明示する構造になっています。

3-gate audit-reviewループ

偽陽性を削減しながらH/M/L（高・中・低）のリコールを維持するために、Dead Code / Trust Boundary / Scopeの3ゲートからなる自己改善ループを実装しています。一次的に報告された問題を複数の観点で再審査し、実際に問題となる可能性が高いものだけを最終出力に残します。

Pythonオーケストレータ

再利用可能なPythonオーケストレータには並列化・リジューム・予算制御・circuit breakerが完備されており、大規模なコードベースの監査にも対応しています。

バグバウンティ対応設計

BUG_BOUNTY_SCOPE.jsonとTARGET_INFO.jsonを用意するだけで新しいターゲットの監査を開始できます。バグバウンティのスコープやルールをそのままJSONとして読み込み、実践的な脆弱性だけを抽出します。

対応言語・実行環境

対応言語はGo・Rust・Nim・TypeScript・Cのマルチ言語です。Claude Code CLI＋MCPサーバー上で動作し、GitHub Actionsで全フェーズを自動実行できます。

なぜ今OSSとして全公開するのか

Nyx Foundationは公開の理由として以下を挙げています。

エンタープライズのセキュリティ部門でもClaude・OpenAIを活用したセキュリティツールを導入する選択肢が現実的になってきた現在、SPECAをオープンに公開しても「攻撃に悪用されるのを指をくわえて見ているだけではない」状況が整ったという判断です。防御側・ホワイトハッカー側が先に活用できる環境が作れると判断し、「攻撃者より先に、ホワイトハッカーが現実システムのバグを見つけ、報告し、修正につなげられる世界を作りたい」という目標のもと全公開に踏み切っています。

プロンプトロジック・再帰的自己改善ループ・Pythonハーネス・JSONログ構造のすべてがMITライセンスで公開されており、改造・拡張・フォークが自由に行えます。

クイックスタート

リポジトリをcloneして以下のコマンドを実行するだけです。

uv run python3 scripts/run_phase.py --target 04 --workers 4 --max-concurrent 64

新しいターゲットの監査を開始するにはBUG_BOUNTY_SCOPE.jsonとTARGET_INFO.jsonを用意するだけです。

セキュリティ担当者・開発者へのポイント

ホワイトハッカー・バグバウンティハンターへとして、SPECAのバグバウンティ対応設計は即実践投入が可能です。スコープJSONを設定するだけで対象プロジェクトの監査が始まり、報告可能な脆弱性候補を体系的に抽出できます。特にEthereum・ZK・DeFi領域のバグバウンティ活動に直接活用できます。

セキュリティエンジニア・監査担当者へとして、STRIDE＋CWE Top25への対応・全ステップのJSONログ・偽陽性の根本原因分析という設計は、既存の監査プロセスへの組み込みを意識したものです。GitHub Actionsとの統合でCI/CDパイプラインへのセキュリティ監査の組み込みも可能です。

研究者・ツール開発者へとして、proof-attemptプロンプト設計・3-gate audit-reviewループという核心的な実装がすべて公開されているため、より高度なバグ発見システムの研究・開発の土台として活用できます。

よくある質問（FAQ）

Q. Claude Code CLIがなければ動かせませんか？ READMEによれば、Claude Code CLI＋MCPサーバーで動作する設計ですが、PromptとPythonオーケストレータ部分は他のLLM APIと組み合わせた拡張も可能です。フォーク・改造はMITライセンスで自由に行えます。

Q. ブロックチェーン・ZK以外の分野にも使えますか？ はい。RepoAudit C/C++ベンチマークでの実績が示すように、一般的なC/C++コードベースにも対応しています。対応言語はGo・Rust・Nim・TypeScript・Cであり、BUG_BOUNTY_SCOPE.jsonで監査対象とルールを定義することで様々なプロジェクトに対応できます。

Q. 仕様書がないプロジェクトには使えませんか？ SPECAは「仕様書がある高信頼性ソフトウェア」を主な対象としています。EIPやコンセンサス仕様書のような詳細な自然言語仕様が存在するプロジェクトで最大の効果を発揮します。仕様書のないプロジェクトへの適用は拡張・改造が必要になります。

Q. 商用利用できますか？ MITライセンスのため、商用利用・改造・再配布が自由に行えます。