メインコンテンツまでスキップ
SPECA

SPECA

Specification-to-Property Agentic Auditing

ドキュメントを読むGitHub で見る
SPECA CLI
$npm install -g speca-cli$speca auth login$speca init$speca run --target 04

仕様駆動監査

自然言語仕様 (EIP、コンセンサス仕様など) から型付きセキュリティプロパティ (Invariant / Precondition / Postcondition / Assumption) を抽出し、仕様レベルでしか表現できない脆弱性を検出します。

Proof-Attempt 推論

STRIDE + CWE Top 25 に基づく脅威モデルで整理した各プロパティに対し、「このプロパティが成立することを証明してみろ」と構造的に問い、仕様と実装のギャップを検出します。

完全な解釈可能性

全監査ステップを JSON で構造化。3-gate review ループ (Dead Code / Trust Boundary / Scope) で偽陽性を根本原因ごとに分解し、監査可能・解釈可能な監査結果を提供します。

実績

研究論文での評価を通じて、コンテストの既知脆弱性を高い割合で回復できることと、加えて未公開バグを独立に発見できることが確認されています。RepoAudit ベンチマークでも精度 88.9% / 再現率 100% を達成し、1 バグあたり $1.69 という費用対効果を実証しました。

  • Sherlock コンテスト: 専門家の補助ありで既知 H/M/L 脆弱性 15 件すべて回復、完全自動だと 8 件 (53%)
  • RepoAudit (C/C++ 15 プロジェクト): 既知 35 件のバグをすべて検出、F1 = 0.94 / 精度 88.9%
  • 独立発見した未公開バグ 4 件 — うち 1 件は 366 名のコンテスト監査者が見落とした暗号アルゴリズムの不変条件違反
  • 1 バグあたり約 $1.69 / H/M/L バグ 1 件あたり約 $30、severity を落とさないフィルタで効率的な常時監視

研究論文

SPECA は 2 本の研究論文に基づいて設計されています。最初の論文は Ethereum Fusaka 監査での実戦ケーススタディ、2 本目は同じ仕組みをマルチ実装分散プロトコル全般へ一般化した発展研究です。

SPECA: 仕様書チェックリスト駆動の監査 — Ethereum クライアントのケーススタディ

Kamba, Sannai · arXiv:2602.07513 · 2026

SPECA の最初の論文。仕様書を「監査チェックリスト」に変換し、Ethereum Fusaka に参加する 11 クライアントへ適用した実戦ケーススタディ。

  • 実装間でチェックリストを使い回し、有効 finding の 76.5% をクロス実装由来に
  • Fusaka コンテストで valid finding 採択率 31.5% (平均 27.6% を上回る)
  • V2 再評価で High-severity 脆弱性 2/3 を検出
  • エージェント主導で submission 1 件あたり手動検証 40 分まで短縮
arXiv で読むPDF

コード推論を超えて — マルチ実装分散プロトコルの仕様アンカー監査

Kamba, Murakami, Sannai · arXiv:2604.26495 · 2026

Fusaka ケーススタディの仕組みを、Ethereum 以外を含むマルチ実装分散プロトコル全般に拡張した発展論文。

  • Sherlock 既知 H/M/L 脆弱性 15/15 を回復 (専門家補助あり)、自動のみだと 8/15
  • 366 名のコンテスト監査者が見落とした暗号アルゴリズムの不変条件違反を含む 4 件の未公開バグを独立発見
  • RepoAudit (C/C++ 15 プロジェクト): F1 = 0.94 / Precision 88.9% / Recall 100%
  • 1 バグあたりのコストは約 $1.69、H/M/L バグ 1 件あたり約 $30
arXiv で読むPDF

はじめる

リポジトリを clone して、Python オーケストレータを直接実行するか、npm 経由で SPECA を起動できます。Go / Rust / Nim / TypeScript / C などマルチ言語対応で、GitHub Actions による完全自動化に対応しています。

Python オーケストレータを直接実行

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

speca-cli を使用 (npm 公開予定)

npx speca-cli init
npx speca-cli run --target 04
npx speca-cli browse