Anthropic、Claudeが123のライブラリでセキュリティ特性を証明したと発表

Anthropicは2026年10月22日、Theoremとの共同研究で、Claudeがオープンソースライブラリ123件のファズテストのエントリーポイント239か所について、RISC-Vアセンブリコードのレベルでセキュリティ特性を示す機械検証可能な形式証明を作成したとする研究成果を発表した。

Anthropicによると、Claudeは見つけたバグにパッチを適用したうえで、64 MB未満のすべての入力と、モデル化されたLinuxオペレーティングシステムのあらゆる応答およびメモリ配置について、プログラムがメモリ安全性エラーやアサーション失敗を起こすことなく、必ず正常終了することを証明した。証明では、プログラムがLinuxを使用するRISC-V CPU上で、メモリ量が固定された単一スレッドの静的バイナリとして実行されることを前提としている。Anthropicによると、証明は約1億8,000万行のRocqで構成され、典型的な証明は約60万行に及び、命令数の中央値が18,000のバイナリを対象としていた。同社は、把握している限り、AIを使ってアセンブリコードのレベルで本番ソフトウェアに形式検証を適用する大規模な取り組みとして、これが初めてだと述べた。

証明の一部と、その基盤となるRISC-Vおよびオペレーティングシステムの意味論がGitHubで公開されている。Anthropicは、すでに公開されていないプロジェクト用の信頼性確保コンポーネント、パッチが不要だったファズテストの完全な証明、証明できなかったファズテストの仕様も公開すると述べた。一方、未修正のバグを明らかにするおそれがある証明は公開を見送る。

ファズテストを形式証明に変換

この手法では、各ライブラリに既存のコンパイル可能なファズテストを形式仕様に変換し、「64 MB未満の入力であれば、どのような入力でもテストがクラッシュしない」という単一の規則を表す。仕様は、RISC-V命令セットとLinuxプロセスに関するTheoremの形式意味論を用いて、コンパイル済みのRISC-V命令を対象に定義される。Rocqの証明チェッカーは、完成した各証明を仕様に照らして検証する。Anthropicによると、この方法で開発者が信頼すべき要素は、RISC-VとLinuxプロセスの形式モデル、正確な定理の記述、そしてRocqのチェッカー自体の3つに限られる。

Anthropicは、条件を満たすオープンソースプロジェクトに継続的なファズテストを提供するGoogleのOSS-Fuzzイニシアチブに参加する数百のプロジェクトに、この手法を適用したと述べた。OSS-FuzzはCおよびC++プログラムにAddressSanitizerを自動的に組み込む。AddressSanitizerは、メモリへの不正なアクセスがあるたびにプログラムをクラッシュさせるツールだ。2026年10月22日付の付録には、証明した定理の全容が記されている。64 MiB未満のすべての入力とあらゆるメモリ配置について、AddressSanitizerを組み込んだバイナリも通常のバイナリも、障害や異常終了を起こさず、モデル化されていない動作も示さない。また、両者の読み書きのトレース、終了時の動作、最終的なファイルシステムの状態はすべて同一である。

付録によると、この取り組みでClaudeは約10億行のRocqコードを記述し、そのうち約1億8,000万行が証明チェッカーを通過した。cJSONの391行のパーサー・エントリーポイントには63万行の証明が作成され、51,000行がリンクされたfftw3には48万行の証明が作成された。Claudeには証明を完成させる前にコードへパッチを適用することが認められていたため、Anthropicはパッチにペナルティを課し、パッチによって変更される入力を証明できた場合には追加評価を与えた。また、報酬の不正操作を防ぐため、パッチを記録して監査した。

証明の試みで発見されたバグ

Anthropicによると、証明を試みた結果、数百件のバグが見つかり、その多くはファザーでは発見されにくいものだった。あるライブラリのエントリーポイントを証明する過程で、Claudeは解凍プログラムのカウンターがアンダーフローし、範囲外書き込みを引き起こすバグを発見した。ただし、このバグが発生するのは、約20 MBの入力で、まれな特定のメモリ配置が生じた場合に限られていた。ほかにも、64 MBの入力と2 GBを超えるメモリを必要とする画像デコーダーの範囲外読み取り、同じファイルを指す2つのハンドルに対して特定の順序で関数を呼び出す必要がある範囲外読み取り、そして深くネストされた入力を必要とするlibexpatのCVE-2026-56132の再発見があった。

