セキュリティ2026/11/10 19:46 UTC·2 分で読めます

DeepMindのAlphaProof Code、Signalの安全性を形式検証

Google DeepMindはAlphaProof CodeでSignalのPQXDHハンドシェイクとTriple Ratchetを形式検証したと発表。プロトコルの保証を実際のコードに結びつけた。

Abstract illustration of a padlock and lines of code representing formal verification of Signal's encrypted messaging protocol. — 画像: theregister

SUMO：数字パズル

Dialo：話して学ぶ語学アプリ

ediviewer：EDIファイルを文書のように読む

giftdetect：数分でぴったりの贈り物

Google DeepMindの研究チームは、Signalのメッセージ暗号化に関する形式検証を完了した。AIの支援により、プロトコルレベルの安全性保証を広く使われる暗号実装と結びつける証明を作ったのは初めてだと主張している。

使われたのは、形式的なソフトウェア仕様と検証のためのマルチエージェント基盤「AlphaProof Code」だ。人間が誘導するエージェントがLeanの仕様を書き、マシンコードの意味論を評価し、Leanカーネルが仕様に照らして確認する証明を作成する。今回はSignalのポスト量子対応PQXDHハンドシェイクとTriple Ratchetを検証し、libsignalにおける前方秘匿性、認証、侵害後の安全性、ハンドシェイクの秘匿性の設計を裏付けた。

検証の進め方

まず複数のモデルを使い、Signalの安全目標を人間がレビューする数学的仕様に落とし込んだ。その仕様に基づき、Gemini Carbonエージェントがlibsignal実装の正しさを示すLeanコードを生成。約650万行に及ぶコードの後、監査工程で人間の確認が必要な箇所を洗い出した。

結果は完全な暗号を前提とした理論上のもので、バイト列の計算量的な秘匿性は保証しない。それでも正しさを示す意義ある成果だ。Beneficial AI Foundationが4月に出した、SignalプロトコルとアプリをLeanで形式検証する課題への一歩でもある。

コストと今後

論文によると、seL4マイクロカーネルの検証には20人年、CompCertのC言語コンパイラ開発には6年を要した。今回のSignal検証は5人のチームで4週間、相当量のトークンを使ったという。

Google DeepMindの研究科学者でテキサス大学オースティン校教授のSwarat Chaudhuri氏は、検証のスケールが可能になった今、問題は何を検証するかだと述べた。攻撃的AIの能力が高まるなか、世界中の脆弱なシステムに応用したいという。次の段階はソフトウェア設計の過程への適用で、暗号プロトコルに限らず一般のコードが対象となる。同氏は、次のフロンティアは証明ではなく仕様だと語った。