ディープマインドのAI、Signal暗号コードを機械語レベルで証明

グーグル・ディープマインドは11月10日（現地時間）、Geminiを基盤とするAIエージェントを使い、暗号化メッセンジャー「Signal（シグナル）」の中核コードが主要な安全性を満たすことを、機械で検証できる数学的証明で示したと発表した。対象はSignalプロトコルの参照実装「libsignal」をコンパイルした機械語コードである。同社は、広く使われるこの種のプロトコルの実装を形式検証したのは、AIの有無を問わず初めてだとしている。

要点

• ディープマインドの新フレームワーク「AlphaProof Code」が、Signalのコンパイル済みコードについて約650万行のLean証明を生成した。
• 何を証明するかは人間が決めて承認し、証明はエージェントが書いた。検証期間は4週間である。
• 証明の対象は1対1の会話に限られ、グループメッセージやSignalアプリ全体は含まれない。

AlphaProof CodeがSignalで検証した内容

技術論文によると、対象はlibsignal v0.105.4だ。研究チームはコードに手を加えず、標準のRustコンパイラーでAArch64向けLinux機械語にビルドした。証明は耐量子のPQXDHハンドシェイクとトリプルラチェットを扱い、前方秘匿性、認証、侵害後の安全性、ハンドシェイクの秘匿性を示した。

これまでのSignal検証研究の多くは、抽象モデルや検証用に書き直したコードを対象としていた。ディープマインドは、現実の脆弱性は設計と実装の隙間に潜むことが多いため、実行ファイルそのものを証明の対象にしたと説明している。

AIエージェントの役割分担

ディープマインドのブログによると、研究者はまず複数のモデルと協力してSignalの安全性目標を形式仕様に落とし込み、専門家がすべての仕様を確認した。その後、Gemini Carbonを搭載したエージェントが、カーネルが全ステップを検査する証明言語Leanで証明を書いた。

論文によれば、証明チームは通常40～80のエージェントで構成され、1台のマシンで24～72時間稼働した。「ゲートキーパー」役のエージェントは、人間が承認した仕様の控えとLeanカーネルが照合した証明だけを受け入れた。エージェントが人間の再確認を求めた部分は、コードベースの約1％だった。

読者が信頼して受け入れる必要がある部分は約2万6000行で、仕様が約1万8000行、AArch64の意味論が約8000行である。意味論モデルは467命令と31のシステムコールをカバーする。

過去のSignalのバグで証明を試験

仕様が実際の誤りを捉えられるかを確かめるため、研究チームは修正済みのlibsignalのバグ2件を隔離したビルドに戻した。いずれの場合も、バグを含む実行ファイルが安全性の定理に違反することを示す機械検証済みの証明が得られた。

Signalの最高技術責任者（CTO）エーレン・クレット氏は、ディープマインドの発表の中で「AIエージェントを使って実際のコードを有効なLeanの定理に変換したことは大きな飛躍だ」と述べた。

形式検証はなぜ高コストだったか

形式検証は長年、人手の負担が壁となってきた。論文によると、seL4マイクロカーネルの検証には20人年、Cコンパイラー「CompCert」には6人年を要した。どちらも当初から検証を前提に書かれたコードであり、libsignalのような実運用コードとは条件が異なる。

AI Newswayが11月9日に報じたマイクロソフト・リサーチの「PDD Kit」のように、AIでコードを証明する試みはこの秋相次いでいる。

今回の証明の限界

保証は、承認済みの仕様、Leanカーネル、機械語の意味論、そして信頼された契約として扱う暗号プリミティブの仮定の上に成り立つ。意味論はスレッド、シグナル、動的リンクをモデル化していない。論文を検討した米メディアUnite.AIは、鍵生成、サイドチャネル、複数端末の状態も対象外だと指摘している。

今後の見通し

ディープマインドは仕様と証明をGitHubで公開し、外部の専門家が再確認できるようにした。研究チームはグループメッセージを今後の課題に挙げ、医療機器のファームウェアや電力網のソフトウェアなどへの応用も見込んでいる。

よくある質問

Signalにバグが一つもないということか。 そうではない。特定のビルドが、明示された仮定の下で定められた安全性を満たすことを証明したものであり、仕様の外側は対象外である。

Signalの利用者がすべきことはあるか。 ない。既存のコードを検証した研究であり、アプリが変わるわけではない。

第三者も証明を確認できるか。 できる。ディープマインドはLeanのコードと再ビルド・検証の手順を公開している。

参考資料

• Formal Verification of Signal's Protocol with Gemini — Google DeepMind（2026年11月10日）
• AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — Google DeepMind・Google（2026年11月10日）
• GitHub - google-deepmind/code-verification: Verifying Signal's security at the machine-code level — Google DeepMind
• Google DeepMind Uses AI Agents to Verify Signal's Core Machine Code — Unite.AI（2026年11月10日）