（十分な性能の）AI時代のセキュリティ監査

（十分な性能の）AI 時代のセキュリティ監査

セキュリティ企業は、エージェントハーネスをコードベースに向け、多数のバグを発見したと説明するブログ記事を数多く公開しています（私たちもその一つです）。しかし、これらの記事はエージェントによるコードレビューに焦点を当てがちですが、それは私たちがセキュリティレビューでAIを使用する方法の一側面に過ぎません。私たちは異なる視点を提供したいと思います。コードレビューが始まる前に、エージェントはカスタムツールや形式モデルを構築することを可能にし、レビューの質と深さを向上させます。

私たちは最近、独自のカスタムアセンブリ言語とほとんど開発者向けツールを持たない新しいゼロ知識VMであるMiden VMのレビューを行いました。準備として、私たちはエージェントに6ヶ月かけて、LSPサーバー、デコンパイラ、静的解析エンジン、そしてVMエグゼキュータのLeanモデルをゼロから構築させました。これらのツールは、検証されていないプロバー提供の入力が、悪意のあるプロバーにFalcon署名を偽造させ、Midenアカウント保有者から資金を盗むことを可能にする、といった実際のセキュリティ問題を発見しました。さらに、Leanによる作業は95件の機械チェック済みの正当性証明を生成し、Midenコアライブラリの大部分を網羅しました。

Miden zkVM の監査

2025年末、Midenチームはローンチ前にゼロ知識VMの一部レビューを依頼してきました。レビューの一部は、カスタムアセンブリ言語であるMidenアセンブリ（MASM）で書かれた少数の暗号プリミティブを含むMidenコアライブラリを対象としていました。これは私たちにとって非常にエキサイティングな機会でした。なぜなら、それはまさに私たちの得意分野であり、高信頼性プロジェクトが低レベルのカスタムアセンブリ言語で複雑な暗号コードを書くという、これまで見たことのないものであったからです。同時に、それはいくつかのユニークな課題も提示しました。

［画像: “2つのコードリストが並べて表示されている：128ビット値のXORを計算するMASMプロシージャと、32ビットx86アセンブリで実装された同じプロシージャ”］

図1：左の画像は、128ビット値（32ビットリムで表現）のXORを計算するMASMプロシージャを示しています。右の画像は、32ビットx86アセンブリコードを使用した同じプロシージャを示しています。

まず、Miden VMはスタックマシンアーキテクチャを実装しています。これは、各命令がスタックから読み取られた値で操作され、命令の結果がスタックの最上位に書き戻されることを意味します。概念的には単純ですが、命令の入力と出力はスタックから読み取られ、常に暗黙的であるため、MASMで書かれたコードのレビューは困難になります。さらに、Miden VMは完全に新しいアーキテクチャであるため、IDEサポート、Language Server Protocol（LSP）サーバー、リンターなどの開発者向けツールはほとんど存在しませんでした。

プロジェクトがまだ機能完成していなかったため、レビューの準備に6ヶ月あることを知っていました。そこで私たちは自問しました。「レビューがコードベースのバグを可能な限り多く根絶できるように、時間とトークンを何に費やすことができるだろうか？」

全てのツールを構築！

MASMには開発者向けツールが欠けていたため、プロジェクト開始時にどのようなツールがあれば便利かという問いから始めました。私たちは通常、VS Codeをコードレビューに使用しており、シンタックスハイライトとコードナビゲーションは可読性とコードベース全体でのデータフローを追跡するために不可欠です。これにはLSPサーバーと対応するVS Code拡張機能が必要でしたが、数日以内にClaudeに、シンタックスハイライト、定義へ移動、コード参照の検索、ホバー時のプロシージャドキュメント表示などの機能のほとんどを提供する動作プロトタイプを構築させました。これらの基本的な機能が整ったところで、インライン命令ドキュメントや個々の命令のスタック効果を表示するような、より言語固有の機能を追加することにしました。

［画像: “インラインスタック効果と命令ドキュメントで注釈付けされたコードを示す図。これにより、命令セマンティクスを elsewhere で調べるために必要なコンテキストスイッチを防ぐのに役立つ”］

図2：コードにインラインスタック効果と命令ドキュメントで注釈を付けることは、命令セマンティクスを elsewhere で調べるために必要なコンテキストスイッチを防ぐのに役立ちます。

LSPサーバーを構築した後、手動およびエージェント駆動のレビューをサポートするために、高レベルのセマンティック情報を提供する他の方法について考え始めました。レビュー担当者が、見ているプロシージャの高レベルな制御フローとデータフローを迅速に理解できるように、VS Code UI内でMASMプロシージャの忠実なデコンパイルを提供できるかどうかを確認するのは興味深いと考えました。MASMの場合、これは最初に現れるよりも難しい問題です。スタックマシンリフティングとデコンパイルはよく研究された問題ですが、手書きのMASMをデコンパイルすることは、いくつかの理由で依然として困難です。

