Signalの暗号、AIが書いた650万行の数学的証明をクリア

Signalの暗号化コードに、広く使われているソフトウェアとしてはほとんど例のない裏付けが加わった。約束どおりに動作することを示す数学的証明だ。AIエージェントのチームは、Signalプロトコルを動かすライブラリ「libsignal」を検証し、1対1のチャットで会話の秘密が守られ、相手が誰かを確認でき、鍵を盗まれた後も攻撃者を再び締め出せることを証明した。新たな欠陥は見つからなかった。

この成果はSignalの利用者だけにとどまらない意味を持つ。Signalのプロトコルはエンドツーエンド暗号化メッセージの世界標準であり、その派生版はWhatsApp、Messenger、Google Messagesのチャットも保護している。実際に公開されているコードをここまで深く検証する作業は、かつては非常に時間がかかり、ほとんど誰も試みなかった。この分野の大きな成果の一つである、検証済みOSカーネルの開発には、合計で20人年を要した。今回の作業は4週間で終わった。

Google DeepMindが開発したこのツールは、AlphaProof Codeと呼ばれる。まず人間の専門家とAIモデルが、Signalのセキュリティ目標を、数学的証明のために作られたプログラミング言語Leanで形式的な命題に置き換え、それぞれを人間が確認した。続いてGemini Carbonを基盤とする40〜80体のエージェントのチームが証明を作成。1台のマシン上で、1回あたり24〜72時間にわたって稼働した。できあがったLeanのコードは約650万行にのぼる。

この膨大なコードを人が信頼する必要はない。Leanのカーネルがすべての手順を検査し、成立しない証明は排除する。そのため、どのモデルが証明を書いたのか、途中で何度間違えたのかは結果に影響しない。一方、人が信頼しなければならない部分は、仕様書約2万6000行と、ARMプロセッサがコードを実行する仕組みを表すモデルに限られる。

証明の対象は、会話を守るSignalの機能だ。チャットを始めるためのハンドシェイク「PQXDH」と、メッセージごとに鍵を更新する「Triple Ratchet」が含まれ、将来の量子コンピューターに対抗することを目指す耐量子レイヤーも対象となった。実際には、スマートフォンの現在の鍵を盗まれても過去のメッセージは解読されず、双方が新しい鍵を交換すれば、窃盗犯は再びアクセスできなくなる。

システムが安全なコードと脆弱なコードを見分けられることを示すため、研究者たちは、すでに修正済みだったlibsignalの古いバグを2つ再び持ち込んだ。うち1つは、破棄すべき秘密鍵のコピーをライブラリが保持し続けるというものだった。どちらのケースでも、AlphaProof Codeはバグのあるビルドが安全でないことを、機械検証可能な証明によって示した。

ただし、限界も明確だ。証明の対象は1対1のセッションに限られ、DeepMindはグループメッセージングを今後の課題に挙げている。また、対象となるのはlibsignalのバージョン0.105.4を、標準のRustコンパイラでコンパイルし、小規模なテストプログラム内でARM Linux上で動かした場合だ。iPhone、Android、デスクトップ向けのSignalアプリ全体を検証したわけではない。低レベルの暗号処理部品は安全だと仮定されており、証明の対象ではない。人間が承認した仕様に誤りがあれば保証は弱まるうえ、WhatsAppなどのアプリはそれぞれ独自のプロトコル実装を使っているため、今回の成果が自動的に適用されるわけでもない。GoogleはWiredに対し、分析にかかった費用や、サービスとして販売する計画があるかどうかを明らかにしなかった。

Signalはこの成果を歓迎した。「AI主導のセキュリティ脅威が高まるなか、Signalプロトコルの実装を厳密に検証することで、コードがプライバシーを守るという保証に、これまで以上の自信を持てます」と、Signalの最高技術責任者エーレン・クレット（Ehren Kret）は声明で述べた。DeepMindの研究科学者、スワラット・チャウドゥリ（Swarat Chaudhuri）は、より慎重な見方を示した。Wiredに対し、この手法を「世界中のあらゆるソフトウェア」に広げられるようになるまでには、「まだ長い道のりがある」と語った。

Signalを使っている人が、何かをインストールしたり設定を変更したりする必要はない。この証明が対象にしているのは、すでにアプリに組み込まれているコードだ。

DeepMindは11月10日、技術論文とともにこの研究成果を発表し、仕様書と証明をGitHubでオープンソースとして公開した。同社はこのSignalプロジェクトを、4月に掲げた形式検証の大きな課題に向けた節目と位置づけ、次に検証を目指すシステムとして医療機器のファームウェアや電力網のソフトウェアを挙げている。

チャウドゥリは、作業のどこまでを機械に任せるべきかについても一線を引いた。「AIが目標を作り、AIが証明を生み出すような、雰囲気任せの世界は望んでいません」とWiredに語った。何を安全とみなすかを決めるのは、今も人間だ。AIが行うのは、それを証明することに限られる。

タグ: サイバーセキュリティ, Google DeepMind, AlphaProof Code, libsignal, Signal, エンドツーエンド暗号化