要点
- Google DeepMind が、Signal の暗号ライブラリ libsignal の主要な安全性の性質を、AI エージェントと人の組み合わせで数学的に証明したと発表した。
- 証明されたのは「過去の会話が後から読まれない」「乗っ取られても会話が回復する」などの性質だが、対象は 1 対 1 の会話に限られ、グループや複数端末は含まない。暗号部品の安全性などは前提として仮定している。
- Signal が危ないという話ではなく、暗号の信頼を裏づける研究の発表である。
何が起きたか
2026 年 11 月 10 日、Google DeepMind と Google の研究者が「AlphaProof Code」の成果を公開した。複数の AI エージェントが協力して、実際のプログラムが安全性の約束を守っていることを証明する仕組みだ。Lean という証明支援ツールが、証明が正しいかを機械的に確かめる。
検証されたのは、Signal の libsignal（v0.105.4）と、量子コンピューターへの備えである spqr（v1.6.0）だ。Signal は 2025 年 10 月に、会話の開始時の鍵交換（PQXDH）に加えて、会話の途中で鍵を更新し続ける SPQR を導入した。既存の仕組みと合わせて Triple Ratchet と呼ぶ。(Signal の解説)
DeepMind の公開ページによると、証明した性質は次のとおりだ。
- 過去の会話は、あとで鍵を盗まれても読まれない（前方秘匿性）。
- 端末の鍵が一時的に漏れても、のちに会話が安全な状態へ戻る。
- 通信相手が本物であると確かめられる。
- 会話の開始時の鍵交換で作る鍵が、将来の量子コンピューターを持つ攻撃者に対しても秘密に保たれる。ただし、これは記号的なモデルでの証明に限られる。
特徴は、論文上の設計ではなく、実際にコンパイルした実行ファイルを対象にした点だ。証明の量は約 650 万行にのぼる。人が確認して承認するのは「何を証明するか」を書いた仕様で、証明そのものは 40〜80 のエージェントが 24〜72 時間かけて作った。
研究者は、過去に直された libsignal の欠陥 2 件をわざと戻し、証明が失敗して欠陥を検出することも確かめている。
日本の利用者への影響
今回は研究成果の発表で、日本の利用者への影響について述べた一次情報は確認できなかった。
Signal は、SPQR の導入でアプリの使い方は変わらないと説明している。
今すぐやること
- 特別な対応は要らない。Signal は更新で自動的に新しい方式へ移ると説明している。
- Signal アプリを最新版に保つ。
- 「証明された」を「絶対に破られない」と受け取らない。範囲と前提は下記のとおり限られる。
- 大事な連絡をする相手とは、安全番号（相手の鍵が本物かを確かめる数字）の照合も考える。
背景
形式検証は、プログラムが仕様どおりに動くことを数学で示す方法だ。ただ、人手では非常に高くつく。The Register によると、有名な OS カーネル seL4 の検証には 20 人年かかった。今回は 5 人のチームが 4 週間で進めたという。
一方、限界も公開ページに明記されている。
- 対象は 1 対 1 の会話だけ。グループ、複数端末、SPQR の量子耐性での回復の部分、鍵の生成は含まない。
- 量子コンピューターを使う攻撃者を想定した証明は、記号的なモデルに限られる。数値で安全の強さを示す計算量的な証明は、従来型の攻撃者のみが対象だ。
- 37 個の処理は、中身を検証せず、動きを契約（そう動くという約束）として信頼する扱いだ。暗号部品や一部の libc 関数（memcpy など）のほか、エラーメッセージの整形や、ファイル・標準出力へ書き込む処理も含む。
また、研究者が新しい未修正の欠陥を見つけたかは、確認できた範囲では書かれていない。なお、Signal の暗号の一部は別の検証もされている（Cryspen による F* を使った検証）。
技術者向けの詳細
- 対象: libsignal v0.105.4、spqr v1.6.0。1 対 1 のセッション限定。標準の rustc で AArch64 Linux 向けにビルドした実行ファイル（libsignal-cli で包む）。
- 操作: init（PQXDH）、send、recv。
- 記号モデル（Dolev–Yao）: 10 個の定理。前方秘匿性、侵害後の回復、認証、ハンドシェイクの秘匿（将来の量子攻撃者に対するものを含む）、鍵漏れなりすまし耐性。
- 計算量モデル: 機密性と真正性。従来型の攻撃者のみ。仮定は Gap-DH、XEdDSA、Kyber1024 の衝突耐性、HKDF と HMAC の PRF/PRG 安全性、AES-CBC と HMAC など。
- 信頼する部分: 仕様約 18,000 行、AArch64 の意味論約 8,000 行（467 命令、31 システムコール）。
- 範囲外: スレッド、動的リンク、PKI は本物と仮定、1 GiB を超えるメモリ。
- 記号モデルでは、事前鍵メッセージの完全な再送を同じセッションと数えるため、再送による前方秘匿性の喪失は排除されない。
- 一次情報: DeepMind の公開ページとコード。
