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

セキュリティ企業は、エージェントハーネスをコードベースに向けたところ、数十個のバグを発見したと説明する多数のブログ記事を公開しています（私たちもその一つです）。しかし、これらの記事はエージェントによるコードレビューに焦点を当てる傾向がありますが、これは私たちがセキュリティレビューでAIを使用する方法の一側面に過ぎません。私たちは異なる視点を提供したいと思います。コードレビューが始まる前に、エージェントはカスタムツールや形式モデルを構築することを可能にし、レビューの質と深さを向上させます。 私たちは最近、独自のカスタムアセンブリ言語とほとんど開発者向けツールを持たない新しいゼロ知識証明VMであるMiden VMをレビューしました。準備のために、私たちは6ヶ月かけてエージェントにLSPサーバー、デコンパイラ、静的解析エンジン、およびVMエグゼキュータのLeanモデルをゼロから構築させました。これらのツールは、悪意のあるプロバーがFalcon署名を偽造してMidenアカウント保有者から資金を盗むことを可能にする、検証されていないプロバー提供入力のような実際のセキュリティ問題を発見しました。さらに、Leanの作業は、Midenコアライブラリの大部分をカバーする95個の機械チェック済み正当性証明を生成しました。 Miden zkVMの監査 2025年末、Midenチームはローンチ前にゼロ知識証明VMの一部をレビューするために私たちに依頼しました。レビューの一部は、カスタムアセンブリ言語であるMidenアセンブリ（MASM）で書かれた少数の暗号プリミティブを含むMidenコアライブラリをカバーするようにスコープされました。これは、私たちがこれまで見たことのない低レベルのカスタムアセンブリ言語で複雑な暗号コードを書いている高信頼性プロジェクトであったため、私たちを本当に興奮させました。同時に、それは独自の課題も提示しました。 図1：左の画像は、2つの128ビット値（32ビットリムとして表現）のXORを計算するMASMプロシージャを示しています。右の画像は、32ビットx86アセンブリコードを使用した同じプロシージャの実装を示しています。 まず、Miden VMはスタックマシンアーキテクチャを実装しています。これは、各命令がスタックから読み取られた値で操作され、命令の結果がスタックの最上位に書き戻されることを意味します。概念的には単純ですが、命令の入力と出力はスタックから読み取られ、常に暗黙的であるため、MASMで書かれたコードのレビューは困難です。さらに、Miden VMは完全に新しいアーキテクチャであるため、IDEサポート、言語サーバープロトコル（LSP）サーバー、リンターのような開発者向けツールはほとんど存在しませんでした。 レビューの準備には6ヶ月かかることがわかっていました。実装はまだ機能が完成していなかったため、私たちは自問しました。「レビューがコードベースの可能な限り多くのバグを根絶することを確実にするために、時間とトークンを何に費やすことができるだろうか？」 すべてのツールを構築！ MASMには開発者向けツールが欠けていたため、プロジェクト開始時にどのようなツールが利用可能であってほしいかという問いから始めました。私たちは通常、コードレビューにVS Codeを使用しており、構文ハイライトとコードナビゲーションは可読性とコードベース全体でのデータフローを追跡するために不可欠です。これにはLSPサーバーと対応するVS Code拡張機能が必要でしたが、数日以内にClaudeに、構文ハイライト、定義へ移動、コード参照の検索、ホバー時のプロシージャドキュメントの表示などの機能を提供する、機能的なプロトタイプを構築させました。これらの基本的な機能が整ったので、インライン命令ドキュメントや個々の命令のスタック効果を表示するような、より言語固有の機能を追加することにしました。 図2：インラインスタック効果と命令ドキュメントでコードに注釈を付けることは、他の場所で命令セマンティクスを調べるために必要なコンテキストスイッチを防ぐのに役立ちます。 LSPサーバーを構築した後、手動およびエージェント駆動のレビューをサポートするために、高レベルのセマンティック情報を提供する他の方法を考え始めました。レビュー担当者が確認しているプロシージャの高レベルな制御フローとデータフローをすばやく理解できるように、VS Code UI内でMASMプロシージャの忠実な逆コンパイルを提供できるかどうかを確認するのは興味深いと考えました。MASMの場合、これは最初に現れるよりも難しい問題です。スタックマシンのリフティングと逆コンパイルはよく研究された問題ですが、手書きのMASMを逆コンパイルすることは、いくつかの理由で依然として困難です。 コアライブラリのほとんどのプロシージャには宣言されたシグネチャがないため、入力と出力の数はコンテキストから推測する必要があります。 MASMプロシージャは、明確に定義された呼び出し規約に従わず、そのような呼び出しの正味スタック効果は一般的に静的に決定不可能です。これは、すべての解析失敗が呼び出しチェーンを上に伝播することを意味します。 whileループはスタックニュートラルである必要がないため、whileループ条件は各イテレーションで異なるスタックスロットを占める可能性があります。これにより、命令の入力を後続の命令のスタックスロットにマッピングすることも不可能になります。 条件付きステートメントの異なるブランチは異なるスタック効果を持つ可能性があり、同様にスタック追跡とシグネチャ推測を困難にします。 これは、逆コンパイルされた出力が正しいことを望む場合、すべてのMASMプロシージャを逆コンパイルできるとは期待できないことを意味しました。したがって、私たちは定義されたサブセットのMASMを正しく逆コンパイルすることに焦点を当てました。デコンパイラ開発中、計画と開発にはClaudeを、コードレビューにはCodexを交互に使用しました。新しい機能が実装されるたびに、エージェントにコアライブラリからランダムに選択されたプロシージャを逆コンパイルさせ、元のMASMと比較して回帰がないかを確認しました。発見された問題は、モデルによって修正される回帰テストとして追加されました。 図3：256ビット整数（8つの32ビットリムとして表現）がゼロと等しいかどうかをテストするeqzプロシージャ、および対応する逆コンパイルされた擬似コード。 デコンパイラは、このプロジェクトのツール開発における最大の努力であり、数ヶ月にわたる100以上のAI生成コミットがありました。この作業の主な利点は、完全な逆コンパイルパイプラインではなく、静的解析に再利用できるデコンパイラの内部解析フレームワークと中間表現であることが判明しました。 デコンパイラが配置されたことで、各プロシージャの中間表現にアクセスできるようになり、命令の入力と出力が式として入力されました。これにより、MASMコードのバグ発見の問題に、データフロー解析などの標準的な静的解析メカニズムすべてを適用できるようになりました。これを使用して、中間表現に対する多数の解析パスを構築し、次のような質問に答えました。 プロバー提供のアドバイス値（剰余やモジュラ逆数など）は適切に検証されていますか？ 型制約（例：入力が32ビット整数またはブール値であること）は強制されていますか？ ローカル変数はすべての実行パスで初期化されていますか？ これらの問題を探索する1つの方法は、抽象解釈です。この手法の背後にある考え方は単純です。プログラムを実際の数値で実行するのではなく、解析は各ステップでスタック上に存在する可能性のある値の型（「32ビット整数」または「不明」など）を追跡します。新しい情報が見つからなくなるまで、コードを何度も歩き回ります。常にすべての可能な値を（少し余裕を持って）追跡しているため、実際のケースを見逃すことは決してありません。したがって、解析でチェックがパスする場合、プログラムのすべての実際の実行でそれが保持されることが保証されます。 ClaudeとCodexを使用して一般的な抽象解釈エンジンを構築し、その上に多数の具体的な解析パスを実装しました。エージェントは、上記のように開発とコードレビューを切り替えました。また、新しいツールをエージェント駆動のコードレビューワークフローで利用できるようにするために、デコンパイラと新しいMASMリンターの両方のコマンドラインインターフェースを設計および構築するようにエージェントに依頼することにしました。 すべてのバグを発見！ 実際のレビュー中、これらの解析により、型検証が可能であった400以上のユニークな場所が特定されました。