レッスン14 — Systems-code auditing

問い

Differential fuzz harness と chaos drill を ship した。コードは両方に通る。これで完了か？ いや — 両規律はコードを 走らせる ことで exercise する。Audit は走らせるだけでは表面化しないものを捕まえる — まだ exercise されていないコードパス、今日は動くが将来の修正で壊れる不変量、validate されない trust 仮定。読むことは独立した規律。

原理（最小モデル）

• Solidity audit と systems-code audit は別仕事. Solidity = 整数オーバーフロー / reentrancy / アクセス制御 / oracle 操作。Systems = レース条件 / 状態破損 / コンセンサス不変量違反 / unsafe 正しさ / 信頼境界漏れ。
• 5 systems バグクラス. ① 状態破損ウィンドウ（部分更新 + 中断）+ ② 並行性バグ（論理競合、loom + miri）+ ③ コンセンサス不変量違反（vote dedup / モノトニック time / 2f+1 厳密チェック）+ ④ unsafe ブロック正しさ（不変量 + 違反条件 + 検証）+ ⑤ 信頼境界漏れ（RPC / P2P / CLI / Engine API）。
• execute ↔ unwind の対称性. Reth ステージは「execute の state 変更を unwind が完全に undo」が不変量。非対称があれば破損ウィンドウ。
• すべての unsafe に 3 問. どの不変量に依拠? どの条件で違反? どう verify?（テスト / 型 / コメント証明）。「分からない」なら finding。
• 4 信頼境界. RPC（認証 + レートリミット + ペイロード検証）+ P2P（state root 検証 + tx 署名 + trie ノード）+ CLI / config（chainspec 内部一貫性）+ Engine API（hardfork rule）。
• ツールは reviewer を増幅、置き換えない. cargo audit / cargo geiger / kani / loom / miri / cargo clippy。
• 信頼性トライアングルを完成. Fuzz（正しさ）+ Chaos（耐性）+ Auditing（潜在的）。

具体例

5 バグクラスのチェックリスト:

ツール表:

Audit レポート構造（Sigma Prime / Trail of Bits / OpenZeppelin 共通）:

各 finding:

• Severity（Critical / High / Medium / Low / Informational）
• Title（1 行サマリー）
• Location（ファイル + 行番号）
• Description（2-3 文）
• Exploit / consequence
• Recommendation
• Status（Open / Acknowledged / Fixed）

レポート全体: Executive summary（1 ページ）+ Methodology + Findings + Out-of-scope。

信頼性トライアングル振り返り:

失敗例（誤解）

「Solidity audit 経験で systems-code も audit できる」— 間違い。バグクラスが違う。Solidity = ロジック層（reentrancy）/ Systems = システム層（レース条件、unsafe、信頼境界）。別の思考モデル + ツール。

「cargo geiger で unsafe 数を 0 に減らすのが audit」— 間違い。Audit は数を減らすことではなく 各 unsafe が明確な + ドキュメント化された不変量を持つこと。unsafe 自体は valid な道具、暗黙の仮定が問題。

「Audit はリリース前の独立 review session」— 半分間違い。Independent audit も必要だが、consensus に影響する全 PR を正しい問いを持って読む ことが日々の auditing。PR review に audit マインドセットを織り込まないと event 駆動になり遅れる。

🛑 予測。 Reth の execute ↔ unwind 対称性が示唆する audit の問いは？（答え: execute が行う state 変更で、unwind が undo しないものはないか？ あれば破損ウィンドウ。具体的に: ① execute が書き込むテーブルすべてを列挙、② unwind がそれぞれを reverse する処理を持つか確認、③ index / cache / 派生データも含めて完全か。1 つでも非対称があれば finding。）

ステップで組み立てる

Step 1: 5 バグクラスを即答

状態破損 / 並行性 / コンセンサス不変量 / unsafe / 信頼境界。

Step 2: execute ↔ unwind audit

Reth ステージで両方を読み、state 変更の完全対称性を確認。非対称 = finding。

Step 3: 全 unsafe に 3 問

不変量 / 違反条件 / 検証手段。1 つでも「分からない」= finding。

Step 4: 4 信頼境界をマップ

RPC / P2P / CLI / Engine API。各境界で「何が検証され、何が黙って信頼されているか」を問う。

Step 5: ツールを正しく使う

cargo geiger でスコーピング → loom で並行性 → miri で UB → kani で critical unsafe → clippy で lint。チェックリストが基盤。

Step 6: コンセンサス実装の不変量 audit

プロトコル不変量（HotStuff の「正しいレプリカは同じ高さで矛盾するブロックに vote しない」）をリスト → 各不変量について影響コードパス追跡 → state 永続化 / 原子性確認。

Step 7: 信頼性トライアングルを完成

Fuzz + Chaos + Auditing。1 つ ship なし = 既知ギャップ ship。

答え合わせ

• Solidity audit vs systems-code audit のバグクラス差: Solidity = 整数オーバーフロー / reentrancy / アクセス制御 / oracle 操作（言語 + コントラクト層）vs Systems = レース条件 / 状態破損ウィンドウ / コンセンサス不変量 / unsafe / 信頼境界（ランタイム + 並行性 + 物理層）。別仕事、別ツール、別 reviewer。
• 3 問が全 unsafe に適用される理由: unsafe は「Rust の安全性保証をプログラマが手作業で維持する」契約 → 不変量明示なしでは契約が不明 → 将来の refactor で違反可能。契約が明示されていれば違反検出可能。
• Loom と Miri の使い分け: Loom = 並行性順列テスト（複数スレッド interleaving を網羅、レース条件決定論的検知）。Miri = 実行時 UB 検出（unsafe 内の未定義動作、メモリ違反、aliasing 違反）。Loom は「論理が正しいか」、Miri は「メモリ安全性」。

合格基準

• 5 systems バグクラスを即答できる。
• execute ↔ unwind audit の問いを言える。
• 全 unsafe の 3 問を暗唱できる。
• 4 信頼境界の各々で問うべきことを言える。
• 6 ツールの役割を即答できる。

まとめ（3行）

• Systems-code audit は Solidity audit と別仕事 — 5 バグクラス（状態破損 / 並行性 / コンセンサス不変量 / unsafe / 信頼境界）。
• execute ↔ unwind 対称性 / 全 unsafe の 3 問 / 4 信頼境界マップ / 6 ツールの使い分けが日々の audit 道具。
• 信頼性トライアングル（Fuzz + Chaos + Auditing）3 つそろえて初めて production-grade、1 つ ship なし = 既知ギャップ ship。