■ 1. 概要: AIによる大規模な形式検証
- 背景にある脅威:
- ほとんどのソフトウェアはバグを抱えており、AIはそれを容易に発見し悪用できる
- 従来のサイバー攻撃対策ではもはや不十分であり、コードにバグがないことを証明する手段が必要
- 形式検証の実用化:
- 形式検証は従来、長年にわたる専門家の労力を要し、多くの実プロジェクトでは非現実的だった
- Theorem社との共同研究により、LLMが大規模に形式証明を生成できることを示した
- これにより、証明済みのセキュリティ保証を含む新たな開発ワークフローが可能になる
- 主な成果:
- Claudeを用いて、100以上の実在のOSSライブラリについてアセンブリ(RISC-V)レベルでセキュリティ特性を証明した
- AIで本番ソフトウェアにアセンブリレベルの形式検証を大規模適用した初の取り組みと認識している
- 証明の過程で、数兆回のテスト実行でも見つからなかった長年のバグをClaudeが発見した
- 今後の見通し:
- モデル能力の向上に伴い、形式検証はセキュアなソフトウェア開発に不可欠な要素になる
■ 2. 形式検証の意義と従来の課題
- 成熟したソフトウェアにも残るバグ:
- 徹底的にテストされたLinuxカーネルでも、最近1,000件以上の脆弱性が公表された
- フロンティアモデルは無害に見えるバグを連鎖させ、重大なエクスプロイトにする能力を高めている
- 実環境で悪用される前にバグを検出し修正する技術が必要
- 形式検証の仕組み:
- コードを数学的モデルに変換し、定義したセキュリティ規則に常に従うことを証明する
- 証明に失敗した場合、規則に違反するバグが存在しうることを意味し、失敗の性質がバグの内容を示唆する
- 失敗原因の除去を繰り返すことで、最終的に規則違反バグが存在しない証明が得られる
- 従来の困難さ:
- 証明は元のコードの何倍もの規模になり、ニッチで高度に専門的なスキルを要する
- seL4カーネルは実装に2人年、形式検証に20人年を要した
- そのため形式検証はAirbusのアビオニクスコードなど、真にミッションクリティカルな用途に限られていた
- LLMによる変化:
- フロンティアモデルは実ソフトウェアの正しさの証明を完全自律的に生成できる
- 123のOSSライブラリについて、一部の実行成果物が特定条件下で決してクラッシュしないことを証明させた
- 証明した内容:
- 64MB未満のあらゆる入力で、メモリ安全性エラーやアサーション失敗なしに正常終了する
- モデル化されたあらゆるLinux OS応答とメモリレイアウトに対して成り立つ
- 証明の前提条件:
- シングルスレッドの静的バイナリであること
- 固定のメモリ予算で、Linux OS上のRISC-V CPUで動作すること
- 位置づけ:
- あらゆるバグの修正にはまだ遠いが、従来より大きく近づき、そこへのロードマップを示す
- 公開物:
- 証明の一部と、RISC-VおよびOSのセマンティクスを公開し、誰でも検証、再利用できるようにした
- Theorem社は他のOSSプロジェクトにも同じパイプラインを実行する提案をしている
- Theorem社は開発者が自身のコードの検証を始めるためのClaudeスキルも公開する
- 他手法の探索:
- zlib圧縮のセキュリティ評価、Rust製Pythonインタプリタの振る舞い等価性の証明にも取り組んだ
- 重要なソフトウェアに長年潜んでいたバグの根絶にも形式検証を用いた
- 前途の明るさ:
- モデルの知能向上により証明作成のコストは低下している
- 形式化されたコードが増え、保証手法が標準化されれば、証明の再利用によりコストが償却される
- 以前に性能の低いモデルで試して失敗した開発者にも、LLMでの形式検証を改めて勧める
■ 3. テストを証明に変換する手法
- 仕様(spec)の問題:
- 正しさを証明するには、まず「正しい」とは何かを仕様として定める必要がある
- PNGデコーダのようにRFC 2083に従う明確な仕様を持つプログラムもある
- テキストエディタやWebブラウザの「正しさ」は自明でなく、包括的で曖昧さのない仕様の入手は大規模検証の障害
- テストスイートを仕様化する発想:
- 既存のコンパイル可能なテストスイートを「このテストスイートは常にパスする」という規則として仕様に自動変換する
- RISC-Vにコンパイルされた任意のバイナリをLinux上で実行する汎用モデルを用いる
- LLMが適する理由:
- 数万命令のアセンブリのあらゆる振る舞いと入力を網羅する証明は、従来は手に負えなかった
- 明確に定義された目標に向けて数百万行のコードを処理する作業は、LLMに極めて適している
- ファズテストの性質:
- 開発者は入力を受け取るエントリーポイントを書き、クラッシュを起こす入力をバグとみなす
- ファザーは半ランダムかつ変異させた大量の入力を生成してバグを探す
- 本質的に総当たりであり、入力をいくら試してもすべてのコードパスを通る保証はない
- 入力は無限にあるため、探索は決して完全にならない
- ファズテストの仕様化:
- ファズテストを、コンパイル済みRISC-V命令上で定義された仕様に変換した
- 仕様の内容は、64MB未満のいかなる入力でもファズテストがクラッシュしないこと
- この上限の引き上げは、パラメータ変更と仕様再生成という些細な人手で済み、あとはClaudeが再証明する
- 証明できれば、そのエントリーポイントへのファジングは決してバグを見つけられず、不要になる
- OSS-Fuzzへの適用:
- GoogleのOSS-Fuzzに参加する数百のプロジェクトに適用した
- OSS-Fuzzには、アサーション失敗などでクラッシュさせる開発者作成のエントリーポイントが数千ある
- C/C++プログラムはAddressSanitizer(ASan)で自動計装され、不正なメモリアクセス時にクラッシュする
- メモリの不正アクセスはソフトウェア脆弱性の主要因であり、メモリ安全性はほぼ全ソフトウェアに当てはまる仕様
- 検証パイプライン:
- OSSライブラリと既存のファズテストをRISC-V実行ファイルにコンパイルする
- 実行ファイル、Theorem社のRISC-VとOSの形式セマンティクス、クラッシュしない特性から仕様を機械的に導出する
- Claudeが証明を書き、Rocqカーネルが仕様に照らして検査する
- 規模の実績:
- 数週間で、発見したバグを修正したうえで123ライブラリ、239エントリーポイントの無クラッシュを証明した
- 証明は合計約1億8,000万行のRocqで構成される
- 典型的な証明は約60万行で、対象バイナリのRISC-V命令数の中央値は1万8,000
- スコープ拡大の見込み:
- より多くのアセンブリアーキテクチャやOSプロセスのセマンティクスを標準化すれば、証明範囲の拡大は十分可能
- 全入力に対する証明の効果:
- エントリーポイントから到達可能なあらゆるパス上のクラッシュを排除する
- 証明を反復する中で、Claudeは残っている到達可能なクラッシュバグも発見し修正できる
■ 4. 信頼すべき要素の最小化
- 人手レビューの不要性:
- 膨大な証明コードだが、Rocq証明検査器が仕様の充足を保証するため、ほぼ人手レビューは不要
- 開発者が信頼すべき成果物:
- RISC-VとLinuxプロセスの形式モデル
- 証明された正確な定理文
- Rocq証明検査器そのもの
- 厳密には、Rocqが依存するハードウェア、OS、OCamlコンパイラも信頼する必要がある
- 「バグがない」ことの意味:
- ライブラリにバグがないことを意味するのではない
- 残るバグは上記の信頼対象の中にあるか、証明の範囲外にある
- 信頼対象の強化:
- Rocq、RISC-V、Linuxセマンティクスの強化は軽い作業ではない
- それでも証明が網羅する全コード行のデバッグよりはるかに扱いやすい
- 信頼対象の規模を増やさずに任意の数のプロジェクトを保護できる
- 独立検証の歓迎:
- 未公開の信頼対象、修正不要だったファズテストの完全なRocq証明、証明できなかったファズテストの仕様を公開する
■ 5. バグの発見と修正
- 証明過程でのバグ発見:
- 仕様の証明を試みる過程で数百件のバグが見つかった
- 自律的な修正ループ:
- バグのたびに人間を待たずに済むよう、Claude自身にバグを修正させた
- パッチ適用後のコードから仕様を再生成し、Claudeがその新仕様を証明する
- 報酬ハッキングへの対策:
- プログラムを自明にクラッシュしないものへ書き換えれば、どんな定理も証明可能になる余地がある
- あらゆるパッチにペナルティを課し、変更される入力とその少なさを証明すれば追加点を与えた
- パッチを記録し、こうした失敗パターンを監査した
- ファザーでは見つけにくいバグ:
- ファザーは通常1MB程度に制限された小さな入力を変異させ、コードカバレッジに頼って探索する
- 発見したバグの例:
- あるライブラリ内のデコンプレッサで、約20MBの特定レイアウトの入力のみで起きるカウンタのアンダーフローと範囲外書き込み
- 64MBの入力と2GB超のメモリを要する画像デコーダの範囲外読み取り
- 同一ファイルへの2つのハンドルにまたがる特定の呼び出し順序でのみ起きる範囲外読み取り
- 深くネストした入力を要するlibexpatのCVE-2026-56132の再発見
- クラッシュしない論理バグ:
- あるライブラリのメモリ安全性を証明中に、アプリが読み込めるファイルを制限する機能が常には強制されないことに気づいた
- 試みるだけで得られる利益:
- 最終目標は無クラッシュの証明だが、達成の成否に関わらず、この過程自体が修正すべき実バグを生み出す
■ 6. メモリ安全性を超える証明
- 高水準特性の証明:
- 実コードのファズテストは、エンコード/デコードの往復、冪等性、代数法則などの高水準特性を検査することが多い
- 差分テスト、自己整合性、参照実装との等価性もよく検査される
- 特性が成り立たなければクラッシュするため、無クラッシュの証明はその特性自体の証明と等価
- LZOの例:
- 圧縮後に伸長した結果が元と同じになることをアサートしており、無クラッシュの証明が往復特性の証明になる
- 開発者が明示しない特性:
- cpp-httplibの証明では、std::setのデストラクタの再帰によるスタックオーバーフローを排除する必要があった
- 再帰の深さは木の最大深さで制限されるため、libc++の赤黒木の再平衡が深さを対数に抑えることを機械語上で証明した
■ 7. その他の形式検証事例
- zlibの検証:
- zlibの圧縮形式を定めるRFC 1950の形式仕様をClaudeに書かせた
- Linuxカーネルのzlib実装がその仕様を正しく実装していることを、x86バイナリレベルで証明させた
- x86 ISAの形式セマンティクスはClaudeが生成し、十分にテストしたものを用いた
- 同じ手順を他の広く使われる6つほどのライブラリにも繰り返し、コーナーケースの軽微な(悪用不能な)バグを見つけた
- 発見したバグは上流への報告を進めている
- zlib検証から得た結論:
- 極めてよくテストされたコードベースは、既にほぼ完全に正しい
- 実在の既存コードベースについて、エンドツーエンドの正しさを証明することは可能
- ISAセマンティクス生成という教訓:
- Claudeが完全自律的にISAの形式セマンティクスを生成できたこと自体が興味深い
- セマンティクスが完璧とは言い切れないが、シングルステップ実行でLinuxカーネル上のUbuntuユーザ空間を起動できた
- 生成過程で公式リファレンス文書の数百件の誤りと、少数のハードウェア自体のバグを特定した
- Rust製Pythonインタプリタ:
- Pythonの大部分をRustで実装させ、学術論文のCPythonセマンティクスに従うことをVerusで証明させた
- 170万件超のランダム生成Pythonプログラムで、99.95%のテストがCPythonと同一の振る舞いを示した
- 残る差異は既知の想定内のコーナーケース
- 重要アプリケーションでの発見:
- 単純なセキュリティ特性の形式検証を試みる中で、広く使われる重要アプリケーションに問題を見つけた
- そのうち1つで、10年以上潜在していた未知の論理バグを発見した
- 広く使われるPDFリーダーの検証では、通常1年間に報告される数のセキュリティバグを1週間で見つけた
■ 8. 効率改善の見通し
- 主要な制約:
- 証明の生成に数億トークンを要することがある
- ソフトウェアエコシステム全体に普及させるにはコスト効率が重要
- 新しいモデルほど少ないトークン:
- 実際のOSS-Fuzzコードから36の小規模な検証タスクを作成した
- Opus 5.5はOpus 5より約40%少ないトークンで半数のタスクを証明した
- 各タスクは500万トークン予算で3回の独立した単一エージェント試行を行い、最初の完了時点で証明済みとした
- 長い検証タスクでの学習により、この傾向は続く見込み
- 証明の再利用:
- 証明はソフトウェアと同様に小さな証明から再帰的に構成され、小さいほど再利用しやすい
- 互いの証明を複製できる共有ワークスペースでは、単独作業より17%少ないトークンで済んだ
- 単独で失敗したエージェントが、共有環境では成功した例もあった
- 完了した34件の証明のうち30件で、単独作業の平均コストを下回った
- 単独作業のエージェントは2件の証明を完了できなかった
- 大規模での再利用:
- 証明の大半はCランタイムやASanの初期化など、全プログラムに共通するコードに関する
- そのため大きく異なるプログラムでも証明が大幅に重なる
- エージェントチームは他チームの完成した証明を複製し、自分のプログラムに適応させた
- libcups、freerdp、libzmqの例では、共有部分にほとんど新規コードが追加されなかった
- Mathlibとの類似:
- Leanの形式数学ライブラリMathlibは、700人超の貢献者による約30万の定理へと成長した
- 新しい証明が既存の成果の上に積み上がる構造であり、OSS-Fuzzの取り組みでも同様の証明群が蓄積した
- 未修正のバグを明かしうる証明は公開しない
- 既存ソフトウェアの検証戦略:
- 最も重要な依存関係から始めて、膨大な既存ソフトウェアを検証する戦略が必要
- 汎用仕様とバイナリレベルでの作業により、コードベース全体を別言語に書き直す必要を回避できる
- パッケージ単位の再利用:
- 各依存関係は一度検証すれば済む
- 依存関係はべき乗則に従うため、少数の共有ライブラリの証明で広範なソフトウェアが証明可能になる
- Theorem社は、glibc、OpenSSL、cURLを含むNixエコシステム全体の検証ロードマップを示している
■ 9. 限界
- 形式検証の限界:
- 実際には、形式検証が示せるセキュリティは期待より少ない場合がある
- 「形式検証済み」は「バグなし」ではない:
- 証明検査器は、仕様が現実と一致するかどうかを判断できない
- 仕様はCPUやOSを含め、実行環境のすべてを正しくモデル化する必要がある
- 検証済みコードのバグは、仕様や想定セマンティクスと現実との差異から生じる
- 裏を返せば、残るバグの所在と、その隙間を最小化するシステム設計の方向が分かる
- モデル外の実機の振る舞い:
- 証明はmusl libcにリンクされたシングルスレッドの静的RISC-Vバイナリが対象
- 実際の利用者の多くはx86やARM上で、glibcに動的リンクして使う
- 隙間を埋めるには、実環境に近いシステムモデルが必要であり、正確なx86セマンティクスの生成がその一歩
- 主張の範囲の不足:
- ASanはすべてのメモリ安全性バグを検出するわけではない
- 各ライブラリの全エントリーポイントを検証したわけではない
- 全エントリーポイントを検証しても、特にデッドコードがあればライブラリ全体はカバーされない
- 実プログラムがライブラリを誤用し、呼び出し側でメモリ破壊を起こす可能性がある
- 解消には、公開関数ごとに呼び出し側の義務を仕様化し、呼び出し側が厳守する必要がある
- 限界の克服:
- LLMの形式手法への活用知見が増え、モデルが向上すれば、これらの限界は扱えるようになる
- 依存するコードのはるかに大きな割合を検証できるようになる
■ 10. 結論
- 形式検証の将来:
- 従来は最も安全性が重要なコードに限られたが、まもなく今日のファジング並みにほぼ全本番ソフトウェアで実用的になる
- 静的型やテストフレームワーク同様、検証は「後付け」から「組み込み」へ成熟する
- その推進力はLLMだけでなく、言語設計や開発ワークフローの革新にもある
- 保証を伴うプロセスの必要性:
- LLMが自動で脆弱性を見つける時代には、コードのセキュリティ特性を保証できるプロセスが必要
- LLMで拡張された形式検証は、従来不可能だった範囲と規模で保証を得る有望な手段
- 呼びかけ:
- 多くの人に実験を促し、堅牢なソフトウェアが普及し、バグがよく理解され迅速に対処できる稀なものになる世界を目指す