mcpField
X
x-ray

x-ray

github.com/pashovセキュリティ1.3k326 回インストール1 週間前に更新
リポジトリ

x-ray について

x-rayは、Solidityプロジェクトを分析し、`x-ray/`フォルダーにセキュリティレポートを作成するスキルです。ソースコード、エントリーポイント、Git履歴、脅威を確認します。

主な機能

  1. 013段階の順次監査ワークフロー
  2. 02Solidityソースと入口の分析
  3. 03Gitのセキュリティ・変更分析
  4. 04カバレッジと仕様書の確認
  5. 05構造化されたレポートの出力

活用シーン

  1. 01Solidityコードベースのリスク確認
  2. 02アクセス制御とコントラクト入口の追跡
  3. 03リポジトリ履歴と依存関係の変更評価

インストール

コマンドをコピーしてターミナルで実行します。

$npx skills add https://github.com/pashov/skills --skill x-ray

インストール後、Claude Code で/x-rayを入力して読み込まれたか確認します。

同梱ファイル

SKILL.md と一緒にインストールされる参考資料やスクリプト。

README.md
VERSION
references/
templates.md
threats.md
scripts/
analyze_git_security.py
entry_points.py
enumerate.sh
generate_svg.py

詳細

X-Ray

プロジェクトのルートに、すべての出力ファイルを含む x-ray/ フォルダーを生成します。パイプラインは 3 ステップで、必ず順番に実行します。

$SKILL_DIR = この SKILL.md ファイルが含まれるディレクトリです。このスキルを読み込んだパスから解決してください(例:このファイルの場所が /path/to/x-ray/SKILL.md の場合、$SKILL_DIR = /path/to/x-ray です)。

進捗の追跡(必須)

何かを始める前に、次の 3 つの ToDo をすべて pending にして TodoWrite を呼び出してください。

  1. Phase 1: Enumerate & measure codebase
  2. Phase 2: Read sources, classify entry points, synthesize invariants
  3. Phase 3: Write x-ray report files

状態遷移(TodoWrite で更新してください。まとめて更新してはいけません):

  • enumerate.sh を実行する前に、直ちに Phase 1 を in_progress にします。
  • Step 1 の並列バッチが返されたら、1 回の TodoWrite 呼び出しで Phase 1 を completed、Phase 2 を in_progress にします。
  • Step 2(2b~2g を含む)が完了したら、1 回の TodoWrite 呼び出しで Phase 2 を completed、Phase 3 を in_progress にします。
  • Step 3 の出力ファイルをすべて書き込んだ後、Phase 3 を completed にします。

ルール:常に in_progress の ToDo は 1 つだけにします。状態更新は、各フェーズの開始時または終了時に直ちに行います。

ステップ 1:列挙と測定

ユーザーがパスを指定した場合は、それをプロジェクトルートとして使用します。指定がない場合は、cwd を使用します。ルートに .sol ファイル、または foundry.toml/hardhat.config.* がない場合は、1 階層下を確認します。

ソースディレクトリの検出:foundry.toml(src = "...")または hardhat.config.* から自動検出します。設定ファイルがない場合は、src/ と contracts/ の両方を試します。foundry.toml がある場合は、最初に読み込みます。

列挙を実行(単一の Bash 呼び出し。出力ディレクトリの作成を含みます):

mkdir -p [project-root]/x-ray && bash $SKILL_DIR/scripts/enumerate.sh [project-root] [src-dir]

その直後に、以下をすべて単一のメッセージで並列に開始します。

0. バージョン確認(フォアグラウンド):

  • $SKILL_DIR/VERSION のローカル VERSION ファイルを読み込みます
  • Bash curl -sf https://raw.githubusercontent.com/pashov/skills/main/x-ray/VERSION
  • リモートの VERSION の取得に成功し、ローカルと異なる場合は、⚠️ You are not using the latest version. Please upgrade for best security coverage. See https://github.com/pashov/skills を出力します。失敗した場合は、何もせずにスキップします。

1. カバレッジ(run_in_background: true):

Foundry の場合:

cd [project-root] && forge coverage 2>&1 || (echo "RETRYING_WITH_IR_MINIMUM" && forge coverage --ir-minimum 2>&1)

Hardhat の場合:

cd [project-root] && npx hardhat coverage 2>&1

ツールチェーンがインストールされていない場合(例:forge: command not found、npx: command not found、node_modules/ がない場合)、カバレッジコマンドは失敗します。これは想定内です。テストの存在は、上記のステップでの列挙ですでに確認されています。カバレッジの失敗は、テストが存在しないことを意味しません。

2. Git セキュリティ分析と JSON の読み込み(フォアグラウンド、単一の Bash 呼び出し):

cd [project-root] && python3 $SKILL_DIR/scripts/analyze_git_security.py --repo . --src-dir [src-dir] --json x-ray/git-security-analysis.json 2>&1 && cat x-ray/git-security-analysis.json

JSON には 7 つのセクションがあります:repo_shape、fix_candidates、dangerous_area_changes、late_changes、forked_deps、tech_debt、dev_patterns。

3. 参照ファイルを事前読み込み(並列の Read 呼び出し 2 回。ステップ 2d/3a の前に、これらをコンテキストに含めてください):

  • $SKILL_DIR/references/threats.md — 脅威プロファイル、時間的脅威、コンポーザビリティに関する脅威
  • $SKILL_DIR/references/templates.md — 出力テンプレート、エントリーポイントのテンプレート、アーキテクチャガイド

