LLM を活用した形式検証：ソフトウェアセキュリティ保証の新たな飛躍

著者: Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal, Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich, Nicholas Carlini, Rajashree Agrawal, Jason Gross

概要

• 課題: 多くのソフトウェアにバグが存在し、AI はそれらを発見・悪用する。従来の防御策では不十分であり、コードがバグから完全に自由であることを証明する手法が必要。
• 解決策: 形式検証は保証を提供するが、従来は専門家による数年単位の労力を要し実用的ではありませんでした。Theorem との協業により、大規模な言語モデル（LLM） を活用して形式証明を生成することが可能になりました。
• 実績: Claude を用いて、100 以上のオープンソースライブラリにおける RISC-V アセンブリレベルでのセキュリティ特性を検証。
  • これにより、安全性が保証された新しいソフトウェア開発ワークフローを実現しました。
  • 証明生成プロセスにおいて、Claude は過去に数千万回のテストで見出されていなかったバグを発見しました。
• 展望: モデルの能力向上に伴い、形式検証は安全なソフトウェア開発において不可欠な要素となっていくでしょう。

序論：LLM が形式検証を可能にした背景

• 現状の問題点:
  • 成熟したかつ十分にテストされたソフトウェア（例：Linux カーネル）にもバグが存在し、LLM はそれらを見つけることが得意になっています。
  • 最先端モデルが悪意的なバグを連鎖させて致命的なエクスプロイトに繋げうるため、野外での悪用前に検出・修正する手法が必要です。
• 形式検証の役割:
  • コードを数学的なモデルに変換し、特定のセキュリティ規則に従うことを証明するアプローチです。
  • 証明が失敗した場合はルール違反を示すため、失敗の原因除去を繰り返してバグが存在しないことを最終的に証明できます。
• 従来からの課題:
  • 証明は元のコードより大きく、専門知識と多大な努力が必要でした（例：seL4 カーネルの実装に要した 2 人月に対し、検証には 20 人月）。
  • 航空機電子機器など、ミッションクリティカルなアプリケーションでのみ実用化されていました。
• LLM による革命:
  • 最先端モデルがリアルワールドのソフトウェアに対して完全に自律的に正当性証明を生成できるようになり、形式検証は大幅に容易になりました。
• 本プロジェクトのアプローチ:
  • 123 のオープンソースライブラリで有用なセキュリティ特性を検証しました（例：特定の条件下でクラッシュせず正常終了、メモリ安全エラーや断言失敗がないこと）。
  • これによりバグ修正のロードマップを提供し、証明の一部を公開・再利用可能にしています。

テストから証明へ（Turning tests into proofs）

• 「正しさ」の定義:
  • 仕様（spec）によって定義されます。しかし、多くのプログラム（テキストエディタ、ブラウザなど）については包括的で曖昧性のない仕様が得られず、検証の大きな障害でした。
• 解決手法：既存テストスイートから仕様の自動生成
  • オープンソースライブラリのコンパイル可能なテストスイートを自動的に仕様へ変換しました。
  • 「このテストスイートは常にパスする」というルールを、RISC-V コンパイル済みバイナリを実行することの意味を表すモデルに符号化しています。
• LLM の役割:
  • 歴史的には不可能だった数百万行のコード（数万行のアセンブリ命令）の振る舞いについて証明を書くことを可能にしました。
• プロセスの詳細:
  1. ファズテストからスタート: ファズサーが膨大な入力を生成しクラッシュを引き起こしますが、これは本質的に暴力行為でありどのパスも実行されるとは限りません。
  2. 仕様への変換: ファズテストを「64 MB 未満のあらゆる入力についてクラッシュしない」という仕様に変換しました。
  3. 証明の生成: Claude がこの仕様が証明できれば、以降のエントリーポイントへのファズリングは不要になります。
• OSS-Fuzz イニシアチブとの連携:
  • 数週間で、123 つの異なる OSS-Fuzz ライブラリ（239 のエントリーポイントを跨ぐ）について、64 MB 以下のあらゆる入力でクラッシュがないことを証明しました。
  • 典型的な証明はセキュリティ保証を与えるために約600,000 行に達します（Rocq を含む約 1.8 億行のコード）。
• 信頼できるコンポーネント:
  • 開発者が信頼する必要があるのは以下のアーティファクトのみです：
    • RISC-V および Linux プロセスの形式的モデル；
    • 証明された定理の正確なステートメント；
    • Rocq 証明チェッカー自体。

バグの発見と修正（Finding and fixing bugs）

• 自律的なバグ修正:
  • Claude は数百のエントリーポイントを証明しようとし、その過程で数百のバグを発見しました。
  • 人間による介入を最小限にするため、Claude にコードのパッチ適用と仕様の再生成を任せています。
• ファズサーで見逃された重大なバグ:
  • ファズサーは通常 1 MB 未満の入力に制限されるのに対し、Claude は以下の大規模なバグを発見しました：
    • デコンプレッサーのコピーにおけるカウンターアンダースローフ（境界外書き込み）。
    • 64 MB の入力および 2 GB 以上のメモリーが必要な画像デコーダーの境界外読み取り。
    • 同じファイルへの二つのハンドルの呼び出し系列を必要とする別のライブラリのバグ。
    • CVE-2026-56132 の再発見（深くネストされた入力が必要）。
