AIエージェントが600万行超の証明を生成、Signalの暗号実装を形式検証 - Google DeepMindが発表

Google DeepMindは11月10日、AIエージェントを活用してソフトウェアを形式検証の新たなフレームワーク「AlphaProof Code」を使い、Signalの暗号プロトコルの実際のコードについて、主要なセキュリティ特性が成り立つことを数学的に証明したと発表した。

AIエージェントが証明、人間は重要な1%をレビュー

DeepMindによると、研究者がAIモデルと協力してセキュリティ目標を数学的な仕様に落とし込み、専門家がそのすべてをレビューした。証明はエージェントが担い、正しさはLeanが自動で検査し、AIが作り出した証明をそのまま信用するのではなく、数学的に成立しているかを確認できるようにした。

• 

  AlphaProof Codeによる形式検証の概要

エージェントが証明を監査した結果、人間が再確認すべき箇所はコードベースの1%に絞り込まれた。設計だけでなく、デバイス上で実際に動くコードまで踏み込み、デバイスが一時的に侵害される前後でもメッセージが保護されるといった特性を証明した点が特徴だ。

作業は4週間で完了した。「Gemini 4 Carbon」を基盤とするAIエージェントが、証明言語Leanで600万行超の証明を生成した。専門家チームなら従来は数年かかるという。Google DeepMind リサーチサイエンティストのSwarat Chaudhuri氏はAxiosの取材に「ついに、ハッキングされないソフトウェアの世界にたどり着ける」と語った。

設計ではなく「実際に動くコード」まで検証

従来の暗号プロトコルに対する形式検証は、主にプロトコルの設計段階を対象としてきた。しかし、現実の脆弱性は、正しく設計された仕様と実際の実装とのずれから生じる場合がある。

今回の研究では、メッセージを送受信するデバイス上で実際に動作するコンパイル済みコードまで検証範囲を広げた。具体的には、デバイスが一時的に侵害された場合でも、その前後のメッセージを保護するなど、Signalが掲げる主要なセキュリティ特性を実装コードが満たすことを証明した。

AlphaProof Codeが安全なコードと問題のあるコードを区別できることを確認するため、研究チームは過去に修正済みの実在する脆弱性2件を隔離環境上のSignalコードへ意図的に再導入した。いずれの場合も、システムは変更後のコードが安全ではないことを機械検証可能な証明として示した。

Google DeepMindは、今回の成果を医療機器のファームウェアや電力網のソフトウェアなど、高い安全性が求められるシステムにも応用できる可能性があるとしている。今後はコードの脆弱性を自動修正するAIエージェント「CodeMender」などと形式検証を組み合わせ、AIを利用したサイバー攻撃の速度と規模に対抗することも視野に入れる。同社は検証成果物をオープンソースで公開するとしている。