Signalの暗号コード、AIが約4週間で数学的に検証　DeepMind「AlphaProof Code」

Signalや、Google Messagesのようなメッセージアプリを使っている人にとって、画面や操作が変わる発表ではありません。一方で、通信を守る暗号プログラムの安全性を確かめる手法が大きく進んだことを示しています。

AlphaProof Codeは、AIエージェント（自分で手順を進めるAI）に形式検証をさせる研究用の枠組みです。形式検証とは、コードが欠陥なく動くことを数学的に証明する方法を指します。Google DeepMindの公式ブログによると、対象はSignalプロトコルの実際のコードです。

設計ではなく実際のコードを証明

暗号プロトコル（通信を守る決まり事）は、ネットバンキングやウェブ閲覧など、ほぼすべてのデジタル通信を支えています。1つの欠陥で、多くの人が一度に危険にさらされかねません。

そのため、設計段階の検証は長年行われてきました。ただ、実際の脆弱性は設計と実装の間のすき間に潜みがちです。今回のAIエージェントは、端末で動く実際のコードが主要な安全性を満たすことを証明しました。DeepMindはそう説明しています。

証明した性質の例は、端末が一時的に乗っ取られた前後でも、メッセージが保護されることです。DeepMindは、広く使われる暗号プロトコルの実装を形式検証したのは、AIの有無を問わず初めてだとしています。

人が決め、AIが証明する分業

AlphaProof Codeは複数の大規模言語モデルを使う枠組みで、研究チームのように作業を分けます。

• 人の専門家とAIが、Signalの安全性の目標を数学的な仕様に翻訳する。人がすべての仕様を確認した
• Gemini Carbonを使うエージェントが証明を作る。Leanのコードは600万行を超えた
• エージェントが証明を監査し、人が再確認すべき箇所を示す。範囲はコード全体の1%

Leanは、コードの正しさを数学的に確かめる言語です。残りの部分はLeanが自動で検査するので、専門家は人の判断が要る場所に集中できました。

Gemini Carbonについては、Googleが10月に公開した最上位モデルです（Gemini 4 Carbon）。

4週間で完了、過去のバグも見抜く

DeepMindによると、検証にかかったのは約4週間でした。従来は専門家チームが数年かけてきた作業だと説明しています。

システムが正しいコードと欠陥のあるコードを区別できるかも試されました。過去に修正された実在のバグ2件を、隔離したSignalのコードに戻しました。どちらも、機械で検査できる形で安全でないと証明されたといいます。

Signalの最高技術責任者（CTO）Ehren Kret氏は、従来の検証は範囲が限られていたと述べました。AIエージェントで実際のコードをLeanの定理に変換できる点を「大きな進歩」と評価しています。

医療機器や電力網への展開を想定

DeepMindは、この成果が企業・政府・重要インフラに高い水準の安全保証をもたらすと説明します。Signalの中核暗号の検証は、医療機器のファームウェアや電力網のソフトなど、ほかの重要システムを守る土台になるとしています。

自動防御エージェントの「CodeMender」と組み合わせれば、サイバー攻撃の速さと規模に対抗できる可能性も挙げました。ただし、技術の拡大には引き続き研究が必要だと述べています。

開発者・セキュリティ担当者へ

DeepMindは、形式検証の成果物（検証に使ったコードや証明）をオープンソースで公開しています。技術論文も公開されており、自社の暗号実装や重要ソフトの検証を考える担当者は、検証の範囲や前提を確認できます。