Claudeは、クラッシュを引き起こさないロジックバグも発見した。その中には、アプリケーションが読み込めるファイルを制限する機能が常に適用されるわけではないという問題も含まれていた。Anthropicによると、広く使われている複数の重要なアプリケーションを対象に検証を試みたところ、10年以上潜在していた未知のロジックバグが見つかった。また、広く利用されているPDFリーダーの検証では、通常1年間に報告される数と同じ数のセキュリティバグを、わずか1週間で発見した。

追加実験と効率に関する知見

OSS-Fuzz以外では、AnthropicはClaudeに、zlib圧縮形式を定義する技術文書RFC 1950の形式仕様を作成させ、Linuxカーネルのzlib実装がその仕様に正しく準拠していることを証明させた。Claudeは、Claudeが生成したx86命令セットの形式意味論を用いて、x86向けにコンパイルされたバイナリを直接証明した。Anthropicによると、同社は同じ手順をほかの広く使われているライブラリ6種類ほどにも適用し、悪用できない軽微な境界条件のバグを発見して、上流プロジェクトに報告している。また同社は、x86の意味論を生成する過程で、公式のリファレンス文書に数百件の誤りと、ハードウェア自体にそれより少ない数のバグが見つかったと報告した。さらに、意味論を1命令ずつ実行することで、Linuxカーネル上でUbuntuのユーザー空間を起動できるという。

別の実験では、ClaudeはRustでPythonの大規模なサブセットを実行するインタープリターを構築し、検証ツールVerusを用いて、学術論文で示されたCPythonの意味論に準拠していることを証明しました。技術付録によると、インタープリターの17段階すべてが証明され、次の定理が成り立ちました。「インタープリターが結果を返す場合、その結果は形式意味論が規定するものと一致する」。Anthropicによると、ランダムに生成したPythonプログラム170万件を用いた実証テストでは、テストの99.95%でCPythonと同一の動作が確認されました。また、意図的に埋め込んだ7件のバグのうち、ランダムテストでは5件が検出されずに残った一方、証明では7件すべてが不成立につながりました。

効率を測るため、Anthropicは実際のOSS-Fuzzのエントリーポイントを縮小し、36件の小規模な検証タスクを作成しました。生成されたプログラムは283～2,491命令で、入力は64バイトまでに制限され、AddressSanitizerは約100命令の「mini-ASan」ランタイムに置き換えられました。Anthropicによると、Opus 5.5はOpus 5より約40%少ないトークン数で、タスクの半数を証明しました。また、共有ワークスペースで互いの証明をコピーできるエージェントは、単独で作業するエージェントより必要なトークン数が17%少なく、単独では以前に失敗したタスクを成功させたケースもありました。一方、単独で作業したエージェントは、2件の証明を完了できませんでした。同社によると、OSS-Fuzzの取り組みでも同じ再利用効果が大規模に見られました。証明の多くが共通のCランタイムとAddressSanitizerの初期化コードを対象としているため、エージェントのチームは完成済みの証明をコピーし、改変して活用しました。

明示された限界とOSS Verifyプログラム

Anthropicは、証明がライブラリーにバグがないことを意味するわけではないと述べています。残るバグは、信頼されたコンポーネント内に存在する可能性も、証明の対象範囲外にある可能性もあります。証明の対象は、musl libcにリンクされたシングルスレッドの静的RISC-Vバイナリーです。一方、ユーザーの大半はこれらのライブラリーをx86またはARM上で実行し、glibcに動的リンクしています。また、AddressSanitizerはメモリー安全性に関するすべてのバグを検出できるわけではありません。同社は、モデルの性能向上に伴い、こうした限界への対処が可能になると見込んでいると述べました。

Theoremは、条件を満たすオープンソースプロジェクトに対し、OSS Verifyプログラムを通じて、同じパイプラインを無料で提供しています。登録するには、プログラムのリポジトリにproject.yaml、Dockerfile、build.shの各ファイルを追加するプルリクエストを送ります。Theoremによると、プロジェクトの審査はOSS-Fuzzと同様の方針で行われ、広く利用されている重要な基盤が優先されます。Theoremによれば、メンテナーには、各ファズターゲットが最大64 MiBまでのあらゆる入力でクラッシュしないことを示すRocqの証明が提供され、Rocqカーネルによる検証も行われます。証明作業中に見つかったバグは、公開期限を設けず、メールでメンテナーに非公開で報告されます。また、証明の作成には数日かかる場合があります。Theoremのロードマップでは、glibc、OpenSSL、cURLなどの重要な基盤を含むNixエコシステム全体の検証を目指しています。