米Google DeepMindは、通信アプリ「Signal」の暗号プロトコルを実装したコードについて、AIを使った数学的な安全性検証に成功したと発表した。従来は専門家チームが数年を要する作業を4週間で実施し、人による追加確認の対象をコード全体の1％に絞った。
600万行超の証明を生成、実装コードまで検証
2026年11月10日の発表によると、DeepMindは、独自のAIエージェントと人間の専門家の組み合わせによって秘匿性の高い通信アプリSignalのプロトコルの基盤となる実コードの主要なセキュリティ特性について検証した。結果、プロトコルは理論レベルだけでなく、実際に仕様を満たすものであることを確認したという。
今回用いられた「AlphaProof Code」は、複数の大規模言語モデルを組み合わせたAIエージェント基盤だ。人間の専門家が何を証明するかを決め、AIが証明を進める形で、形式検証（※）の作業を分担する。
まず研究者がAIモデルと協力し、Signalの安全性要件を数学的な仕様に変換した。仕様はすべて人間が確認し、その後、Gemini Carbonを基盤とするエージェントが600万行超のLeanコードを生成した。
生成された証明はLeanによって機械的に確認し、そのうえでAIが注意を促したコード全体の1％を専門家が重点的に調べた。
従来の暗号プロトコル検証は設計段階にとどまる例が多かったが、今回は端末で実行されるコードの水準まで検証した。対象には端末が一時的に侵害されても、その前後のメッセージを保護する性質などが含まれる。
Google DeepMindによると、広く利用される暗号プロトコルの実装をこの深さで形式検証したのは、AIの使用有無を問わず初めてだという。
さらに、過去に修正された実際の不具合2件を隔離したコードに再導入したところ、どちらも安全でないことを機械的に証明できた。研究成果に関する検証用資料はオープンソースで公開するとしている。
※形式検証：ソフトウェアやシステムが定められた仕様を満たすことを、数学的な手法で証明する技術。テストによって個別の動作を確認する方法とは異なり、論理的な証明を通じて指定された条件下での正しさを保証する。
検証の省力化に期待、適用範囲の拡大は課題
この成果の意義は、暗号技術の設計と実際のプログラムの間に生じるずれを、数学的な根拠をもって調べられる点にある。設計上は安全でも実装に不具合が残れば、利用者の通信が危険にさらされる可能性がある。AIが膨大な証明作業を担えば、高度な検証を限られた専門家だけに依存しない体制につながるだろう。
一方、数学的な証明が保証するのは、あらかじめ定めた仕様に対する適合性だ。仕様自体が不十分なら、想定していない攻撃や運用上の問題まで排除できるわけではない。今回も安全性要件の定義と確認には専門家が関与しており、人間の判断が不要になったとは言えない。
また、Signalの中核暗号コードでの成功を、他の複雑なシステムにそのまま適用できるとも限らない。今後は検証対象を広げる研究とともに、仕様の妥当性をどう評価し続けるかが普及の鍵となりそうだ。
関連記事:
OpenAI、Linuxカーネルのローカル権限昇格脆弱性948件をAIで検証 パッチ候補を自動生成
Anthropic、AI応答検証システム「FlashProve」公開 zkSNARKで指定モデルによる生成を証明