1. コアライブラリのほとんどのプロシージャには宣言されたシグネチャがないため、入力と出力の数はコンテキストから推測する必要があります。
2. MASMプロシージャは、明確に定義された呼び出し規約に従わず、そのような呼び出しの正味スタック効果は一般的に静的に決定不可能です。これは、すべての解析失敗が呼び出しチェーンを伝播することを意味します。
3. whileループはスタックニュートラルである必要はありません。これは、whileループ条件が各イテレーションで異なるスタックスロットを占有する可能性があることを意味します。これも、命令入力を後続の命令のスロットにマッピングすることを不可能にします。
4. 条件付きステートメントの異なるブランチは異なるスタック効果を持つ可能性があり、同様にスタック追跡とシグネチャ推測を困難にします。

これは、デコンパイルされた出力が正しいことを望む場合、すべてのMASMプロシージャをデコンパイルできるとは期待できないことを意味しました。そのため、私たちは定義されたMASMのサブセットを正しくデコンパイルすることに焦点を当てました。デコンパイラ開発中、計画と開発にはClaudeを、コードレビューにはCodexを交互に使用しました。新しい機能が実装されるたびに、エージェントにコアライブラリからランダムに選択されたプロシージャのセットをデコンパイルさせ、元のMASMと比較してリグレッションを探しました。発見された問題は、モデルによって修正されるリグレッションテストとして追加されました。

［画像: “eqz MASMプロシージャが、そのデコンパイルされた疑似コードの上に表示されている”］

図3：eqzプロシージャは、256ビット整数（8つの32ビットリムで表現）がゼロと等しいかどうかをテストし、対応するデコンパイルされた疑似コードとともに示されています。

[デコンパイラ]は、このプロジェクトのツール開発における単一最大の努力であり、数ヶ月にわたって100以上のAI生成コミットがありました。この作業の主な利点は、デコンパイルパイプライン全体ではなく、静的解析に再利用できるデコンパイラの内部解析フレームワークと中間表現であることが判明しました。

デコンパイラが配置されたことで、各プロシージャの中間表現にアクセスできるようになり、命令の入力と出力が式として入力されました。これにより、MASMコードのバグ発見問題に、データフロー解析のような標準的な静的解析メカニズムすべてを適用することができました。これを使用して、中間表現上で[多数の解析パスを構築]し、以下のような質問に答えました。

1. プロバー提供のアドバイス値（例：剰余やモジュラ逆数）は適切に検証されていますか？
2. 型制約（例：入力が32ビット整数またはブール値であること）は強制されていますか？
3. ローカル変数はすべての実行パスで初期化されていますか？

これらの問題を探索する1つの方法は、抽象解釈です。この技術の背後にある考え方は単純です。プログラムを実際の数値で実行する代わりに、解析は各ステップでスタック上に存在する可能性のある値の型（「32ビット整数」や「不明」など）を追跡します。コードを新しい情報が見つからなくなるまで何度も歩き回ります。常にすべての可能な値を（少しの余裕を持って）追跡するため、実際のケースを見逃すことは決してありません。したがって、解析でチェックがパスする場合、プログラムのすべての実際の実行でそれが保証されます。

ClaudeとCodexを使用して一般的な抽象解釈エンジンを構築し、その上に多数の具体的な解析パスを実装しました。エージェントは、上記のように開発とコードレビューを切り替えました。また、デコンパイラと新しいMASMリンターの両方にコマンドラインインターフェースを設計・構築するようにエージェントに指示しました。これにより、新しいツールをエージェント駆動のコードレビューワークフローでも利用できるようになります。

全てのバグを発見！

実際のレビュー中、これらの解析により、型検証が改善される可能性のある400以上のユニークな場所[2]（すべてライブラリの公開APIから到達可能）と、1件の高深刻度発見が特定されました。

［画像: “アドバイススタックから読み取られた剰余が、有効な64ビット整数であることを確認するために検証されていないことを示す図”］

図4：剰余はアドバイススタックから読み取られますが、有効な64ビット整数であることを確認するために検証されていません。

高深刻度の問題は、mod_12289プロシージャにおける制約が不十分なアドバイス値に起因していました。これは64ビット値を12289で割った余りを計算するもので、商と剰余がプロバーによってアドバイス値として提供されます。商は有効な64ビット値（32ビットリム2つで表現）であることを確認するためにチェックされますが、剰余は32ビット命令u32overflowing_subに渡される前に決して検証されません。商と剰余が減算の制約を満たすように慎重に変化させることで、mod_12289が正しい剰余ではない値を返す可能性があることがわかりました。悪意のあるプロバーはこれを悪用してFalcon署名を偽造し、Falconキーペアで制御されるMidenアカウントをすべて枯渇させることができました。

