Trail of Bits、エージェントを活用して MASM 監査ツールを構築、Lean による95件の正当性証明を公開

Trail of Bits は9月18日、Miden ゼロ知識仮想マシンの監査事例を公開した。チームは正式なレビューに先立ち、6カ月をかけてエージェントの支援を受けながら、言語サーバー、逆コンパイラー、静的解析ツール、Lean による実行モデルを構築した。今回公開されたのは、モデルの出力をプログラム解析と証明カーネルで検査する作業手法だ。[事例の原文](https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/)

Miden のアセンブリ言語 MASM はスタックを介してオペランドを受け渡すため、コードを読む際には各ステップでデータの位置を追跡する必要がある。公開された言語サーバーは、命令によるスタックの変化、逆コンパイル結果、型診断をエディター内に表示する。また、有限体の要素が32ビット整数として扱われているにもかかわらず、必要な検証が欠けているケースも検出でき、人間とエージェントが同じ解析情報を共有できる。[ツールのリポジトリ](https://github.com/trailofbits/masm-lsp)

チームの報告によると、静的解析によって型検証を改善できる箇所が400カ所超見つかったほか、深刻度の高い問題が1件発見された。剰余演算で証明者が提供する余りを十分に検証しておらず、Falcon 署名検証を回避できる可能性があるという。これらの箇所を、そのまま400件の悪用可能な脆弱性とみなすことはできない。また、報告には、現在のデプロイ環境におけるリスクを判断するための、修正済みバージョンの網羅的な一覧も示されていない。[監査での発見事項](https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/)

形式検証では、MASM の手続きを Lean の定義に変換し、仮想マシンの実行可能な意味論モデル上で正当性を証明する。公開リポジトリには、64、128、256ビット整数および word の操作にわたる、検証済みの95個の手続きが列挙されている。使用する Lean のバージョンとモジュールごとのビルド方法も示されており、外部の研究者が再検証するための出発点となる。[証明と検証手順](https://github.com/trailofbits/masm-lean)

ただし、証明の範囲は個別に確認する必要がある。例えば、64ビットの右ローテーションを行う手続きの定理には、「シフト量を32で割った余りが0ではない」という前提条件が明記されている。証明カーネルの検査を通過しても、裏付けられるのは指定されたモデルと前提条件の下での性質に限られ、仮想マシン全体の安全性が完全に保証されたと一般化することはできない。チームも、定理が本当に検証したい振る舞いを記述しているかどうかは、人間によるレビューが引き続き必要だと説明している。[定理の制約](https://github.com/trailofbits/masm-lean)、[人間によるレビューの方法](https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/)

エンジニアリングチームが参考にできるのは、エージェントによる探索の成果を、繰り返し実行できるツールとして定着させる点だ。導入時には、まず解析対象のコードと意味論モデルのバージョンを固定し、未対応の構文、定理の前提条件、回帰テストを確認する必要がある。その後に最も注目すべきなのは、コードの更新後も、これらの証明と診断が引き続き有効であり続けるかどうかだ。