アンソロピック、クロードでOSSライブラリ123件を検証
- •アンソロピックとシーラム、OSS-Fuzzのライブラリ123件でセキュリティ特性を形式検証
- •239のテスト入口で証明を完了し、数百件のバグとCVE-2026-56132を発見
- •Opus 5.5、36課題の半数を旧モデルより約40％少ないトークンで解決
アンソロピックは22日（現地時間）、形式証明を専門とする企業シーラム（Theorem）と協力し、GoogleのOSS-Fuzzに登録されたオープンソースライブラリ123件のセキュリティ特性をClaudeで検証したと発表しました。数週間で239のテスト入口について、64MB未満のすべての入力がクラッシュせずに終了することを証明し、従来のファズテストで見つからなかったバグも発見しました。同社は、実際に運用されているソフトウェアの安全性を、アセンブリコードの水準でAIを使って大規模に検証した初の事例だと説明しています。
形式検証は、プログラムを数学的なモデルで表し、コードが定められた規則を常に満たすことを証明する技術です。従来は時間と専門知識が必要なため、航空電子システムやOSカーネルなど安全性が重要な一部のソフトウェアで主に使われてきました。マイクロカーネルseL4の実装には約2人年、形式検証には約20人年かかりました。アンソロピックは、AIモデルの推論能力の向上で検証の自動化と適用範囲の拡大が可能になったと説明しています。
今回の実験では、OSS-Fuzzの既存のファズテストを検証基準にしました。ファズテストは、変化を加えた入力を繰り返し与えてクラッシュやエラーを探しますが、すべての実行経路を確認できるわけではありません。Claudeはテストを、コンパイル済みのRISC-Vアセンブリコードに対する数学的な命題に変換し、64MB未満の入力で正常に終了すること、メモリ安全性のエラーやアサーション失敗が起きないことを証明しました。対象はRISC-Vプロセッサで動く単一スレッドの静的バイナリで、Linuxや固定のメモリ予算など特定の条件を前提としています。
完成した証明はRocq形式で合計1億8000万行に及びます。証明1件には、中央値でRISC-V命令1万8000個規模のバイナリを対象とする、通常60万行の証明コードが含まれていました。Rocqの証明チェッカーが仕様を満たすか確認するため、人が膨大なコードを一行ずつ調べる必要はありません。ただし、信頼性は命令、Linuxプロセスの動作モデル、仕様、チェッカーの正確さに左右されます。
Claudeは証明の過程で問題を直接修正し、修正後のコードも再検証して、数百件のバグを見つけました。解凍プログラムでは約2000万バイトの入力と特定のデータ配置でカウンターのアンダーフローが起き、メモリ範囲外への書き込みにつながる可能性を確認しました。画像デコーダーでは約6400万バイトの入力と2GBを超えるメモリを必要とする範囲外読み取りを発見しました。2つのハンドルを特定の順序で呼び出した場合に生じるメモリアクセスエラーや、深く入れ子になった入力で発生するlibexpatのCVE-2026-56132も再発見しました。クラッシュは起きなくても、ファイル読み込み制限が常に適用されるとは限らない論理エラーも見つかりました。
アンソロピックは別の実験で、Linuxカーネルのzlib実装が技術仕様に従うことを証明し、Rustで書かれたPythonインタープリターがCPythonと同じ動作をするかも検証しました。ランダムに生成したPythonプログラムを170万件以上実行し、99.95％で同じ動作を確認しました。広く使われるPDFリーダーの検証では、1週間で通常1年間に報告される水準のセキュリティバグを発見し、一部の重要ソフトウェアでは10年以上潜伏していた論理エラーも見つけました。
今回の証明は、すべてのバグが存在しないことを保証するものではありません。対象は64MB未満の入力と特定の実行環境に限られ、未検証の入口や別のプロセッサ、OSで起きる問題は保証しません。メモリ安全性ツールのASanも、すべてのメモリエラーを検出できるわけではありません。アンソロピックの社内実験では、Opus 5.5は36件の検証課題の半数をOpus 5より約40％少ないトークンで解決しました。複数のAIエージェントが証明を共有すると、個別に作業する場合よりトークン使用量が17％減りました。同社は証明の一部と検証モデルを公開しており、開発者は再利用や自社コードの検証に活用できます。シーラムも、同じ手順をほかのオープンソースプロジェクトに適用する支援をしています。