ディープマインドのAI、Signalの暗号コードを4週間で証明 数年の作業、人の確認は1％

　グーグル・ディープマインドは11月10日（米国時間）、AIエージェントを使い、メッセージアプリ「Signal」の暗号プロトコルのコードについて、主要なセキュリティ特性を数学的に証明したと発表した。新たに開発したエージェント型の検証フレームワーク「AlphaProof Code」を使った。

　対象は、SignalやGoogle Messagesなどで数十億人の私的な会話を守っているプロトコルの、実際に端末で動くコードだ。同社は、広く使われている暗号プロトコルの実装を、この深さで形式検証したのは、AIを使った例として初めてだと説明する。AIの有無を問わず、実装そのものが形式検証されたのも初めてだとしている。

　形式検証とは、コードが欠陥なく正しく動くことを数学的に証明する手法で、セキュリティ保証の最高水準とされる。ただ、手間がかかるため、従来は設計の段階にとどまることが多かった。

　手順は次のとおり。まず研究者が複数のAIモデルと協力して、Signalのセキュリティ目標を形式的な仕様に翻訳し、人間の専門家がそのすべてを確認した。その後、「Gemini Carbon」を搭載したエージェントが、数学の証明言語「Lean」で600万行超の証明を生成した。

　エージェントは証明を監査し、人間による再確認が必要な箇所を、コード全体の1％に絞り込んだ。残りはLeanが自動で検査する。端末が一時的に侵害された前後でもメッセージが保護される、といった特性を、端末上のコードの水準で証明したという。

　検証にかかったのは4週間。従来は専門家のチームが数年かけてきた作業だと、同社は説明する。

　検証手法の有効性を確かめるため、過去に修正済みの実際のバグ2件を、Signalのコードの隔離版に再び仕込んだ。いずれの場合も、システムはそのコードが脆弱だと示す、機械検査済みの証明を出したという。

　Signalの最高技術責任者（CTO）のEhren Kret氏は「従来の形式検証は範囲が小さかったが、今回の手法は大幅な拡張を可能にする。AIエージェントで実際のコードを有効なLeanの定理に翻訳できるのは大きな進歩だ」と述べた。

　ディープマインドは、検証に使った成果物をオープンソースで公開するとしている。技術論文も公開した。