AIエージェントがSignalの実装を数学的に証明
米Google DeepMindは11月10日（日本時間10日）、ソフトウエアの形式検証の新しい枠組み「AlphaProof Code」を発表した。形式検証は、プログラムが決めた性質を必ず満たすことを数学的に証明する手法で、ソフトウエアの安全性を保証する方法として最も厳しいとされる。同社の研究者の指導のもとでAIエージェントが、Signalプロトコルの実際のコードについて主要なセキュリティ特性を証明したという。Signalプロトコルは、メッセージアプリのSignalやGoogle Messagesの会話を守る暗号の仕組みだ。
同時に公開した技術論文によると、対象はSignalプロトコルの参照実装「libsignal」で、コンパイル後の機械語（AArch64）の水準で証明した。証明したのは、会話の始めに鍵を共有する耐量子暗号の手順「PQXDH」と、メッセージごとに鍵を更新する「Triple Ratchet」の2つの部分だ。性質は、過去の通信を後から解読されない前向き秘匿性、相手の認証、鍵が一時的に漏れた後に安全な状態へ戻る侵害後の安全性、鍵交換の秘匿性の4つ。
DeepMindはブログで、広く使われている暗号プロトコルをこの深さでAIを使って形式検証したのは初めてだと説明した。あわせて、このように広く使われているプロトコルの実装を形式検証したのは、AIの有無を問わず、どの方法でも初めてだとしている。論文は、広く使われている暗号プロトコル実装の改変していないコードに、プロトコル水準の安全性の保証をつないだ初めての証明だと書いている。
証明はAIが担い、仕様は人間が確認
ブログによると、AlphaProof Codeは複数のAIモデルを使い、何を証明するかを人間とAIで決め、証明そのものはAIエージェントの集団が進める。仕様（証明すべき性質を数式で書いたもの）は研究者が複数のモデルと協働して作り、人間の専門家がすべて確認した。証明は「Gemini Carbon」を使うエージェントが担い、証明を記述する言語「Lean」のコードを600万行超生成したという。エージェントは証明を監査し、人間が見直すべき箇所として示したのはコードベースの1%にとどまった。残りはLeanが自動で検査する。
論文は、仕様づくりにGemini 4 Carbonと米Anthropicの「Claude Opus 5.5」を使うエージェントを用い、証明はGemini 4 Carbonを使うエージェントの集団だけで作ったと書いている。著者は証明のコードを1行も書いていないという。一方で、作業の大半は証明よりも仕様づくりに費やしたとしている。
検証にかかった期間を、ブログは「わずか4週間」とし、従来は専門家のチームが何年もかけていた作業だと説明した。論文によると、この4週間は5人のチームによる作業で、2種類の証明を並行して進めた。暗号を理想的な部品とみなす「記号的なモデル」と、攻撃が成功する確率を計算の難しさで抑える「計算量的なモデル」だ。論文は過去の代表例として、OSの中核部分「seL4」の検証に20人年、Cコンパイラー「CompCert」に6人年かかったと紹介している。いずれも検証を前提に書かれたコードだという。
証明の規模は約650万行
論文によると、公開したリポジトリのLeanのコードは、コメントと空行を含めて約700万行ある。このうち証明は約650万行で、実行ファイルの動作についての証明が530万行、計算量的なモデルの証明が約86万行、記号的なモデルの証明が約35万行を占める。検証したlibsignalのコードは約560KB、AArch64の命令で約14万にのぼる。
証明の正しさはLeanが機械的に検査するため、結果を信頼するために人が正しさを確かめる必要があるのは仕様の側だと論文は説明する。要旨は、信頼する仕様とAArch64の意味論を合わせて約2万6000行としている。
対象はCLIで動かす実行ファイル、暗号の部品は前提扱い
ブログは、多くのプロトコル検証が設計の水準で止まるのに対し、今回は機器上で動くコードに至るまで証明したと説明した。機器が一時的に乗っ取られる前後でもメッセージを守る、といった性質が対象だという。
論文と公開リポジトリが示す検証の対象は、より限られている。改変していないlibsignal（v0.105.4）を小さなコマンドライン（CLI）のプログラムにつなぎ、標準のRustコンパイラー（rustc 1.98.1）でAArch64のLinux向け実行ファイルにした。証明はこの実行ファイルの機械語についてのものだ。SHA-256やAES、楕円曲線の演算などの低水準の暗号処理と、一部のメモリ操作やファイルの書き出しなどは、あらかじめ決めた条件どおりに動くものとして扱った。
論文は、扱ったのは1対1の会話に限られ、グループのメッセージは今後の課題だとしている。鍵の生成は検証しておらず、処理時間などから秘密を探るサイドチャネル攻撃も範囲外だ。
戻した既知の不具合2件を検出
DeepMindは、正しいコードと不具合のあるコードを見分けられるかを確かめるため、過去に修正済みの実際の不具合2件を、切り離した版のコードに戻した。どちらの場合も、不具合のある版が安全でないことを、機械が検査できる証明で示したという。
論文によると、2件はいずれもChevalらの研究者がlibsignalで見つけ、既に修正されたものだ。修正を取り消したコードをコンパイルし直し、その実行ファイルが安全性の定理を満たさないことをLeanで証明した。
Signalの最高技術責任者は「大きな進展」と評価
Signalの最高技術責任者（CTO）のEhren Kret氏は公式ブログに、AIエージェントを使って実際に動くコードを正しいLeanの定理に変換したことは大きな進展だとコメントを寄せた。AIを使ったセキュリティ上の脅威が増すなかで、Signalプロトコルが厳密に検証されたことで、コードがプライバシーの保証を果たしていることに一段と自信が持てるとしている。
DeepMindは形式検証の成果物を公開した。GitHubのリポジトリには記号的なモデルと計算量的なモデルの2つの証明が収められ、DeepMindのコードはApache 2.0で提供する。リポジトリに含むlibsignalのコードは、元のAGPL-3.0のライセンスのままだ。
同社は、医療機器のファームウエアや電力網のソフトウエアなど、ほかの重要なシステムの安全確保につなげるとしている。DeepMindは11月6日にも、AIエージェントが旧式の1024ビットRSAに2つの弱点を見つけたとする研究を公表していた。
