11月10日、Pushmeet KohliとSwarat Chaudhuri（プシュミート・コーリとスワラット・チョードゥリ）が「Formal Verification of Signal's Protocol with Gemini」と題した記事を公開した。Google DeepMindの研究チームがAIエージェントフレームワーク「AlphaProof Code」を用いてSignalプロトコルの暗号実装コードの形式検証に成功したことが報告されている。
「設計レベル」ではなく「実装コード」を検証した、という意味
Signalプロトコルは、SignalアプリやGoogle Messagesをはじめ、数十億人のプライベートな会話を守る暗号技術の基盤だ。その安全性を数学的に証明する「形式検証（Formal Verification）」は、セキュリティ保証の最高水準とされているが、従来は膨大な手作業を要するため、現実の大規模なコードベースへの適用は困難だった。
従来の形式検証ツールとしては、プロトコルの設計レベルの安全性解析に用いられるProVerifやTamarinが知られている。これらは抽象的なプロトコルモデルに対して強力な解析能力を持つ一方、実際のデバイス上で動作するコードの検証には直接対応していない。設計と実装の「隙間」には現実の脆弱性が潜むことが多く、実装コードそのものを検証することは長年の未解決課題だった。
さらに言えば、既存の形式検証の多くはプロトコルの「設計」レベルに留まっていた。実際にデバイス上で動くコードが設計通りに実装されているかどうかは、別の問題だ。
今回、Google DeepMindが達成したのは、Signalの実装コードそのものについて形式検証を行うことである。これはAIを用いた手法であるかどうかを問わず、広く実運用されているプロトコルの実装レベルでの形式検証としては、史上初だとしている。
AlphaProof Codeの仕組み
今回の成果を支えたのは、AlphaProof Codeと呼ばれる新しいエージェント型フレームワークだ。複数のLLMを組み合わせ、形式検証の作業を「研究チームが分担するように」分割して進める。
具体的な流れは以下のとおりだ：
- 仕様の形式化：研究者がAIと協働し、Signalのセキュリティ目標を数学的な仕様に変換する。すべての仕様は人間の専門家がレビューする。
- 証明の生成：Geminiを搭載したエージェント群が証明を生成する。出力されたのは**Lean（リーン）というプログラム検証言語で書かれた600万行超のコード**だ。Leanは型理論に基づく定理証明支援システムであり、証明の正確性を機械的に自動チェックできる点が特徴だ。近年、数学や形式検証の分野でAIとの親和性の高さから注目を集めている。
- 人間によるレビューの絞り込み：エージェントが証明を監査し、人間の再確認が必要な箇所をピックアップする。その量は**全コードの1%**にとどまり、専門家は本当に判断が必要な部分に集中できる。
検証対象となったセキュリティ性質には、「デバイスが一時的に侵害された前後もメッセージが保護される」といった項目が含まれる。
4週間で完了——従来なら数年かかる作業
特筆すべきは速度だ。今回の検証プロセスはわずか4週間で完了した。同等の作業を専門家チームが手作業で行えば、数年単位の時間がかかるとされてきた。
また、AlphaProof Codeが「正しいコードと誤ったコードを区別できるか」を確認するため、過去に実際に発見・修正された2つのバグをSignalのコードに意図的に再導入して検証した。いずれのケースでも、システムはバグを含むバージョンが安全でないことを機械検証済みの証明として出力した。
今後の展開とオープンソース化
今回のSignal暗号実装の検証は、医療機器のファームウェアや電力グリッドのソフトウェアなど、他の重要システムの検証へのステップとして位置付けられている。
Google DeepMindはAlphaProof Codeを、形式検証を現代のサイバー脅威の速度・規模に対抗する実用的な手段として発展させていく方針だ。
形式検証の成果物はオープンソースとして公開されており、コミュニティでの活用が可能だとしている。
詳細はFormal Verification of Signal's Protocol with Geminiを参照していただきたい。
