Anthropic社は、AIモデルを用いて既存プロジェクトの信頼性とセキュリティを正式に検証する実験結果を発表した。この実験では、OSS Fuzzインフラストラクチャでテストされた123のオープンソースライブラリについて、メモリエラーが存在しないことを数学的に証明するためにAIモデルが使用された。
検証はRISC-Vアーキテクチャのコンパイル済みアセンブリコードレベルで行われました。生成された証明の総量は、Rocq Prover検証システムで約1億8000万行のコードに相当します（バイナリファイル1つあたり約60万行、RISC-V命令数1万8000）。これらの証明は、既存のファジングテストを自動的に形式仕様に変換することで生成され、その後、Claude AIモデルによって、最大64MBの入力データに対してプログラムに欠陥がないことが証明されました。
検証プロセスにおいて、AIモデルは、ファジングテストではこれまで検出されなかった数百ものバグを特定し、修正策を準備することができました。これには、特定の入力データを処理する際のバッファオーバーフローの脆弱性（libexpatのCVE-2026-56132など）や論理エラーなどが含まれます。さらに、AIモデルは、カーネルにおけるzlibアルゴリズムの実装が規格に適合していることを証明するためにも使用されました。 Linux RFC 1950仕様。
また、Pythonの一部の言語に対応するインタプリタがRustで生成され、Verusツールキットを用いてCPythonのセマンティクスへの準拠を示す正式な証明が作成されました。CPythonとの動作を比較するため、1.7万個以上のランダムに生成されたPythonプログラムが実行されました。99.95%のケースで、これらのプログラムを新しい実装とCPythonで実行した結果は一致し、見つかった相違点は既知のエッジケースでした。
形式検証は仕様への準拠を保証するものの、マルチスレッドの問題、動的リンク、実機ハードウェア上での異常動作などによるリスクは形式化されないため、セキュリティ上の問題を完全に排除するものではありません。提案する手法の重要な利点は、バイナリファイルを直接扱うことができるため、既存のコードを形式検証可能な言語で書き直す必要がないことです。
出所： オープンネット.ru