4. 仕様書/ホワイトペーパーの検出(node_modules/、lib/、x-ray/、test/ を除外して、1 回の Glob で **/{whitepaper,spec,design,protocol,architecture,overview,README}*.{pdf,md} を検索)。ユーザー向けドキュメント(チュートリアル、API リファレンス、変更履歴、コントリビューションガイド)はスキップします。その後、サイズに応じて処理します。

  • パス A(ドキュメントが 5 件以下で、それぞれ 300 行以下):ステップ 2 の並列メッセージに Read 呼び出しとして含めます。直接読み込みます。サブエージェントは不要です。
  • パス B(ドキュメントが 5 件超、またはいずれかのドキュメントが 300 行超):単一のサブエージェント(model: "sonnet")を起動し、すべてのドキュメントを読み込ませて、構造化された抽出結果(最大 200 行)を返させます。サブエージェントへのプロンプト:
    Read each doc file listed below. Extract ONLY security-relevant information into this format:
    Files: [list of doc file paths]
    
    Return this exact structure:
    ### Doc-Stated Global Invariants
    [Bullet list of every invariant, constraint, or guarantee the docs claim must hold globally across calls. Treated like NatSpec-stated invariants by Step 2g — routed directly to §2 / §3 / §4 of invariants.md by shape, NOT into §1 (Enforced Guards, which is per-call preconditions only).]
    ### Actor Definitions
    [Each actor/role with stated permissions and trust level]
    ### Trust Assumptions
    [What the protocol assumes about external systems, oracles, admins, users]
    ### Cross-System Flows
    [How value/data moves between contracts or external systems]
    ### Economic Properties
    [Fee structures, reward mechanisms, tokenomics, bounded parameters]
    ### Key Design Decisions
    [Explicit "we chose X over Y because Z" statements]
    
    Rules: Quote the source doc for each claim. Omit sections with no relevant content. Max 200 lines total.
    
    このサブエージェントをステップ 1 の並列メッセージに含めます。その出力はステップ 3 のレポート作成に使用します。

どちらのパスでも、抽出するのは次の項目に限ります:ドキュメントに記載された全体的な不変条件、アクターの定義、システム間のフロー、信頼に関する前提、経済的特性、主要な設計上の決定事項。仕様書に由来する主張には、コードで検証された内容と仕様書に記載された内容を監査担当者が区別できるよう、レポート内で (per spec) を付けます。ドキュメントに記載された全体的な不変条件は、ステップ 2g の NatSpec ルーティング処理に使用します。形状に応じて invariants.md の §2/§3/§4 に振り分け、§1(強制適用されるガード)には振り分けません。

すべての呼び出し(カバレッジ、Git 分析、参照ファイルの読み込み、仕様書の Glob)は、同じメッセージに含める必要があります。forge のカバレッジを待たずにステップ 2 に進みます。

ステップ 2:ソースファイルの読み込みとエントリーポイントのスキャン(単一メッセージですべてのツール呼び出しを並列実行)

重要:Bash、Agent、Read、Grep のすべてのツール呼び出しを、1 つのメッセージ内で実行する必要があります。これには、ソースファイルの読み込み、エントリーポイントのスキャン、ステップ 1 で検出された仕様書の読み込みが含まれます。これらはすべて独立しているため、並列に実行します。

対象範囲のフィルタリング
  • インターフェースをスキップします:interfaces/ ディレクトリ、または I + 大文字で始まるファイル名
  • ベンダー提供のライブラリをスキップします:Uniswap FullMath/TickMath、OZ のコピー
  • 判断に迷う場合は含めますが、スコープ表からは除外します
パス A:ソースファイルが20個以下(直接読み込み)

ファイルごとに1回、Read を呼び出します。README、docs、foundry.toml は読み込まないでください(Step 1 ですでに読み込み済みです)。

ファイルごとに抽出する項目: コントラクトの種類と継承関係、ロールとアクセス制御、値を保持する状態変数、外部呼び出し、資金フロー、不変条件に関するコメント、assert/require、後方互換性を示す要素(下記参照)、差分書き込み(関数ごとに、ストレージ変数と適用される記号上の差分を記録します。例:Δ(totalSupply) = +shares, Δ(balanceOf[msg.sender]) = +shares。同一の基本ブロック内に限り、関数をまたいだ推論は行いません。OZ _mint/_burn などの継承されたヘルパーは、balanceOf/_totalSupply への影響が意味的に明白な場合に限り、その効果を解決してかまいません)、ガード述語(ストレージ変数を参照する require/assert/if-revert をすべて、行番号とともに原文どおり引用します。関数パラメーターのみを参照するガードは除外します)、enum/一度限りの状態遷移(すべての require(state == X); ...; state = Y の組み合わせを X@Lx → Y@Ly の形式で記録します。require(addr == address(0)); addr = concrete のような一度限りのラッチも含めます)。

パス B:ソースファイルが20個超(並列サブエージェント)

Tier 1 — 小さいファイル(120行以下): 1回の Bash cat 呼び出しにまとめます。

Tier 2 — 大きいファイル(120行超): サブシステムごとにグループ化します。サブシステムごとにサブエージェントを1つ起動します(model: "sonnet"、最大5つ、各サブエージェントあたり約10ファイルまで)。サブエージェントへのプロンプト:

