暗号プロトコルの安全性を確かめるには、どこまで検証すれば十分なのか。従来、セキュリティ研究者はプロトコルの設計仕様を数学的にモデル化し、その安全性を証明する手法を発展させてきた。しかし、現実のソフトウェアでは、設計そのものが正しくても、それをコードとして実装する過程で脆弱性が入り込む可能性がある。設計上の安全性を証明することと、実際に動作するプログラムの安全性を保証することの間には、依然として大きな隔たりがある。
Google DeepMindの研究チームは2026年11月10日、この隔たりを埋めるための新たな形式検証システム「AlphaProof Code」を発表した。複数のAIエージェントを協調させ、メッセージングアプリのSignalなどで使われる暗号通信ライブラリについて、コンパイル後の機械語を対象に、特定の条件下でセキュリティ特性が成立することを機械的に検証したという。従来、実用規模の暗号実装を機械語レベルまで形式検証するには、専門家チームによる数年単位の作業が必要とされてきたが、DeepMindは今回の検証をわずか4週間で完了したと説明している。
ただし、今回の成果は「Signalアプリ全体の安全性が数学的に保証された」ことを意味しない。検証されたのは、特定のライブラリと検証用プログラムを組み合わせて構築した単一のLinuxバイナリであり、証明には暗号学的な仮定や実行環境に関する厳密な前提条件が設けられている。AIは何を証明し、どの部分が依然として人間による判断や検証に委ねられているのか。公開された技術文書を基に、その成果と限界を整理する。
約14万命令の機械語に対して10のセキュリティ特性を証明
DeepMindが主な検証対象に選んだのは、広く利用されている暗号通信技術「Signalプロトコル」の基盤ライブラリだ。具体的には、Rustで記述されたlibsignal-protocolのバージョン0.105.4と、耐量子計算機暗号に関連する拡張機能SPQRのバージョン1.6.0を使用した。研究チームはこれらの既存クレートに変更を加えず、検証用に独自開発したlibsignal-cliというテストハーネスに組み込んだ。続いて、Rustの公式コンパイラrustc 1.98.1を使い、LinuxのAArch64アーキテクチャ向けに静的リンクされた実行可能バイナリを生成した。
完成した実行コードのサイズは約560KBで、約14万命令に相当する。検証対象は、1対1の通信におけるPQXDHによるセッション確立と、メッセージの送受信を担うTriple Ratchetプロトコルの動作に限定されている。重要なのは、AlphaProof Codeが直接検証した対象がRustのソースコードではなく、コンパイル後の機械語だった点だ。研究チームは、このバイナリの命令がどのように実行されるかを数学的に記述し、その動作について定理を証明した。
この手法には、ソースコードを対象とする従来の形式検証とは異なる利点がある。ソースコード上で正しさを証明しても、コンパイラの不具合や最適化の影響によって、生成された機械語が意図と異なる動作をする可能性は残る。一方、コンパイル済みバイナリそのものを検証すれば、コンパイラが正しいコードを生成することを証明の前提とする必要がない。今回の研究では、こうしたコンパイラへの依存を信頼基盤から取り除くことができた。
研究チームが記号的モデルの下で証明したのは、合計10項目のセキュリティ特性である。これには、長期鍵などが後から漏洩しても過去の通信内容を保護する「前方秘匿性（Forward Secrecy）」や、一時的な端末侵害の後に安全な通信状態を回復する「侵害後セキュリティ（Post-Compromise Security）」が含まれる。さらに、ハンドシェイクの認証、鍵侵害偽装（KCI）攻撃への耐性、ハンドシェイク自体の機密性なども検証対象となった。ただし、これらの性質は、それぞれ定められた攻撃者モデルと環境条件の下で成立するものである。
DeepMindは、実際に広く利用されている暗号プロトコルの実装について、この水準まで機械的な形式検証を行ったのは、AIの利用有無を問わず史上初だと位置づけている。ただし、これは発表元による主張であり、第三者機関が過去の研究事例を網羅的に比較して認定したものではない。今回の成果を評価する際には、証明の規模だけでなく、どの範囲の動作が保証され、何が検証対象から除外されているかを確認する必要がある。
650万行の証明をAIが生成、人間が監査するのは2万6,000行の信頼基盤
AlphaProof Codeの特徴は、人間の専門家、AIエージェント、数学的な証明チェッカーの間で作業を分担する仕組みにある。検証工程は大きく「仕様の定義」「証明の構築」「証明の検査」の三段階に分かれており、それぞれに異なる役割が割り当てられている。AIが証明の生成を担う一方、何を証明すべきかという仕様の策定と、その仕様が妥当かどうかの判断には人間が関与する構成だ。
最初の段階では、人間の専門家が仕様記述エージェントと協力し、Signalプロトコルに求められるセキュリティ特性を対話型定理証明器Leanの定義や定理として記述した。研究チームは、約1万8,000行の仕様依存定義と、約8,000行のAArch64命令セット意味論を構築している。これらを合わせた約2万6,000行の記述が、今回の検証における主要な信頼基盤（Trusted Computing Base：TCB）となる。仕様が実際のセキュリティ要件に対応しているかについては、レビュー用エージェントと人間の暗号専門家が確認した。
仕様が定まると、推論モデルGemini 4 Carbonを利用する自律的な証明エージェントが、定理を成立させるための論理的な手順を探索した。その結果、約650万行に及ぶLeanの証明コードが生成され、関連する記述も含めたコード全体は700万行近い規模に達した。通常であれば、このような膨大な証明を人間が一行ずつ確認することは現実的ではない。そこでAlphaProof Codeは、生成された証明を機械的に検査する仕組みを組み合わせている。
AIが作成した証明は、まず「ゲートキーパー」と呼ばれる検査機構に送られる。ここでは、証明が人間によって承認された定義や依存関係と一致しているか、Leanの標準公理系のみを使用しているかなどを確認する。そのうえで、Leanの証明検証カーネルが、与えられた前提から結論が論理的に導かれることをチェックする。カーネルによる検証を通過しない証明は受け入れられないため、AIが生成した論証を無条件に信用する必要はない。
ただし、Leanが証明の論理的な正しさを確認できることと、証明の対象となる仕様そのものが現実の安全要件を十分に表していることは別問題だ。 仮に仕様の定義から重要な攻撃経路が漏れていた場合、その仕様に対する証明が完全に正しくても、実際のソフトウェアの安全性が十分に保証されるとは限らない。証明チェッカーが確認できるのは、あくまで与えられた定義と仮定に基づく数学的な整合性であり、現実世界で想定すべき脅威が過不足なく定義されているかどうかではない。
さらに、今回の証明では、約2万6,000行の仕様定義と命令セット意味論だけを信頼すればよいわけではない。Leanの検証カーネル自体の正しさに加え、Linuxプロセスの意味論、外部システムとのやり取りを表すフック関数の契約、暗号プリミティブに関する仮定、バイナリからコードを抽出するツールの挙動なども信頼の前提となる。一方、コンパイル後の機械語を直接検証したことで、Rustコンパイラそのものを信頼基盤から外せた点は重要な成果といえる。
今回の研究は、形式検証における人間の役割が変化する可能性を示している。AIエージェントが約650万行の証明を構築できるようになれば、専門家が膨大な証明手順を手作業で組み立てる負担は大きく減る。その一方で、証明の前提となる仕様や信頼基盤が正しいかどうかを判断する作業の重要性は、むしろ高まることになる。つまり、AIによる証明生成の自動化が進むほど、実用上の課題は証明を作る能力から、何をどのような前提で証明するかという仕様の品質管理へ移る可能性がある。今後、未監査の仮定を増やさずに仕様策定や信頼基盤のレビューまで自動化できることが示されれば、この課題の構図も変わるだろう。
記号的証明と計算量的証明では保証される安全性が異なる
今回の成果を正しく理解するには、研究チームが採用した二つの証明方式、「記号的証明（Symbolic Proof）」と「計算量的証明（Computational Proof）」を区別する必要がある。両者は暗号プロトコルの安全性を数学的に扱う点では共通しているが、攻撃者の能力や暗号技術について置く仮定が異なる。そのため、一方の証明が成立しても、もう一方が対象とする脅威にまで同じ保証が及ぶわけではない。
記号的証明では、暗号鍵や暗号文を抽象的な記号として扱い、暗号アルゴリズム自体が理想的に機能すると仮定する。例えば、攻撃者が復号鍵を持たない限り、暗号文から平文の情報を取得できないというモデルを用いる。この枠組みでは、プロトコルの状態遷移や鍵交換の手順、通信相手の認証などが正しく機能するかを検証できる。今回の研究では、コンパイル済みバイナリの実行動作をこの記号的モデルに結びつけ、10項目のセキュリティ特性について証明を行った。
ただし、現実の暗号アルゴリズムは数学的に完全なブラックボックスではない。攻撃者は暗号文のビット列に対して計算を行い、鍵や平文の推測、署名の偽造などを試みることができる。こうした攻撃まで評価するには、暗号技術の計算量論的な安全性を考慮する必要がある。このため研究チームは、記号的証明とは別に、計算量的な攻撃者モデルに基づく証明も構築した。
| 比較項目 | 記号的証明（Symbolic Proof） | 計算量的証明（Computational Proof） |
|---|---|---|
| 攻撃者モデル | 暗号プリミティブを理想化したDolev-Yaoモデル | 確率的多項式時間（PPT）で動作する攻撃者 |
| 主な保証 | 前方秘匿性、侵害後セキュリティ、ハンドシェイク認証、KCI耐性など10項目 | 鍵交換とメッセージ通信に関する計算量的な機密性・認証性 |
| 主要な仮定 | 理想的な暗号プリミティブ、独立した秘密の乱数生成 | Gap-DH仮定、XEdDSAの偽造不可能性、Kyber1024の衝突耐性、PRF・PRGの安全性 |
| 主な検証対象外 | サイドチャネル攻撃、メモリ破損、OSカーネルの不正動作、複数端末の同期、3者以上のグループ通信、SPQRの耐量子的な状態回復 | サイドチャネル攻撃、メモリ破損、乱数生成器の欠陥、量子計算機を用いる攻撃者、セッション昇格前の敵対的な初回メッセージ |
計算量的証明は、Gap-Diffie-Hellman（Gap-DH）仮定、XEdDSA署名の偽造不可能性、耐量子暗号Kyber1024の衝突耐性、疑似乱数生成器（PRG）や疑似乱数関数（PRF）の安全性など、複数の暗号学的仮定に依存している。これらの仮定が成立することを前提として、プロトコルの機密性や認証性を評価する仕組みだ。したがって、証明の成立は個々の暗号アルゴリズムが無条件に安全であることを意味せず、前提となる仮定が破られた場合には、そこから導かれる保証も見直す必要がある。
特に重要なのは、今回の計算量的証明が、量子計算機を利用する攻撃者を対象としていない点である。計算量的な安全性の評価では古典計算機を前提とする仮定が用いられており、量子計算機による攻撃に対する保証は与えられていない。記号的証明では耐量子鍵交換に関する抽象モデルも扱われているが、それだけで量子アルゴリズムによる暗号解読の脅威全体を検証したことにはならない。また、SPQRが備える耐量子的な状態回復機構についても、今回の証明対象から除外されている。
検証用の実行環境にも、実際のアプリケーションとは異なる制約がある。第一に、検証用ハーネスは鍵生成処理そのものを実行しておらず、通信当事者の公開鍵と秘密鍵が、セットアップ時に正しく与えられることを前提としている。第二に、バイナリレベルの検証では通信相手の身元鍵があらかじめ固定されており、初回通信時に相手の鍵を信頼する「Trust On First Use（TOFU）」に関する動的な確認手順は対象外となっている。これは、実際のSignalアプリで新しい相手と通信する際に発生する鍵確認の経路まで、安全性が証明されたわけではないことを意味する。
さらに、計算量的証明には、通信量やラチェット更新の回数に応じた数学的な制約もある。技術文書によれば、同一セッション内で大量のメッセージが送受信され、そのたびに新しいエポックが生成されるような極端な条件では、安全性を評価する式の余裕が失われる。1セッションあたり約2万5,000メッセージを超えるような頻繁なラチェット更新が発生した場合、計算上の保証の限界に達するという。ただし、これは証明で用いた評価式の限界を示すものであり、そのメッセージ数を超えた瞬間に実際の暗号が破られることを意味しない。
また、今回の検証対象は、研究者が構築したLinux環境で動作するlibsignal-cliのバイナリであり、Signalの公式スマートフォンアプリや、Signalプロトコルを採用するGoogle Messagesの実行環境全体ではない。複数端末間の同期状態の不整合、OSのメモリ破損、ハードウェアのサイドチャネル攻撃など、実際の利用環境で問題となり得る脅威は検証の範囲外にある。したがって、今回の成果は特定の実装に対する厳密な保証として評価すべきであり、Signalを利用するすべての製品の安全性を包括的に証明したものではない。
4週間で形式検証を完了、ただし計算コストは不明
DeepMindが強調するもう一つの成果が、検証に要した期間の短さだ。同社によれば、従来は専門家チームが数年を費やす必要があった規模の作業を、AlphaProof Codeによって4週間で完了できたという。ただし、この数字を「どのようなソフトウェアでも1カ月で形式検証できる」という一般的な生産性の指標として扱うことはできない。論文によれば、今回の実験には5名の研究者が専従し、それぞれのワークステーションでAIエージェントを昼夜連続して稼働させながら、仕様の策定と証明探索を並行して進めていた。
AIエージェントが主に自律的に処理したのは、定義済みの定理を成立させるための証明探索である。何を証明するべきか、どのような仮定を設けるべきかといった設計判断には、形式検証や暗号技術の専門家が継続的に関与していた。研究チームは、人間による重点的なレビューが必要な部分をコードベース全体の約1%に抑えられたと説明している。しかし、その限られた部分には、証明の妥当性を左右する仕様や信頼基盤が含まれており、作業量が少ないからといって重要性が低いわけではない。
データを表で見る
| 規模 (行数・命令数) | |
|---|---|
| バイナリ命令数（AArch64） | 140,000 |
| 信頼基盤（TCB） | 26,000 |
| AI生成証明コード | 6,500,000 |
今回の検証では、約14万命令の機械語に対し、約650万行ものLean証明コードが生成された。この規模の証明を自動構築できたことは重要な成果だが、そのために投入された総計算資源、モデルが消費したトークン数、金銭的なコストの詳細は公表されていない。従来の人手による検証と今回の実験では、対象となるコードや検証範囲、自動化ツールの成熟度も異なるため、単純な所要期間の比較だけで生産性向上の程度を判断することは難しい。
5名の専門家が専従してエージェントを連続稼働させたこと、検証対象が特定の約14万命令のバイナリに絞られていたこと、比較対象となる人手による検証の厳密な実測値が公表されていないことを考えると、今回の4週間という記録は、一般企業でも同じ成果を同じ期間で得られることを示すものではない。むしろ、AIエージェントを活用した形式検証によって、これまで膨大な人的資源を必要としていた作業に取り組める可能性を示した実験結果と評価するのが適切だろう。今後、異なるコードベースでも同程度の期間と実用的なコストで検証できることが示されれば、一般的な開発工程への導入可能性をより具体的に判断できるようになる。
一方、研究チームは、AlphaProof Codeが誤ったプログラムに対しても無条件に安全性を証明してしまうわけではないことを確かめる実験も行った。具体的には、Chevalらが過去にlibsignalで発見し、すでに修正されていた二つの脆弱性を、修正前の状態に戻す形で再導入した。既知の欠陥を意図的に加えたプログラムを使い、検証システムがその問題を検出できるかを調べるミューテーションテストである。
一つ目は、セッション状態の更新処理に問題があったコミットcd36118の修正を取り消した「Weak-state」の変異バイナリだ。二つ目は、楕円曲線暗号の演算で小さな部分群に属する入力を適切に排除していなかったコミット5293caaの修正を取り消した「Small-subgroup」の変異バイナリである。いずれも、過去に確認された実際の欠陥を再現するための変更だった。
研究チームがこれらの変異バイナリを再コンパイルしてAlphaProof Codeに入力したところ、システムは安全性が成立するという誤った証明を生成しなかった。代わりに、記号的セキュリティ定理に反する具体的な入力を構成し、対象のバイナリが安全性の条件を満たさないことをLean上で機械的に証明したという。これは、少なくとも今回選定された二つの既知の欠陥について、AlphaProof Codeが安全性の違反を検出できたことを意味する。
ただし、この結果を未知のあらゆる脆弱性を発見できる能力の証明と解釈することはできない。検証されたのは特定の二つの欠陥に対する検出能力であり、対象外の攻撃手法や脆弱性まで網羅的に発見できることが示されたわけではない。形式検証が保証できる範囲は、あくまで定義された仕様と攻撃者モデルによって決まる。この点は、AlphaProof Codeを一般的な脆弱性スキャナーと区別するうえでも重要である。
研究成果は公開されたが、一般向けの検証サービスではない
DeepMindは今回の発表に合わせ、形式検証の成果物をGitHubのgoogle-deepmind/code-verificationリポジトリでオープンソースとして公開した。公開された資料には、コンパイル済みバイナリから抽出した機械語のモデル、約2万6,000行の信頼基盤、Leanで機械的に検査できる定理ファイル群などが含まれている。これにより、外部のセキュリティ研究者や形式検証の専門家が、公開された証明やその前提条件を独自に調査できるようになった。ただし、成果物を公開することと、第三者が同じ検証結果を再現できたことは別であり、今後の独立した検証が重要になる。
また、今回の公開をAlphaProof Codeそのものの一般提供と混同してはならない。米Axiosの報道によれば、AlphaProof Codeは現時点で商業展開を前提としたサイバーセキュリティ製品ではなく、先端的な研究プロジェクトという位置づけにある。公開されているのは主に研究成果と検証用の資料であり、一般の開発者が任意のソフトウェアを入力して同じ検証を実行できる製品が提供されたわけではない。
証明生成の中核に使われたGemini 4 Carbonについても、利用環境には制約がある。Googleが2026年10月28日に発表した同モデルは、防御側のセキュリティ組織や一部の信頼されたパートナーに対して段階的に展開されている。一般の開発者がAlphaProof Codeと組み合わせ、APIから自由に自社製品の形式検証を実行できる環境は、現時点では整っていない。
DeepMindは公式解説で、将来的な応用先として医療機器のファームウェアや電力網の制御ソフトウェアなど、特に高い信頼性が求められる領域を挙げている。また、同社の自動脆弱性修正エージェント「CodeMender」や、セキュリティ研究チームProject Zeroとの連携についても展望を示した。ただし、これらは今後の研究開発の方向性であり、実際の重要インフラに対する検証が完了したことや、自動修正と形式検証を統合した仕組みが実用化されたことを意味しない。
企業の開発現場への導入という観点では、依然として複数の課題が残る。検証に必要なモデルへのアクセスが限定されていることに加え、証明生成に要する計算資源や費用が不明であり、異なるソフトウェアに適用する際の仕様策定や信頼基盤の整備にも専門知識が必要になる。したがって、現段階のAlphaProof Codeは、既存の開発パイプラインに直ちに組み込めるセキュリティ検査ツールというより、AIによる形式検証の可能性を示す研究成果であり、今後の検証手法を考えるための参考資料と位置づけるのが適切だ。
今回の成果で特に重要なのは、コンパイル済み機械語の検証において、人間が安全性の要件を定義し、LLMエージェントが膨大な証明を構築し、Leanの検証カーネルが数学的な正しさを確認するという、具体的な役割分担が示された点にある。AIが生成したコードや説明を人間がそのまま信用するのではなく、形式的な検証手段によって正しさを確かめる構造は、高い信頼性が求められるソフトウェア開発にとって重要な意味を持つ。
もっとも、AlphaProof Codeが証明したのはSignalプロトコルの絶対的な安全性ではなく、特定の暗号学的仮定と実行環境の下で、検証対象の機械語バイナリが定義されたセキュリティ特性を満たすという条件付きの数学的事実である。 その保証の前提には、人間が監査した約2万6,000行の主要な信頼基盤と、証明システムや実行環境に関する追加の仮定が存在する。今後、この手法が実用的な検証技術として広がるかどうかは、第三者が証明を再現できることに加え、別の暗号ライブラリや実システムにも適用できるか、そして必要な計算資源と専門家の作業量を含めて経済的に成立するかにかかっている。