9月18日、Trail of Bitsが「Auditing in the age of (good enough) AI」と題した記事を公開した。この記事では、AIエージェントを活用してzkVM（ゼロ知識仮想マシン）のセキュリティ監査に必要なツール群を一から構築し、実際の脆弱性を発見した6ヶ月間の実践について詳しく紹介されている。以下に、その内容を紹介する。
コードレビューより前に、ツールを作る
セキュリティ監査企業がAIエージェントでバグを大量発見した、という記事はすでに多い。Trail of Bitsもその一つだ。しかし本記事が伝えるのは、それとは異なるアプローチである。コードレビューが始まる前に、エージェントにカスタムツールと形式モデルを構築させるという方法だ。
対象はMiden VM——独自のアセンブリ言語（MASM）を持つ新しいzkVMで、開発ツールがほぼ存在しない状態だった。Trail of Bitsは2025年末にレビュー依頼を受け、本番レビューに備えて6ヶ月間をツール開発に充てた。
スタックマシンを解析するという難しさ
MASMはスタックマシンアーキテクチャを採用している。各命令はスタックから値を読み取り、結果をスタックトップに書き戻す。概念は単純だが、命令の入出力が常に暗黙的なため、コードのレビューが著しく困難になる。加えて、Miden VMは完全に新しいアーキテクチャであり、IDEサポートやLSPサーバー、リンターといった開発ツールが存在しなかった。
そこで同チームは問いを立てた。「6ヶ月と計算資源を使って、どうすればレビューで最大限のバグを発見できるか？」
作ったもの
Claudeを主な開発エージェントとして使い、以下の4つのツールをゼロから構築した。
- **LSP サーバー**：シンタックスハイライト、定義ジャンプ、参照検索、インライン命令ドキュメント表示など。数日で動作するプロトタイプが完成した。
- デコンパイラ：MASMの手続きを疑似コードに変換する。開発にはAI生成のコミットが100件以上、複数ヶ月を要した。最大の成果はデコンパイルパイプライン自体ではなく、静的解析に再利用できる中間表現（IR）だった。
- **静的解析エンジン**：IRの上に抽象解釈（abstract interpretation）を実装。「プルーバーが供給するアドバイス値が適切に検証されているか」「型制約が強制されているか」「ローカル変数が全実行パスで初期化されているか」などを自動チェックする。
- **LeanによるVM形式モデル**：定理証明支援系LeanでMiden VMエグゼキュータを実装し、手続きの正当性を機械的に検証する。
高深刻度の脆弱性を発見
静的解析エンジンは、型バリデーションが改善できる400箇所以上を特定した（いずれもライブラリの公開APIから到達可能）。さらに高深刻度の脆弱性を1件発見した。
問題はmod_12289という手続きにある。64ビット値を12289で割った余りを計算する処理で、商と余りはプルーバーがアドバイス値として供給する。商は64ビット整数として検証されるが、余りはu32overflowing_sub命令に渡される前に一切検証されない。
商と余りを巧みに操作することで、mod_12289が正しい余りではない値を返せることが確認された。悪意あるプルーバーはこれを悪用してFalcon署名を偽造し、Falconキーペアで管理されているMidenアカウントから資金を奪える。
形式証明で見つかった2件のバグ
Leanによる形式モデルでは、複数のエージェントが並行してコアライブラリの手続きの正当性証明を試みた。Leanカーネルが証明の正しさを機械的に検証するため、審査員は定理の記述が正しい性質を表しているかを確認するだけでよい。
結果として95件の正当性証明がバイナリ演算コンポーネント全体をカバーした。この過程で既存のユニットテストが捉えていなかった2件のバグも発見された。
- 64ビット右回転演算
rotr：シフト量が32の倍数のとき、Goldilocksプライム（2⁶⁴−2³²＋1）より大きな入力で誤動作する。 - 256ビット乗算
wrapping_mul：呼び出し元が所有するスタック上の値をリターン前に消去してしまう。
「2年前には無理だった」
Trail of Bitsはこう結論づけている。今日、失敗したサイドプロジェクトのコストはトークン代だけだ。
以前は探索的な性質が強いこの種のツール開発は、クライアントへの説明が難しく、リソースを割けなかった。エージェントが「軽い監督だけで非本業プロジェクトを回せる程度」に成熟したことで、経済的合理性が変わった。
Miden VMs チームはレビューで開発された静的解析エンジンを採用した。Trail of Bitsのサイドプロジェクトは、今後のMidenコアライブラリのアップデートのセキュリティにも継続して貢献することになる。
詳細はAuditing in the age of (good enough) AIを参照していただきたい。