• 論理バグの発見:
  • アプリケーションがロードできるファイルを制限する機能が一貫して強制されないなど、クラッシュしない論理バグも見つかりました。
• プロセスの利点:
  • RISC-V コンパイル済みファズテストにさらなるクラッシュがないことを証明すること自体が、修正すべき実際のバグをもたらすことを示しています。

メモリ安全性以上の証明（Proving more than memory safety）

• 高レベルプロパティの検証:
  • ファズテストにクラッシュがないことは、より高レベルのプロパティの成立を保証します：
    • エンコード - デコードラウンドトリップ
    • 冪等性、代数的法則
    • リファレンス実装との同値性
• 具体的な事例:
  • LZO 圧縮アルゴリズムにおいて、入力を超圧縮してデコンプレッションしたものが元のものと同一であることを保証しました。
• 非明言的なプロパティの発見と証明:

  • cpp-httplib

    の OSS-Fuzz 証明において、Claude は

    std::set

    デストラクタによるスタックオーバーフローの可能性を排除しました。
  • リバートコード上で libc++ の赤黒ツリー再調整アルゴリズムがツリーの深さを対数的に制限するために正しく最適化されていることを証明しました。

他の形式検証ケーススタディ（Other formal verification case studies）

• zlib 圧縮ファイルフォーマットの検証:
  • RFC 1950 の形式的仕様を作成し、Linux カーネル内の zlib 実装がそれに従うことを Claude に証明させました。
  • x86 アーキテクチャに対して直接証明を行い、マイナーなコーナーケースバグを発見・修正しました。
• Python インタプリターの同値性証明:
  • Verus を使用し、CPython セマンティクスに従うことを Claude に証明させました。
  • 170 万回以上のランダム生成プログラム実行の結果、99.95% のケースで CPython と同一の振る舞いを発見しました。
• セキュリティプロパティの確認:
  • 広く使用されている重要なアプリケーション（PDF リーダーなど）の問題を発見しました。
  • PDF リーダー検証において、通常年間報告される数と同じ数のセキュリティバグを一週間で発見しました。

これがまさに始まり（This is just the beginning）

• コスト効率の向上:
  • 最新のモデル（Opus 5.5 など）は fewer トークンで証明可能です。
  • 証明の再利用: エージェントが他者の証明をコピーして自分のターゲットに適用することで、トークン使用量を**17%**削減し、以前失敗した試みでも成功させることができました。
• 共有ライブラリの活用:
  • 多くの証明は C ランタイムや AddressSanitizer の初期化など共通するコードに関係しています。
  • エージェントチームはこれを利用し、完了した別のチームの証明をコピーして自分のプログラムに適応しました。
• 未来への展望:
  • 既存ソフトウェアの膨大な身体を検証するための戦略として、最も重要な依存関係から始め、汎用仕様とバイナリレベルでの動作によるアプローチが有効です。
  • これはパッケージ粒度での証明再利用を促進し、パワーロー法則に従います（小さい共有ライブラリセットさえ証明すれば膨大なソフトウェア範囲をカバーできます）。
  • Theorem ロードマップにより、glibc, OpenSSL, cURL などのインフラを含む Nix エコシステム全体の検証が可能になる見込みです。

制限（Limitations）

• 「形式的に検証」は「バグフリー」ではない:
  • 証明チェッカーは仕様と生体（現実の機械）が一致するかを知ることができません。
  • バグが発見されたのは、仕様が現実の機械モデル化しきれていないためです。
• 具体的ギャップ:
  • アーキテクチャの違い: 証明は単一スレッド・静的 RISC-V バイナリ（musl libc）ですが、実際には x86/ARM で動的に glibc を使用する場合が多い。
  • 仕様のカバー範囲: ASan はすべてのメモリ安全バグを検出せず、すべてのエントリーポイントも検証されていません。
  • 誤用による影響: ライブラリ自体は正しくても、呼び出し者が誤用することでメモリー腐敗が発生します。
• 将来への展望:
  • LLM の継続的な改善により、これらの制限が扱可能になり、より大きな割合の依存コードを検証できるようになります。

結論（Conclusion）

• 明確な軌跡:
  • 形式検証は、歴史的最も安全クリティカルなコードでの専門家保証のみから、今日すべての生産ソフトウェアにおいてファズリングと同じくらい実用的なものになります。
• 成熟への道:
  • 静的型やテストフレームワークと同様に、検証は LLM を活用し、「bolted-on」から「built-in」へと進化します。
• 社会への呼びかけ:
  • LLM スケール形式検証は、以前不可能な範囲とスケールでセキュリティ保証を実現する有望なアプローチです。
  • 他者を実験することを推奨し、堅牢なソフトウェアが広く普及し、ソフトウェアバグはよく理解され速く解決される世界を構築しましょう。