Read each file listed below and return a structured summary. Do NOT analyze — just extract facts.
Files: [list of file paths]
For EACH file, return this exact format:
### [filename]
- **Type**: contract | library | abstract
- **Inherits**: [parent contracts]
- **Imports**: [imported libraries/contracts]
- **Roles/Access**: [onlyOwner, role constants, modifiers]
- **State vars (value-holding)**: [mappings/vars that hold balances, collateral, etc.]
- **External calls**: [calls to other contracts, ERC20 transfers, etc.]
- **Fund flows**: [deposit/withdraw/mint/burn/transfer paths]
- **Invariants**: [require/assert statements, NatSpec invariant comments]
- **Delta writes**: For EACH non-view non-pure function, list storage variables that change and the symbolic delta applied. Use format `Δ(var) = +expr` or `Δ(var) = -expr`. Only report pairs where BOTH writes appear in the same function body with no intervening call to an unknown external contract. Do NOT chase writes through inherited/imported functions unless the semantic effect is unambiguous (OZ `_mint` → `balanceOf` + `_totalSupply` is fine; custom internal helpers are NOT — list those deltas only in the internal helper's own entry). Example:
  - `deposit()`: `Δ(totalSupply) = +shares`, `Δ(balanceOf[msg.sender]) = +shares`
  - `borrow()`: `Δ(totalBorrows) = +amount`, `Δ(underlyingBalance) = -amount`
- **Guard predicates**: Every `require`/`assert`/`if-revert` in the file that references a storage variable. Quote verbatim with line number. Skip guards that reference only function parameters.
  - `Vault.sol:206`: `require(_fee <= 10, "fee is capped at 0.1%")`
- **Enum/one-shot transitions**: Every pattern of `require(var == X); ...; var = Y` where `var` is a storage enum, uint, or address. Record as `X@Lx → Y@Ly`. Include one-shot latches like `require(addr == address(0)); addr = concrete`.
- **Key logic**: [1-2 sentences on what the contract does]
- **Function-level access map** (REQUIRED for contracts, skip for libraries):
  List every public/external non-view non-pure function with its access control:
  - `functionName()` — [modifier name, e.g. `onlyRole(OCT_KEEPER)`] or [NONE — permissionless]
  For functions with NO modifier, also list which external calls they make:
  - `functionName()` — NONE — calls `ContractName.method()`
エントリーポイントのスキャン(ソース読み込みと同じ並列メッセージに含める)

以下の Bash 呼び出しを、上記のソースファイル読み込みと同じメッセージで起動してください。これは独立しているため、並行して実行できます。

python3 $SKILL_DIR/scripts/entry_points.py [src-dir]

このスクリプトは、コメントと文字列リテラルを空白化した後、function(または receive / fallback)から開始波括弧 { まで、各関数ヘッダー全体を読み取ります。行単位の grep で代用しないでください。フォーマッターはヘッダーを複数行に分割することがよくあります(forge fmt のデフォルト multiline_func_header = "attributes_first" では external が独立した行に置かれます。また、パラメーターを1行に1つずつ記述したヘッダーでは、) external より数行上に function name( が置かれます)。行指向のパターンでは、こうした関数が気付かれないまま除外されます。このスクリプトに必要なのは python3 のみで、Step 1 の git 分析でも使用します。スクリプトを実行できない場合は、対象となるすべてのファイルの関数ヘッダーを自分で読み(サブエージェントの要約ではなく)、一覧を作成してください。

出力は、エントリーポイントごとに1行の path:line: [abstract|library] Container.name(params) attributes 形式で、その後に # N entry point(s) in M of K .sol file(s) の要約が続きます。K が0の場合は、続行する前に [src-dir] を確認してください。読み取り不能なファイルやディレクトリは stderr に報告され、要約の件数に含まれます。このスクリプトは、receive、fallback、初期化関数を含む、view/pure ではないすべての external または public 関数を列挙します。インターフェース、関数本体のない宣言、internal/private 関数、フリー関数、およびパスに /interfaces/ または /mock/ を含むファイルは除外します。マーカー:

  • [abstract] — 抽象コントラクト内で定義されています。そのコントラクトを継承するすべての具象コントラクトに割り当てます。ただし、階層内の下位コントラクトがオーバーライドしている場合は、オーバーライド側の修飾子を適用します。
  • [library] — ライブラリー関数であり、エントリーポイントではありません。非 view のライブラリー関数を直接呼び出すと revert するため、それを呼び出すコントラクト経由でのみ到達できます。下流呼び出しとして扱ってください。
  • // ordinary function named receive(または fallback)— その名前が receive(または fallback)であるだけの通常の関数です。プレーンな ETH の転送を受け取ったり、不明な呼び出しを処理したりするものではありません。

すべてのツール呼び出し(ソース読み込み/Bash/サブエージェント、エントリーポイントのスキャン)は、1つのメッセージ内で行う必要があります。

テストファイルやドキュメントファイルは読み込まないでください。

ステップ 2b:エントリーポイントの分類

ステップ 2 の並列メッセージですでに返されたエントリーポイントのスキャン結果を使い、すべてのエントリーポイントを分類します。サブエージェントの要約だけに頼らないでください。サブエージェントはコントラクトレベルで事実を抽出するため、どの関数がどの外部呼び出しを行うのか、またはどの関数にどのモディファイアがあるのかを誤って割り当てることがあります。

エントリーポイントから除外するもの:view/pure 関数、インターフェースのみの宣言、ライブラリの内部関数(これらは下流の呼び出しであり、エントリーポイントではありません)、モックコントラクト。

各結果を次の 3 つのカテゴリのいずれかに分類します。

  1. 権限不要 — アクセス制御モディファイアがなく、関数本体にも内部呼び出し元の制限がありません。権限不要と分類する前に、必ず関数本体を確認してください。パス A(≤20 ファイル)では、ステップ 2 の読み込みですでに本体がコンテキストに含まれているため、追加の Read 呼び出しを行わずに直接分類します。パス Bでは、候補となる本体の読み込みをすべて、1 つの並列メッセージにまとめます。呼び出し元を制限する次のパターンをすべて確認してください。
    • require(msg.sender == X) または if (msg.sender != X) revert ...
    • if (msg.sender != X || ...) revert ...(複合条件)
    • msg.sender をチェックする内部関数の呼び出し モディファイアがなくても、内部に msg.sender チェックがある関数は権限不要ではなく、ロール制限付きです。よくある例として acceptOwnership()、acceptMsig()、confirmX() があります。これらはモディファイアがないことが多いものの、if (msg.sender != pendingX) revert によって、特定の保留中アドレスからの呼び出しに制限されています。
  2. ロール制限付き — ロールモディファイア(onlyRole(X)、onlyOwner、onlyRouter など)があるか、内部に msg.sender の制限があります(require、if/revert、または委譲されたチェックによるもの)。必要なロールまたはアドレスを記録します。
  3. 管理者限定 — DEFAULT_ADMIN_ROLE、プロトコル管理者を指す onlyOwner、または同等の最上位権限によって制限されています。

注:nonReentrant だけではアクセス制御になりません。initializer/reinitializer はデプロイ時に一度だけ実行される関数です。別途記録してください。

各エントリーポイントについて、次の項目を記録します。

  • コントラクト名と関数名
  • アクセスレベル(権限不要/ロール名/管理者)
  • 呼び出し元(User、Keeper、Admin、LP など)
  • パラメーターと信頼レベル:(user-controlled)、(user-signed)、(keeper-provided)、(protocol-derived)
  • 呼び出しチェーン:サブエージェントの要約と関数レベルのアクセスマップを使って下流の呼び出しを追跡します。形式:→ Contract.fn() → Contract.fn()
  • 変更される状態:変更されるストレージ変数/マッピング
  • 値のフロー:in(トークンを預け入れる)、out(トークンを引き出す)、none
  • 再入防止ガード:あり/なし

このデータは、次の 2 つの出力に使われます。

  • x-ray.md(セクション 2)の権限不要なエントリーポイント一覧 — 権限不要なものだけを使用
  • 完全版の entry-points.md ファイル(ステップ 3c)— すべてのカテゴリを使用
ステップ 2b-flow:プロトコルフローパスの構築

ステップ 2b ですでに収集したエントリーポイントのデータを使い、entry-points.md のフローパスを構築します。これは別の分析工程ではなく、すでにあるデータを整理し直すものです。

主要なユーザー向けエントリーポイント(値を移動させる権限不要およびロール制限付きの関数)ごとに、次の手順を行います。

  1. require 文と状態変数のチェックを特定します。
  2. 各チェックについて、その状態変数を書き込む関数を特定します(他のエントリーポイントの「変更される状態」フィールドですでに把握しています)。
  3. これらを逆方向に連結します:宛先 ← その前提条件を書き込む関数 ← その前提条件を書き込む関数 ← … ← デプロイ
  4. 時間の経過、市場の状況、外部状態など、関数以外の前提条件には ◄── 注記を付けます。

出力:アクターのフローごとにまとめた、シンプルな矢印チェーン。繰り返しを避け、以前のフローを参照します。全体で 15〜30 行です。正確な形式については、entry-points.md テンプレートの Protocol Flow Paths セクションを参照してください。

エントリーポイントのスキャンは必須のゲートです。レポートの権限不要なエントリーポイントのセクションには、サブエージェントの要約ではなく、このスキャンで確認した一覧を記載しなければなりません。食い違いがある場合は、スキャンとコード読み取りの結果を優先します。

ステップ 2c:後方互換性コードの検出

ソースファイルを読む際は、残りのコードベースが壊れないように残されている、削除済みの仕組みの名残と思われるコードに注意してください。よくある兆候:空またはごく簡単な関数本体、実質的に読み書きされていない状態変数、「deprecated」/「legacy」/「backwards compat」/「no longer used」を含むコメント、インターフェースを実装しているものの常にデフォルト値を返す関数、プロキシのストレージレイアウトとの互換性のためだけに保持されているストレージ変数。

すべてのソースファイルを読み終えたら、候補を以下の必須確認項目と照合してから、後方互換性コードと分類してください。候補すべての呼び出し元確認に使う Grep 呼び出しは、1 回の並列メッセージにまとめてください。1 件ずつ確認してはいけません。

  1. 呼び出し元の確認(必須):Grep を使って、その関数/変数に現在のコードベース内でアクティブな呼び出し元がないことを確認します。アクティブなコードパスから呼び出されている場合、デフォルト値やゼロを返すかどうかにかかわらず、後方互換性コードではなく、現在の設計の一部です。
  2. NatSpec/コメントの確認(必須):コードに、そのような動作をする理由(例:「X モード向けに簡略化」、「設計上のもの」、「意図的にゼロ」)を説明する NatSpec またはインラインコメントがある場合、それは文書化された意図的な設計であり、後方互換性コードではありません。ヒューリスティックなパターン照合で、明示された開発者のドキュメントを覆してはいけません。
  3. インターフェース上の義務の確認:デフォルト値を返す関数がインターフェースの要件を満たすために存在し、かつアクティブに呼び出されている場合、それは名残ではなく、現在のアーキテクチャの一部です。

次のすべてを満たす場合にのみ、そのコードを後方互換性コードに分類してください:(a)アクティブな呼び出し元がない、(b)NatSpec/コメントに動作が意図的であるとの記載がない、(c)Git の履歴から、そのコードが属していた仕組みが削除されたことが確認できる。

レポートでは、後方互換性コードをアクティブな機能として説明しないでください。代わりに、監査担当者がコードベースのどの部分が稼働中の機能ではなく互換性のために保持されているのか把握できるよう、セクション 1(出力テンプレートを参照)に明記してください。上記の確認を経ても後方互換性コードが残っていない場合、この小節は省略してください。

ステップ 2d:権限の集中化と一時停止の適用範囲の分析

ソースファイルを読み、エントリーポイントを分類した後、Actors テーブル、Trust Boundaries、Key Attack Surfaces(セクション 2)に反映する分析を 2 つ実施します。これらは独立したセクションではなく、結果を既存のレポートセクションに統合します。

権限の集中化の分析 — 特権ロール(admin、owner、operator、keeper、service など)ごとに、次の手順を実施します。

  1. そのロールが実行できるすべての運用アクションを列挙します(関数レベルのアクセスマップに基づく)。
  2. 各アクションについて、タイムロック、マルチシグ、または遅延があるかを記録します。ロールの移譲にかかる遅延(例:AccessControlDefaultAdminRules の 1 日の遅延)と、運用上のアクションにかかる遅延を区別してください。これらは同じではありません。ロールの移譲に遅延があっても、侵害された保有者が即時実行可能な運用関数を使用することは防げません。
  3. ユーザー資金を引き出したり、移転先を変更したりできるアクションを特定します(例:emergencyWithdraw、setTreasury、transferFee)。

以下に統合します。Actors テーブル(Capabilities 列には、即時実行かタイムロック付きかを具体的に記載)、Trust Boundaries(各境界が実際に何を保護し、何がそれを迂回できるかを説明)、Key Attack Surfaces(「Admin operational powers」または「[Role] compromise」として記述します。攻撃対象領域は個々の関数ではなく、ロールの侵害です)。

一時停止の適用範囲の分析 — 状態を変更する重要な関数ごとに、次の手順を実施します。

  1. whenNotPaused(または同等の仕組み)が適用されているかを確認します。
  2. 一時停止可能な関数と、一時停止できない関数を記録します。
  3. 論理上、一時停止可能であるべき関数(例:ユーザー資金を扱う、権限が制限されたロールが呼び出せる関数)に一時停止が適用されていない場合は、そのロールに関連する攻撃対象領域にこの所見を統合します。一時停止の欠如自体は攻撃対象領域ではありません。該当ロールが侵害された場合のシナリオを悪化させる要素です。

アンチパターン:「Centralization Risks」という独立したサブセクションを作成しないでください。 権限の集中化に関する詳細は、Actors、Trust Boundaries、Key Attack Surfaces、Protocol-Type Concerns に分散して記載します。専用セクションを設けると、これらのセクションにすでに含まれる情報と重複します。一時停止の適用範囲についても同様に、該当ロールの攻撃対象領域の説明に統合してください。

ステップ 2e:プロトコルの分類

ソースを読み込んだ後、references/threats.md の手順(タイプの検出とハイブリッド分類、フェーズの検出、外部呼び出しの分類をすべて 1 つのファイルで実施)に従って、プロトコルを分類します。

ステップ 2f:nSLOC

レポートのヘッダーとスコープテーブルには、ステップ 1 の enumerate 出力に記載された nSLOC TOTAL の正確な値を使用します(~ の接頭辞は付けません)。

ステップ 2g:不変条件の統合

ステップ 2 で抽出した差分書き込み、ガード述語、enum/一度限りの遷移、不変条件に関するコメントを使用して(Path A で直接読み取った場合、または Path B でサブエージェントの出力を使用した場合)、以下の分類体系を体系的に確認し、不変条件の候補を作成します。これは推論の工程です。新たなツール呼び出しは不要です(ただし、ステップ 2 Pass B の Grep 一括実行は除きます。以下を参照)。

用語:ガードとは、単一の呼び出し箇所で強制される、呼び出しごとの事前条件です(例:require(amount >= MIN))。これは反証可能な不変条件ではありません。コードがその呼び出し箇所での条件を保証するためです。不変条件とは、どのような一連の呼び出しを経ても全体として成立しなければならない性質です(例:「有効な各ポジションは ≥ MIN」)。ガードは invariants.md の§1(強制されるガードの参照先)のみに記載します。ガードから導出される不変条件(以下のステップ 2 を参照)や NatSpec に記載された不変条件は、§2/§3/§4 に記載します。 NatSpec の振り分け(構造走査の前に実行):NatSpec の各 @invariant タグ、またはグローバルプロパティを表明するインラインコメント(例:「totalSupply は常に Σ balances に等しい」、「fee は MAX_BP を超えない」、「同時にアクティブなエポックは 1 つだけ」)について、カテゴリの形状(Conservation/Bound/Ratio/StateMachine/Temporal)に基づき、§2(または複数のコントラクトにまたがるプロパティや複数のプリミティブから導かれる場合は §3/§4)に直接振り分けます。ソースタグ:NatSpec: Contract.sol:LN。開発者が記述したグローバル不変条件を §1 に配置してはいけません。§1 に記載するのは、呼び出しごとのガード述語のみです。振り分け後も、以下の構造スキャンを実行します。スキャンによって NatSpec の主張が確認される(On-chain=Yes)場合も、矛盾が見つかる(On-chain=No)場合もあります。

走査順序(各ステップでは、前のステップの結論ではなく、生の抽出データを使用します):

  1. 保存スキャン:各関数について、同じ関数本体内で Δ(A) = +expr と Δ(B) = -expr(またはマッピングの対応関係にある値について Δ(B) = +expr)となる差分書き込みのペアを探します。一致したペアはそれぞれ、保存候補 A + B = const または A == Σ B[key] になります。

    • マッピングへの書き込み(mapping[key] += e と scalar += e のペア)では、scalar == Σ mapping[key] を推定します。いずれかの変数に書き込むすべての関数でこのパターンが成り立つかを確認します。片方にだけ書き込む関数が 1 つでもある場合は、その欠落を「部分的な保存」として記録し、Yes/No の行に分けます。
    • 転送パターン(mapping[from] -= e、mapping[to] += e でスカラーに変化がない場合)では、マッピングの合計が自己保存されることを確認します。
    • 保存の否定(重要):フローを追跡するはずの関数(例:フラッシュローンの引き出し/返却、受け取り/転送)でストレージの Δ が 0 の場合、保存に関する否定的な所見として記録します。Δ がないこと自体が不変条件に関する所見です。
  2. ガードの抽出と昇格(各 require/assert/if-revert について、次の 2 パスを実行します):

    パス A — そのまま抽出(Enforced Guards の参照用):すべての require/assert/if-revert を、invariants.md の §1 に G-N の行として記載します。ソース位置とともに、述語をそのまま引用します。これは呼び出しごとの事前条件を機械的に出力するものであり、反証もファジングも行いません。関数パラメーターだけを参照し、ストレージとの紐付けがなく、グローバルな意味も持たないガード(パス B 以外に監査上の価値がない、純粋なローカル入力検証)は除外します。

    パス B — グローバルプロパティへ昇格し、すべての書き込み箇所を確認:各ガードについて、次のように考えます。「このガードが示すのは、この呼び出し時だけでなく、あらゆる呼び出しのシーケンスを通じて成り立つべきプロパティか?」

    • いいえ(ガードが、関数内で消費され、永続ストレージに結び付かない一時的なパラメーターだけを制約する場合)→ §1 のみに残します。昇格させません。
    • はい(ガードが永続的なプロパティを示す場合。例:入金時の require(amount >= MIN) は「すべてのアクティブなポジションが MIN 以上」を示し、セッター内の require(_fee <= 10) は「fee ∈ [0, 10]」を示す)→ ガードをグローバルプロパティとして書き換え、スコープ内のファイル全体で変数名を Grep し、制約対象のストレージ変数の書き込み箇所をすべて特定します。昇格対象となるすべてのガードについて、書き込み箇所を検索する Grep を単一の並列メッセージにまとめます。1 つずつ確認してはいけません。
      • すべての書き込み箇所で同等のガードが適用されている場合 → Bound 不変条件として §2 に昇格し、On-chain=Yes とします。導出にはガードを引用し、すべての書き込み箇所を確認したことを記載します。
      • 同等のガードなしに変数へ書き込む箇所が 1 つでもある場合 → Bound 不変条件として §2 に昇格し、On-chain=No とします。欠落箇所として、ガードのない書き込み箇所を引用します。これが最も重要な出力です。この欠落は、不変条件であると同時に、潜在的なバグでもあります。

    セッター自身のパラメーター検査によって制約されるストレージ変数にセッターが書き込む場合は、セッターの境界値制約も含めます。同じ書き込み箇所すべてを確認し、複数のセッターが同じ変数に書き込むものの、制約を適用しているのが一部だけなら、そのプロパティは On-chain=No です。

  3. 比率スキャン: A = B * C / D という形式の各ストレージ書き込みについて(ここで B、C、D はストレージ変数またはストレージの関数スコープのスナップショット)、その比率を記録します。スナップショットが同じ関数内の他の状態変更の前にとられたか後にとられたかに注意してください(順序が重要です。たとえば totalSupply が _burn の前にスナップショットされるか後にかなど)。

  4. ステートマシン / ワンショットスキャン: require(var == X); ... var = Y パターン内の各 enum/uint/address 変数について、その遷移を記録します。以下を区別してください:

    • ワンショットラッチ: require(var == default); var = concrete で、戻るパスが存在しないもの(例: setStrategy、setLeverager)。
    • トグル可能なフラグ: require(var == false); var = true だが、別の関数がそれを元に戻すもの(例: freeze/unFreeze、toggleVaultLeverage)。ステートマシンの不変条件ではありません — スキップしてください。
    • 循環状態: タイミングや条件によって false → true → false と駆動されるもの(例: ongoingVestingPosition)。循環不変条件として記録してください。
  5. 時間スキャン: ストレージ変数(deadline、lastUpdate、lockPeriod、interval)を含む各 block.timestamp または block.number の比較について、時間的制約を抽出します。その制約がチェックしてから更新される(安全)か、更新してからチェックされる(古い読み取りの可能性)かに注意してください。

  6. コントラクト間スキャン: 戻り値が算術演算またはストレージ書き込みで使用される各外部呼び出しについて、呼び出し側が何を前提としているかを記録します。次に、その状態に対する呼び出し先の書き込み箇所を見つけます。呼び出し先が(別の関数を介して)それを独立に変更できる場合、その前提は検証されていません — On-chain=No のコントラクト間不変条件として記録してください。両側(呼び出し側の前提 + 呼び出し先の書き込み箇所)がスコープファイル内にある行のみを含めてください。スコープ外のコントラクトについて推測しないでください。

    • また、以下も含めてください: セッター対不変条件の不一致 — 管理者セッターが、既存の不変条件が依然として成り立つことを確認せずにストレージ値を書き込む場合(例: 現在の流動性に対してチェックせずに setReserveCapacity を実行する)。これらは、セッターが 1 つのコントラクト/関数であり、不変条件が別の場所で強制されるという意味でコントラクト間です。
  7. 経済的導出: 手順 1〜6 の後、単一コントラクト + コントラクト間の不変条件の任意の組み合わせが高次の性質を暗示するかどうかを確認します。各経済的不変条件は、それが導出される特定の I-N / X-N ID を引用しなければなりません。導出チェーンにギャップがある場合(ソース不変条件の 1 つが On-chain=No)、その経済的不変条件も On-chain=No です。

検証ゲート(推定された不変条件を含める前に必須):

  • 保存則: 引用された行(同じ関数本体)に Δ ペアが存在することを確認します。
  • ガード(パス A、§1 行): require/assert/if-revert がコードから逐語的であることを確認します。
  • ガードリフト(パス B、§2 行): リフトされたグローバルプロパティが永続ストレージを参照している(一時的なパラメータの言い換えだけではない)ことを確認します。制約された変数のすべての書き込み箇所が Grep を介して列挙されていること、および On-chain=Yes/No の判定がその列挙と一致することを確認します — いずれかの書き込み箇所にガードが欠けており、その行が On-chain=Yes と述べている場合、その行は無効です。
  • NatSpec: @invariant タグまたはコメントが引用された場所に逐語的に存在し、かつグローバルプロパティを主張している(呼び出しごとの注記ではない)ことを確認します。呼び出しごとの注記である場合は、ドロップしてください — §2 にルーティングしないでください。
  • 比率: 数式が正確であり、スナップショットの順序(同じ関数内の他の書き込みの前/後)が記録されていることを確認します。
  • StateMachine: エッジの両側が存在すること、および逆パスが存在しないことを確認します。逆パスが存在する場合、それはトグル可能なフラグです — ドロップしてください。
  • 時間: 比較がストレージ変数を含んでおり、単に block.timestamp 対パラメータではないことを確認します。
  • コントラクト間: 呼び出し側の使用法と呼び出し先の書き込み箇所の両方がスコープ内に存在することを確認します。
  • 経済的: 参照されたすべての I-N / X-N ID 自体が検証済みであることを確認します。
  • 検証できない場合 → その行をドロップしてください。「検証できませんでした」は有効な行ではありません。 出力:不変条件の候補はinvariants.md(ステップ3a)に直接反映します。x-ray.mdのセクション3には、Enforced Guards(参照)に加えて、推定した不変条件のうち上位3~5件を記載します(Conservation、Cross-Contract、リフトされたガードの欠落に基づき、On-chain=Noを優先します。さらに、比率やステートマシンのラッチなど、構造的な網羅性を示すシグナルの強いYesの項目を1件含めます)。

ステップ3:出力を作成する

テストの存在とカバレッジ実行の区別(重要)

テストの存在は、ステップ1の列挙(test_files、test_functions、stateless_fuzz、foundry_invariant、echidna、medusa、hardhat_fuzz、fork、certora、halmos、hevmの各カウント)によって判定します。これらはファイルスキャンの結果であり、ツールチェーンでコンパイルや実行ができるかどうかにかかわらず、常に信頼できます。複数のシグナルを用いるカテゴリ(echidna、medusa、certora、halmos)はfunctions:configsの形式で出力します。たとえば、5:1はテスト関数が5件、設定ファイルが1件検出されたことを意味します。

カバレッジ指標(行/分岐%)は、インストール済みの依存関係、コンパイルの成功、テストの合格を必要とするforge coverageまたはhardhat coverageから取得します。カバレッジは、テストの品質とは関係のないさまざまな理由で失敗する場合があります。

  • 依存関係がインストールされていない(npm install/forge installが未実行)
  • コンパイラーエラー(stack-too-deep、バージョン不一致)
  • テスト実行の失敗(RPCがない、フォーク設定の問題)

ルール:

  1. テストの存在に関するすべての判断には、ステップ1の列挙結果であるtest_files/test_functionsを使用します。カバレッジツールの失敗から「テストなし」と推測してはいけません。
  2. カバレッジの取得に失敗しても、列挙結果からテストの存在が確認できる場合は、次のように報告します:"[N] test files with [M] test functions detected; coverage metrics unavailable — [failure reason]"。
  3. 「Gaps」サブセクションでは、欠落しているテストカテゴリ(stateless_fuzz=0、foundry_invariant=0、echidna=0、medusa=0、certora=0、halmos=0、hevm=0、fork=0)のみを指摘します。列挙結果でテストの存在が確認できる場合、「テストなし」と指摘してはいけません。監査への影響に基づいてギャップの優先順位を付けます。数値処理や金融ロジックにおいては、ステートフルファジングや形式検証の欠落は、フォークテストの欠落より優先度が高くなります。
  4. Git履歴の「Security Observations」では、カバレッジ取得の失敗を根拠に「テストなしで行われたコミット」と主張してはいけません。Git分析におけるtest_co_change_rateは、カバレッジではなく、コミット内でのファイルの同時変更率を測定します。この点を明記してください。
  5. カバレッジ取得に失敗しても、その失敗を脅威モデルやリスク評価に波及させてはいけません。テストの存在(列挙結果)とカバレッジ指標(ツールによる結果)は、互いに独立したシグナルです。

forge coverageの状態を確認します。完了していれば結果を含め、失敗していれば失敗理由を記載し、まだ実行中であれば「pending」と記載します。完了するまで待ってはいけません。

3a. すべての出力ファイルを作成する(1つのメッセージで並列Writeを4回実行)

すべての出力ファイルをx-ray/ディレクトリに配置します。4つすべてのファイルを1つのメッセージで書き込み、同時に作成されるようにします。

1. x-ray/architecture.json — references/templates.mdのアーキテクチャガイドのセクションにある形式とルールに従います(ステップ1で読み込み済み)。

2. x-ray/x-ray.md — references/templates.mdの出力テンプレートのセクションにあるテンプレートに従います(ステップ1で読み込み済み)。500行未満にします。内容を捏造してはいけません。セクション3(Invariants)はinvariants.mdへのポインターのみとします。Guardsの表を含めたり、推定した上位の不変条件を列挙したりしてはいけません。カウント(guards/single-contract/cross-contract/economic)とinvariants.mdファイルへの明確なリンクを記載した引用ブロックを1つだけ配置し、§3全体をその内容だけで構成します。不変条件の一覧はinvariants.mdのみに置きます。x-ray.mdにも重複して記載するのは以前のV2の動作であり、現在は正しくありません。 攻撃対象面の相互参照要件:セクション2「主要な攻撃対象面」を作成する際、各対象面を、作成したばかりの invariants.md のブロックと相互参照してください。対象面に記載した file:line が、いずれかの G-N / I-N / X-N / E-N ブロックの Location / Derivation / Caller side / Callee side の範囲内にある場合、対象面のタイトルの直後に、該当する ID を小文字のスラッグフラグメントを使った角括弧付き Markdown リンクとして追加してください。例:- **対象面名** &nbsp;&#91;[X-4](invariants.md#x-4), [I-17](invariants.md#i-17)&#93; — ...。各対象面の箇条書きの間には空行を入れてください。純粋にアクセス制御またはアップグレード可能性に関する対象面は、リンクなしでもかまいません。これは不足ではなく、健全な兆候です。複雑なプロトコルでの一般的な該当率:対象面の70%以上が、少なくとも1つの不変条件にリンクします。

3. x-ray/entry-points.md — ステップ2bで収集したエントリーポイントの全データと、Step 2b-flow のフローパスを使い、(ステップ1で読み込み済みの)references/templates.md のエントリーポイント用テンプレートセクションに従ってください。まず Protocol Flow Paths セクションを記述し、主要な各エントリーポイントに必要な前提条件の順序を矢印で示したチェーンを記載してから、アクセスレベルごとの詳細セクションを記述します。事実のみを記載し、脅威分析は行いません(脅威分析は x-ray.md に記載します)。プロトコルのエントリーポイントが30個を超える場合は、関数ごとの詳細ブロックの代わりに、ロール制限付きセクションと管理者セクションで簡潔な表を使用してください。数にかかわらず、パーミッションレスのエントリーポイントだけは詳細ブロック形式で記述します。

4. x-ray/invariants.md — (ステップ1で読み込み済みの)references/templates.md の不変条件マップ用テンプレートセクションに従ってください。セクションは4つです:Enforced Guards (Reference)、Inferred (Single-Contract)、Inferred (Cross-Contract)、Economic。表ではなく、#### G-N / #### I-N / #### X-N / #### E-N の見出しブロックを使用してください。 見出しアンカー(#g-1、#i-17 など)は、x-ray.md の攻撃対象面からファイルをまたいで張られる Markdown リンクのリンク先です。表のセル内にある <a id> アンカーは VS Code でファイルをまたぐリンクとして機能しません。各 G-N ブロックには、ガードが何を確認するかだけでなく、何を保護するのかを説明する Purpose 行を含めてください。推論に基づく各ブロックには、具体的な Δ ペア、ガードの解除と書き込み箇所、エッジ、時間的述語、または NatSpec の主張を必ず記載してください。記載できないブロックは削除してください。クロスコントラクトの各ブロックには、呼び出し元側の前提と呼び出し先側の書き込み箇所の両方を必ず記載してください(どちらもスコープ内のファイルである必要があります)。各経済ブロックは、特定の I-N / X-N ID から導出してください。ブロック数に上限はありません。事実のみを記載し、脅威分析は行いません。

セクション2(脅威と信頼モデル)の作成 — 出力テンプレートの構成に従ってください。脅威プロファイル、時間的脅威、コンポーザビリティの脅威に関する内容には references/threats.md を使用します(すべて1つのファイルにあり、ステップ1で読み込み済みです)。ハイブリッドの場合は、主となる攻撃者リストを先に記載し、その後に重複を除いた固有の二次的脅威を統合してください。

検証ルール(セクション2の作成時に適用):

  • パーミッションレスのエントリーポイント:ステップ2bでスキャン検証済みのリストのみを使用してください。ステップ2bの手順が正式な情報源です。サブエージェントの要約に依存しないでください。
  • セキュリティに関する主張:セキュリティチェックが欠落している、不完全である、または回避可能であると主張する場合は、実際のデータフローを関連コードから読み取って必ず追跡してください。具体的には、(1)対象の変数へのすべての書き込み箇所を特定し(Grep を使用)、(2)その書き込み箇所を踏まえて主張が成立することを確認してください。サブエージェントの要約だけでは不十分です。検証できない場合は、事実として断言せず、「確認できませんでした」と限定して記述してください。

セクション7(Git 履歴):x-ray/git-security-analysis.json の内容を、Contributors、Review Signals、Hotspots、Security-Relevant Commits(スコアが5以上)、Dangerous Area Evolution、Forked Dependencies、Tech Debt、Cross-Reference Synthesis(Git のシグナルとセクション2~3を関連付ける箇条書き2~4個)に反映してください。

ブランチのスコープ(重大)

Git 分析の対象は現在のブランチのみ(HEAD)です。JSON メタデータの git_branch フィールドに、分析対象のブランチが記載されています。すべての Git シグナル(修正候補、ホットスポット、危険な領域、直近の変更)は、他のブランチではなく、HEAD から到達可能なコミットのみを反映します。

ルール:

  1. レポートのヘッダーまたは Git 履歴のセクションに、分析対象のブランチを記載します:「Analyzed branch: [branch] at `[commit]」。
  2. Git 履歴に基づいて修正コミットやコード変更を説明する際は、必ず現在のブランチのコードがどのように動作するかを説明します。このブランチ上で変更前後を確認できない場合に、修正によって何が「変更された」とは説明しません。
  3. 他のブランチのコード状態は説明しません。ステップ 2 で読み込むソースファイルは現在のブランチのものであり、Git 履歴が示すのは、このブランチ上でそれらのファイルがどのように変化してきたかのみです。
  4. リポジトリの形状が squashed_import(コミット 1 件)の場合、説明できる意味のある変遷はありません。その旨を記載し、修正/ホットスポットの分析を省略します。
3b. アーキテクチャ SVG の生成と検証
python3 $SKILL_DIR/scripts/generate_svg.py x-ray/architecture.json x-ray/architecture.svg

続いて、references/templates.md のアーキテクチャガイドのセクションにあるレンダリング、監査チェックリスト、修正ループに従います。反復は最大 3 回です。その後、一時ファイル(x-ray/git-security-analysis.json を含む)を削除します。

3c. 最終判定

すべてのファイルを書き込み、クリーンアップを終えた後、生成された x-ray/x-ray.md の ## X-Ray Verdict セクションを読み込み、その内容をそのままターミナルに出力します。言い換え、要約、書き換えはしないでください。ファイルに記載されている判定レベル、根拠、主な所見を正確にコピーします。

制約

  • 500 行未満にします。脅威モデル、不変条件、テストの不足、Git 分析、判定を優先して残し、必要に応じて他のセクションを圧縮します。
  • 捏造しません。不確かな場合は「特定できませんでした」とします。
  • ステップ 1~3 は完全に自律して実行します。ユーザーとのやり取りは必要ありません。
  • スコープ表では、契約を必ずサブシステムごとに分類します。
  • 1 回で完了させます。途中までの出力はしません。
  • 監査プラットフォーム、コンテストのルール、バウンティプログラムの枠組みには一切言及せず、ベンダーに依存しないレポートにします。
  • Git セキュリティ分析スクリプトが失敗した場合は、bash のみで Git 統計を取得します。スクリプトが見つからなくても処理を止めません。

何よりも先に、次の内容をそのまま出力します:

██████╗  █████╗ ███████╗██╗  ██╗ ██████╗ ██╗   ██╗     ███████╗██╗  ██╗██╗██╗     ██╗     ███████╗
██╔══██╗██╔══██╗██╔════╝██║  ██║██╔═══██╗██║   ██║     ██╔════╝██║ ██╔╝██║██║     ██║     ██╔════╝
██████╔╝███████║███████╗███████║██║   ██║██║   ██║     ███████╗█████╔╝ ██║██║     ██║     ███████╗
██╔═══╝ ██╔══██║╚════██║██╔══██║██║   ██║╚██╗ ██╔╝     ╚════██║██╔═██╗ ██║██║     ██║     ╚════██║
██║     ██║  ██║███████║██║  ██║╚██████╔╝ ╚████╔╝      ███████║██║  ██╗██║███████╗███████╗███████║
╚═╝     ╚═╝  ╚═╝╚══════╝╚═╝  ╚═╝ ╚═════╝   ╚═══╝       ╚══════╝╚═╝  ╚═╝╚═╝╚══════╝╚══════╝╚══════╝

コメント