DeepMindがAIでSignalプロトコルの安全性を証明、次の目標はあらゆるソフトウェア

ソフトウェアセキュリティの世界には、長年にわたって存在する不都合な事実がある。私たちが日々依存する暗号化通信の安全性は、ほとんどの場合「今まで誰も突破できていない」という根拠の上に成り立っており、「突破不可能であることが証明されている」わけではない。2026年11月、Google DeepMindの研究成果がこの現状を変えようとした。研究チームはAIツールを用いて、広く普及しているSignal暗号化プロトコルの形式的検証（formal verification）を完了し、機械で検証可能な数学的証明によってプロトコルが設計通りに動作することを確認した。

「テスト」から「証明」へ：パラダイムシフト

この成果の重みを理解するには、まったく異なる二種類のセキュリティ評価手法を区別する必要がある。従来の手法はテストとペネトレーション（侵入テスト）だ。セキュリティ研究者が繰り返し脆弱性の発見を試みるが、攻撃に失敗したからといってプロトコルが安全であることにはならず、「今のところ誰も突破方法を見つけていない」というに過ぎない。一方、形式的検証は別のアプローチをとる。まず精密な数学言語でプロトコルの仕様をモデルとして記述し、次にそのモデルが一連のセキュリティ性質を満たすことを証明する。たとえば「攻撃者は長期鍵なしにセッション鍵を復元できない」「前方秘匿性はあらゆるメッセージシーケンスにおいて成立する」などがその例だ。

このアプローチは学術界では20年以上の歴史を持ち、ProVerif、Tamarin、CryptoVerif、そしてより低レイヤーのインタラクティブ定理証明器であるCoq、Isabelle、F*といったツールが使われてきた。問題はコストにある。産業レベルのプロトコルの完全な証明には、熟練した専門家が数ヶ月から数年を費やすことが多く、補題の追加やモデルの修正を繰り返す必要がある。これが、大多数の商用ソフトウェアが形式的検証を受けたことがない理由だ。

DeepMindの切り込み口はまさにこのコストの壁だった。WIREDの報道によると、研究チームはAIツールを活用して、証明プロセスの中で最も人手を要する部分——証明経路の探索、証明スクリプトの生成、中間補題の補完——を担わせ、最終的な検証は機械が行った。重要なのは、AIが提案する各ステップが証明検査器による機械的な検証を通過しなければならない点だ。これにより「AIが誤りを犯す可能性」が結論を汚染することはない。誤った推論は即座に棄却され、真に閉じた証明だけが通過できる。

なぜSignalプロトコルなのか

Signalプロトコルは現代の暗号化通信における事実上の標準だ。大きく二つの部分から構成される。セッション確立に使われるX3DH鍵合意プロトコルと、メッセージごとに鍵を進める「Double Ratchet（二重ラチェット）」機構だ。後者がもたらす「前方秘匿性」と「後方秘匿性」の特性により、仮に将来ある鍵が漏洩しても、過去の通信履歴を遡って復号することはできない。

このプロトコルはSignal公式アプリで使われているほか、WhatsAppでは数十億ユーザー規模で展開され、Google MessagesのエンドツーエンドRCSメッセージ、Facebook Messengerのシークレット会話モード、そして多数のオープンソース暗号ライブラリを支えている。つまり、プロトコルレベルの系統的な欠陥が存在すれば、その影響は世界規模に及ぶ。それゆえSignalプロトコルはこれまで学術界で繰り返し分析されてきたが、得られてきたのはあくまで「部分的な証明」——特定のバージョンや特定のセキュリティ属性が特定の仮定のもとで成立することの証明——であり、完全かつ一貫した、機械で検証可能な包括的結論ではなかった。

拡張目標：「世界中のあらゆるソフトウェア」に同じことをする

もしこの話が「著名なプロトコルが検証された」で終わるとしても、それ自体すでに十分重要だ。しかしDeepMindチームはその野心をより率直に語っている。

「彼らの拡張目標は？世界中のあらゆるソフトウェアに同じことをすることだ。」

この言葉は一見ほぼ荒唐無稽に聞こえるが、DeepMindの近年の研究の軌跡の中に置けば、さほど突飛ではない。AlphaProofとAlphaGeometryは国際数学オリンピックレベルの問題において機械による厳密な演繹推論の能力を示し、FunSearchは組合せ数学とアルゴリズム設計において人間がこれまで思いつかなかった構造を発見した。これらの研究に共通するのは、「厳密な推論を要し、かつ結果が機械的に検証できる」領域をAIの試験場としている点だ。形式的検証はまさにこの二条件に完璧に合致する。難易度は極めて高いが、正誤が明確だ。

より現実的な道筋は「すべてを検証する」ことではなく、検証コストを産業界が受け入れられる水準まで圧縮することかもしれない。プロトコルの証明が「専門家が一年かける」ものから「エンジニアが二週間で行える」ものになれば、セキュリティ監査の経済学は根本から変わる。その時、形式的検証は今日の静的コード解析と同様に、リリースプロセスにおける標準的な工程の一つになるかもしれない。

冷静な考察：証明が証明できること、できないこと

強調すべきは、形式的検証が万能薬ではないという点だ。その限界は冷静に認識する必要がある。

第一に、証明されるのは「モデル」であって「コード」ではない。仕様自体に誤りがあった場合、あるいは実装コードと仕様の間に乖離がある場合、証明は意味を失う。歴史上有名な「コンパイラへのバックドア埋め込み」という思考実験や、メモリ安全性やサイドチャネル攻撃に起因する実際の脆弱性の数々は、いずれもモデルの外側の戦場に属する。第二に、形式的検証は通常、乱数生成、タイミングリーク、電力解析などの物理レイヤーの問題をカバーしない。しかしこれらはまさに現実の攻撃で頻繁に使われる入口だ。第三に、AIが生成した証明は検査器による検証を経るとはいえ、「何のセキュリティ性質を証明するか」は依然として人間が設定する。誤ったセキュリティ目標を選べば、いかに美しい証明も的外れな回答に過ぎない。

したがって、より正確な表現はこうかもしれない。この成果はセキュリティの終着点ではなく、セキュリティのベースラインを一段階引き上げるものだ。「このプロトコルは高度な攻撃下でも成立する」という言葉が、エンジニアリング上の確信から、監査報告書に記載できる数学的事実へと変わった。

結語

暗号技術の歴史が繰り返し示してきたことがある。信頼は沈黙から生まれるべきではない——「誰も突破していない」という事実からではなく、公開された検証可能な論証から生まれるべきだ。今回DeepMindが行ったのは、AIを使って論証のコストを引き下げることだ。この道が開かれるなら、将来私たちがソフトウェアセキュリティを語る方法は変わるかもしれない。「ハッキングされたことがあるか」を問うのではなく、「その安全性は証明されているか」を問うようになるだろう。

本稿はWIREDの記事をもとに編集・翻訳したものです。