Google DeepMind は11月10日、AI エージェントを使い、メッセージアプリ Signal の暗号の仕組みが安全であることを、実際に動くプログラムの段階で数学的に証明したと発表した。対象は Signal が公開している暗号ライブラリ libsignal をそのままビルドした実行ファイルで、証明は Lean という言語の検査器が機械的に確かめている。
毎日使うアプリの安全は、これまで専門家のレビューと評判を「信頼する」ものだった。その一部が、前提つきで「確かめられる」ものに変わり始めている。
証明された範囲は、どこまでか
語の範囲を先に絞っておきたい。DeepMind の検証資料によると、対象は libsignal v0.105.4 を Rust の標準のコンパイラでビルドした、Arm の 64 ビット (AArch64) Linux 向けの実行ファイルだ。扱うのは、最初の鍵交換 PQXDH と、メッセージごとに鍵を更新し続けるトリプルラチェット。証明したのは、会話の開始・送信・受信の 3 つの処理になる。
証明された性質には、過去のメッセージが後から読まれないこと (前方秘匿性)、端末が一時的に乗っ取られても、その後のやりとりで安全が戻ること、相手が本物であること (認証) などが含まれる。
対象外も、資料にはっきり書かれている。
- 1 対 1 の会話だけで、グループのメッセージは今後の課題
- 鍵を生成する処理は証明に含まない
- 計算量にもとづく証明は、量子計算機を持たない攻撃者が前提
- 処理時間や消費電力から秘密を探るサイドチャネル攻撃は扱わない
- Android や iOS のアプリも同じ Rust のコードを使うが、定理がそのまま当てはまるのは、それぞれの環境がプロトコルの振る舞いを保つと信頼する場合に限る
ハッシュ関数などの暗号の部品そのものは破られないと仮定したうえでの証明でもある。「Signal は絶対に安全だと証明された」と読むと、範囲を広げすぎることになる。
600 万行の証明と、人が見た 1%
量の面でも新しい。Gemini のモデルで動くエージェントが 600 万行を超える Lean の証明を書き、作業は 4 週間で終わったという。DeepMind は、同じ規模の検証は専門家のチームで何年もかかってきたとしている。
人の役割は消えていない。何を証明するかを決める仕様は専門家が全部確認し、証明はエージェントが点検して、人が見るべき箇所を全体の 1% に絞った。Lean の検査器を通った証明は、書いたのが人でも AI でも同じ基準で正しさが保証される。
試験もしている。過去に実際にあり修正済みのバグ 2 件を、隔離した版にわざと戻したところ、どちらでも「この版は安全ではない」という証明が機械的に出てきた。
DeepMind は、広く使われている暗号プロトコルをこの深さで AI が形式検証したのは初めてで、こうしたプロトコルの実装が方法を問わず形式検証されたのも初めてだと述べている。Signal の最高技術責任者 Ehren Kret 氏は、動いているコードを AI で Lean の定理に翻訳できたことを大きな前進と評価した。
使う側に残る入口
使う側の手間がなくなるわけではない。証明が守るのは、通信の途中でメッセージが盗み読まれたり、なりすまされたりしないことまでだ。乗っ取られた端末で画面を見られること、偽のリンクから別のサービスにパスワードを入れてしまうこと、会話のバックアップをどこに置くか。こうした入口は、どれも証明の外にある。端末の更新と、リンクを開く前の確認は、これまでどおり自分の仕事として残る。
それでも、道具を選ぶときの見方は 1 つ増える。そのアプリの安全は、誰が、何を前提に、どこまで確かめたのか。今回の成果物は GitHub で公開されていて、前提と対象外も読める形になっている。
次に見ておきたいのは、libsignal の次のリリースで同じ証明が回し直されるかどうかだ。今回の証明は v0.105.4 という 1 つの版に対するもので、コードが変われば確かめ直しが要る。DeepMind の code-verification リポジトリで、新しい版への対応とグループのメッセージへの拡張が出てくるかを追える。
ことば
- 形式検証 — プログラムが仕様どおりに動くことを、テストではなく数学の証明で確かめる手法。試していない入力でも成り立つと言えるのが強みで、証明を書く手間の大きさが広まらない理由だった。
- Lean — 数学の定理やプログラムの性質を書いて証明し、その正しさをコンピュータが検査する言語。検査を通った証明は書き手が AI でも同じ基準で扱えるため、AI と組み合わせる研究が進んでいる。
- トリプルラチェット — メッセージごとに鍵を更新し続ける仕組みに、量子計算機を見越した鍵交換を重ねた Signal の方式。端末が一時的に破られても、その後の会話で安全を取り戻せるように作られている。
毎日開くメッセージアプリを、あなたは「安全だと言われている」と「ここまで証明されている」のどちらで選んでいるだろうか？
