Google DeepMindのAlphaProof Code、Signalの暗号プロトコルを形式的に検証

Google DeepMindは、長らく重大な難題とされてきたソフトウェアセキュリティの節目に到達したと発表しました。同社の研究者はAIエージェントを導き、SignalおよびGoogle Messagesなどのアプリで数十億件のプライベートな会話を保護する技術であるSignalプロトコルの基盤となる実際のコードについて、送信者と指定された受信者だけがメッセージを読めるようエンドツーエンドで暗号化する主要なセキュリティ特性を数学的に証明させました。この発表は、Pushmeet Kohli氏とSwarat Chaudhuri氏によりGoogle DeepMindブログで公開されました。

この成果は、人間の専門知識とAIエージェントを組み合わせ、前例のない深さでの形式的検証を実現する新しいエージェント型フレームワーク「AlphaProof Code」によって達成されました。形式的検証とは、コードが欠陥なしに正しく動作することを数学的に証明することであり、セキュリティ保証の最も高い水準ですが、困難で多くの場合労働集約的です。従来のテストはプログラムの動作をサンプリングするのに対し、形式的証明はあらゆる実行経路における欠陥を排除します。これは保証コストが非常に高いため、広く展開されているソフトウェアに適用されることはほとんどありませんでした。

同社によると、この成果はAIがこのレベルの深さで広く展開されている暗号プロトコルを形式的に検証した初めての事例であり、またこの種の広く展開されているプロトコルの実装が、AIの有無を問わずいかなる手法によっても形式的に検証された初めての事例でもあります。

Google DeepMindがSignalを検証した方法

AlphaProof Codeは、研究チームと同様に形式的検証の作業を分割するマルチLLMエージェント型フレームワークです。人間の専門家がAIと協力して証明すべき内容を決定し、複数のAIエージェントが証明を実行します。

まず、Google DeepMindの研究者は複数のモデルと協力して、Signalのセキュリティ目標を形式的な数学的仕様に変換し、人間の専門家がすべてをレビューしました。その後、Gemini Carbonを基盤とするエージェントが証明を行い、コードの正確性を数学的に証明するコンピュータ言語であるLeanで600万行を超えるコードを生成しました。

次に、エージェントは証明を監査し、人間による再確認が必要な箇所を特定しました。これはコードベースのわずか1%で、同社はこれを大幅な時間削減としています。残りはLeanが自動的にチェックするため、専門家は人間の判断が最も重要な箇所にレビューを集中できました。

実行されるコードに至るまでセキュリティを証明

暗号プロトコルは、オンラインバンキングからウェブブラウジングまで、ほぼすべてのデジタル通信を支えており、単一の欠陥が一瞬で数百万人を危険にさらす可能性があります。そのため専門家は数十年にわたり形式的な分析を行ってきましたが、ほとんどのプロトコル検証は設計レベルで止まっていました。

Google DeepMindのエージェントはさらに進んで、コンパイルされたコードが、デバイスが一時的に侵害される前後でメッセージが保護され続けることなど、暗号学者が前方秘匿性および侵害後セキュリティとして知る主要なセキュリティ特性を満たすことを、デバイス上で実行される正確なコードに至るまで証明しました。現実世界の脆弱性は設計と実装の間のギャップに潜んでいることが多く、このギャップを埋めることで証明ははるかに複雑になります。

この複雑さにもかかわらず、検証プロセスはわずか4週間で完了しました。同社によれば、これは従来専門家チームに数年を要する作業であり、Signalの中核的な暗号コードが研究者らが指定したセキュリティ保護を実現していることが立証されました。

AlphaProof Codeが正しいコードとバグのあるコードを区別できることを確認するため、チームはSignalのコードの隔離バージョンに、過去に修正済みの2つの実際のバグを再導入しました。いずれの場合も、システムはバグのあるバージョンが安全でないことを示す機械検証済みの証明を生成しました。欠陥のあるコードを検出できない検証器は誤った安心感を与えるため、この確認は重要です。

AlphaProof Codeでは、AIエージェントがユーザーの仕様作成を支援し、その後実装が仕様を満たしていることを自律的に証明します。すべての証明はLeanによってチェックされ、エージェントの作業が検証されます。

Signalの反応

「これまでの形式的検証はコードのより小さな部分に焦点を当てたものでしたが、Google DeepMindのアプローチは大幅な拡張を可能にします」と、Signalの最高技術責任者Ehren Kret氏は述べました。「AIエージェントを使用して実際のコードを有効なLean定理に変換することは大きなブレークスルーです。AIを利用したセキュリティ脅威が拡大する中、Signalプロトコルの実装を厳密に検証することで、当社のコードのプライバシー保証への確信がさらに高まりました」

セキュリティの未来

Google DeepMindは、この長年の難題の達成は、AIが企業、政府、重要インフラに最高水準のセキュリティ保証をもたらし、エージェント主導のサイバー脅威からの防御に役立つことを示していると主張しています。同社によれば、Signalの中核的な暗号技術の検証は、医療機器のファームウェアから電力網ソフトウェアまで、他の重要なシステムの保護への基礎を築くものです。

これらの手法をスケールさせるには継続的な研究が必要です。CodeMenderのような自動防御エージェントと組み合わせることで、形式的検証は現代のサイバー脅威の速度と規模に対抗し、その保護機能が機能することの数学的証明を伴うソフトウェアの創出に貢献できます。

Google DeepMindは、形式的検証の成果物をコミュニティ向けにオープンソースとして公開しており、google-deepmind.github.io/code-verificationでホストされています。完全な技術論文はPDFで入手できます。セキュリティ研究コミュニティにとって、この公開により機械検証済みの証明と手法を直接検証することが可能となります。そして、この深さでの検証がSignalを超えて、同社が挙げる医療、産業、インフラシステムにどこまで広がるかが、今後注目すべき展開です。

謝辞

この研究は、Swarat Chaudhuri、Andrew Ferraiuolo、Anton Kovsharov、Tej Chajed、Sam Schlesinger、Karn Seth、Jonathan Katz、Charles Sutton、Pushmeet Kohliによって開発されました。

チームは、コードのオープンソース化に協力したEric Wieser氏、プログラム管理の支援をしたOwen Jones氏、有益な議論を提供したMartín Abadi、Christopher Henson、Katerina Hristova、Henryk Michalewski、Jonathan Protzenko、George Tsoukalasの各氏に感謝しています。また、手法へのフィードバックを提供したSignalのRolfe Schmidt、Michael Rosenberg、Ehren Kretの各氏、およびプロジェクトを支援したTulsee Doshi、Four Flynn、Kate Olszewska、Alicia Huang、Andy Liu、Benoit Schillings、Raluca Ada Popa、Melvin Johnson、Koray Kavukcuoglu、Demis Hassabis、Sundar Pichaiの各氏にも感謝しています。