Google DeepMind、AIエージェントを活用してSignalの中核的な機械語コードを検証

Google DeepMindは2026年11月10日、AlphaProof Codeを発表し、AIエージェントのチームを使って、Signalのコンパイル済みlibsignalコードにおける指定されたセキュリティ特性について、機械検証可能なLeanの証明を生成した。5人の研究チームは4週間で証明作業を完了し、仕様と検証成果物を公開して外部レビューに委ねた。

この研究は、Signalのプロトコル設計を抽象化したモデルを超え、コンパイル済みの実装を対象とした。研究者らは、改変していないlibsignal v0.105.4とSPQR v1.6.0のクレートを小規模なコマンドライン・ハーネスで包み、標準のrustcを使って静的リンクされたAArch64 Linux実行ファイルを構築した。技術論文では、この成果を、広く導入されている暗号プロトコル実装の未改変コードを対象とした、初のプロトコルレベルのセキュリティ証明と位置づけている。

AlphaProof Codeはどのように作業を分担したのか

5人の研究者は証明作業に4週間を費やし、ワークステーション上でエージェントを継続的に稼働させながら、記号的証明と計算論的証明を並行して進めた。論文によると、エージェントは約650万行の機械検証済みLean証明コードを生成し、その基盤となったのは、約2万6,000行の信頼済み仕様とAArch64の意味論だった。

人間が検証対象の特性を選び、曖昧さやセキュリティ上のトレードオフを解消し、仕様をレビューしたうえで、最終承認権を保持した。Gemini 4 CarbonとClaude Opus 5.5を搭載したエージェントが仕様の草案を作成してレビューし、そのレビューには異なるモデルファミリーによるものも含まれていた。その後、Gemini 4 Carbonのエージェントチームが証明コードをすべて生成し、著者の誰も証明コードを書かなかった。一般的な実行では、1台のマシン上で40～80のエージェントを24～72時間稼働させ、オーケストレーターとチームリーダーが証明作業エージェントを調整する一方、アーキテクトとインテグレーターの役割を担うエージェントが共有の証明基盤を維持した。

ゲートキーパーは、Leanのカーネルによる検査と、比較器による、保留されていた人間承認済み仕様との一致の確認が済んだ場合に限り、証明を受け入れた。この照合では、推移的に参照される定義をすべて含め、Leanの標準公理のみが使われていることも確認した。証明によって仕様上の問題が明らかになった場合、エージェントは小規模な修正を提案できたが、信頼済みの仮定を変更するには、人間の承認またはユーザーが設定したポリシーが必要であり、変更には根拠も記録された。この仕組みは、エージェントが生成する証明に伴う、すでに指摘されているリスクに対処するものだ。仕様は、その定義の一つを介して間接的に弱められる可能性がある。

セキュリティの対象範囲と過去のバグ検証

検証対象は、PQXDHハンドシェイクとTriple Ratchetによるメッセージングをカバーする、1対1のセッション向けコードだった。研究者らは、互いに独立した2種類の論証を報告している。理想化された暗号学的仮定のもとでの10個の記号的定理と、暗号学的仮定および統計的な項を通じて攻撃者の優位性に上限を設ける計算論的証明である。対象となる特性には、現在の状態が盗まれた後も過去のメッセージを保護する前方秘匿性、認証、侵害後の回復に関する侵害後セキュリティ、そしてハンドシェイクの秘匿性が含まれる。さらに記号的論証は、後にDiffie–Hellmanが破られた場合のハンドシェイクの秘匿性も対象としている。

これらの仕様で実際のエラーを検出できるかを試すため、チームは、weak stateとsmall subgroupとして知られる、以前に修正されたlibsignalの2つのバグについて、修正を巻き戻して改変後のバイナリを再コンパイルした。どちらの場合も、記号的セキュリティ定理が成立しないことを示すLeanの証明が生成された。公開検証リポジトリでは、計算論的証明、記号的証明、共有バイナリ、AArch64の意味論に関する資料を分けて収録し、証明を再ビルドして独立に検証する方法を説明している。

Signalの最高技術責任者であるEhren Kret氏は、この取り組みについて「コードのプライバシー保証に対する信頼が、さらに高まります」と述べた。

限界と今後の展開

この保証は、Signalのアプリケーション全体を認証するには遠く及ばない。対象となるのは、研究者らが構築したlibsignal-cliを新規プロセスとして実行した場合であり、鍵生成は検証されていない。グループメッセージングは今後の課題とされ、サイドチャネルとマルチデバイスの状態も対象シナリオから除外されている。低レベルの暗号プリミティブと、一部の出力処理やライブラリのルーチンは信頼済み契約で表現されているため、今回の成果は、そうした契約、承認済み仕様、Leanのカーネル、AArch64の意味論、およびプリミティブに関する仮定にも依存する。

論文によると、いずれの論証も、SPQRが追加することを目的として設計された耐量子暗号による回復力を証明するものではない。計算論的定理が対象とするのは古典的な攻撃者である一方、記号的なラチェット定理では、攻撃者がSPQRの鍵を選べる。また、計算論的モデルでは攻撃者の行動がいくつか制限され、メッセージ数やセッション数が十分に大きくなると、定理は空虚になる。こうした境界は、機械検証済みの証明を特定の導入環境におけるセキュリティ保証とみなす前に、外部レビュー担当者が何を信頼しなければならないかを示している。

研究者らが次の段階として挙げているのは、定理を強化すること、より多くのフックされたルーチンを検証し、暗号学的契約を検証済み実装に接続することで信頼基盤を縮小すること、そしてグループメッセージング、sealed sender、サーバー側プロトコルへ対象範囲を広げることだ。新しいlibsignalのリリースを出荷前に検証するという目標は研究上の目標であり、導入が発表されたわけではない。

この成果が直ちにもたらす意義は、役割分担を明確に示した点にある。エージェントが証明の構築を担う一方で、信頼性の確保は、人間がレビューした仕様と明示的な前提に基づいている。研究者たちがこのワークフローを継続的なlibsignalの開発に取り入れようとするなか、証明と検証手順が公開されたことで、外部のレビュアーもその基盤を検証できるようになった。