しかし、バグがなかったら？

これらすべての作業により、監査に入るにあたり、手動およびエージェント駆動のコードレビューをサポートする包括的なツールセットができました。しかし、手動レビュープロセスをサポートする他の方法について考える時間は十分にあり、さらに試したいアイデアがありました。例えば、コアライブラリのプロシージャが正しく実装されており、バグが含まれていない場合、[Lean]のような証明支援システムを使用してこれを証明することは可能でしょうか？

Miden VMは、命令セットが小さく、ほとんどの命令が副作用フリーであるため、形式モデリングに非常に適していることがわかりました。MASMを形式的にモデル化するために、まずLeanで最小限の[Miden VMエグゼキュータ]を実装し、ClaudeにMASMプロシージャからLeanへの自動トランスレータを構築させました。レビュー中、複数のエージェントが並行して、ライブラリ全体で可能な限り多くのプロシージャの正当性を証明しました。Leanカーネルは生成された証明が正しいことを検証できるため、各定理が対応するプロシージャの正しい正当性プロパティを証明していることを確認するために、定理ステートメントを手動で監査するだけで済みました。定理のレビューを容易にするために、コアライブラリで実装されているフィールド要素と整数型のLean型を導入しました。これにより、高レベルでは、ほとんどの正当性プロパティを次の形式で表現できるようになりました。

スタックが [x1, x2, x3, ..., xn, ...] で与えられ、プロシージャ P を実行した場合、P は終了し、スタックは [P(x1, x2, x3, ..., xn), ...] で与えられる。

図5：n個の引数を持つプロシージャPの正当性に関する高レベルなステートメント

私たちのエージェント駆動の形式モデリングの取り組みは、コアライブラリのすべてのバイナリ算術コンポーネントを網羅する95件の正当性証明をもたらしました。この作業は、既存の単体テストスイートが捕捉できなかった2つの微妙なバグも特定しました。1つ目は、64ビット右回転rotrのエッジケースで、回転シフトが32の倍数である場合に、大きな入力（Goldilocks素数より大きい）で誤って動作しました。2つ目は、256ビット乗算wrapping_mulの問題で、戻る前に呼び出し元が所有する値をスタックからドロップしていました。

［画像: “手動レビューの結果を示す図”］

図6：手動レビューにより、64ビットrotrプロシージャの正当性証明には、証明が完了するために追加の仮定（shift mod 32 ≠ 0）が必要であることが特定されました。

なぜ2年前にこれができなかったのか

このエンゲージメントにつながるまでに開発したツール、およびレビュー中に生成されたLeanライブラリと証明は、すべてサイドプロジェクトであり、1〜2年前であれば時間やリソースを割くことができなかったでしょう。これらのプロジェクトはしばしば非常に探索的な性質を持っており、最終的な結果や潜在的なペイオフを予測するのは困難です。実際には、クライアントに事前に販売するのは難しいということです。しかし、昨年、エージェントは軽微な監督だけでこれらの非必須プロジェクトを遂行できるほど十分に高性能になり、追求する価値のあるプロジェクトのエコノミクスを完全に変えました。今日、失敗したサイドプロジェクトはトークンしかコストがかかりません。

Midenでは、これらの事前作業のすべての利点が明らかでした。LSPサーバーと静的解析エンジンは、手動レビューのカバレッジを向上させ、エージェント駆動レビューを強化し、コードベース内の実際のセキュリティ問題を発見しました。これにより、数百万ドル相当の資金が失われる可能性がありました。AI生成のLean正当性証明は、ライブラリの大きくて基本的なコンポーネント全体の信頼性を向上させ、チームが自信を持ってその上に構築を続けることを可能にしました。チームはレビューのために開発された静的解析エンジンを採用しており、私たちのサイドプロジェクトは将来のMidenコアライブラリのアップデートも保護するようになります。

個人的には、これはTrail of Bitsでの長年のキャリアの中で最も興味深いプロジェクトの1つでした。もしあなたがこの種の仕事に興味があるなら、あるいは同様のものを構築しているなら、[お問い合わせ]ください。ぜひお話を聞かせてください！

---

1. これらはプロバーによって別のアドバイススタックを介して提供される事前計算済みの入力であり、慎重な検証が必要です。[↩︎]
2. これらの発見のほとんどは、コアライブラリのほぼすべてのプロシージャが公開APIの一部であったという事実によるものでした。これは、サードパーティの開発者が適切な検証なしにそれらを呼び出すことができたことを意味します。[↩︎]