Google DeepMindの研究者らは、エージェント型AIを用いて、Signalプロトコルの主要な暗号保証を数学的に証明した。 概念実証プロジェクトとして4週間で実施されたこの研究は、「AlphaProof Code」と名付けられた新しいAIフレームワークに基づいている。
Signalプロトコルは、Signalアプリの通信を暗号化するだけでなく、情報源によればGoogle MessagesやWhatsAppの通信も暗号化している。本記事において、この証明は世界中の膨大なメッセージを保護するこの暗号技術に対する新たな独立した検証であり、Google DeepMindの形式検証能力を示すものでもある。
形式検証とは、ソフトウェアが予定通りに動作し、重大な欠陥がないことを数学を用いて確認する手法である。その支持者らは長年、これをソフトウェアセキュリティの「聖杯」と見なしてきた。しかし、大規模な適用や、大量のコードに対する有効性については不確実性が残る。
ターゲットを絞った分析
AI以前の時代には、ソフトウェアの特性を記述し、それを数式に変換し、証明を構築するには膨大な時間を要した。情報源によれば、エージェント型AIはこの最終段階の時間を大幅に短縮できる。ただし、分析の範囲は限定的であり、例えばSignalモバイルアプリ全体の形式検証は行われていない。
調査対象となったプロトコルの部分では、研究者らは新たな脆弱性を発見しなかった。一方、長年にわたって修正済みの既知の脆弱性を含むSignalの古いバージョンにAlphaProof Codeを適用したところ、ツールはそれらを正しく特定し、そのバージョンではプロトコルが形式的に検証できないことを示した。研究者らは、Signalプロトコル分析のために作成した仕様と証明を公開し、他の形式検証作業を容易にする。
このプロジェクトの迅速さは、DeepMindの研究者が指摘するように、Signal Foundationによるこの分野での先行研究に一部依っている。「従来の形式検証はコードのより小さな部分を対象としていたが、Google DeepMindのアプローチは大幅な拡張を可能にする」と、SignalのCTOであるエーレン・クレットは声明で述べている。「AI関連のセキュリティ脅威が増加する中、Signalプロトコルの実装を厳密に検証することで、我々のコードが提供する機密性保証に対する信頼がさらに高まる」。
コストと規模の問題
Google Cloudのサイエンス部門責任者兼DeepMindリサーチ担当バイスプレジデントのプシュミート・コーリによれば、ハイステークスな状況で使用される重要なサービスにおいて、各コードベースとソフトウェアサプライチェーン全体を形式的に検証できるようになることは大きな進歩だという。「これらの実装の正当性を検証できるなら、安心できる。銀行や、保証に依存しバグを懸念する他のあらゆる企業が、今や『私はこれらの特性を証明できる』と言えるようになることを想像してほしい」と彼は語る。
残る課題は、AIによる自動化された形式検証が、現実的に、かつ合理的なコストでスケールする能力を本当に持つかどうかであり、これは技術業界全体に開かれた問題である。DeepMindは研究プロジェクトの一環としてSignalの分析を無償で実施し、Googleはそのコストを明らかにしなかった。同社はまた、形式検証の製品やサービスの商用化を計画しているかどうかも明らかにしていない。
研究者らは、彼らの重要な進展の一部は、DeepMindの研究科学者スワラト・チャウドゥリの言葉を借りれば「人間とAIの協調プロセス」にあると評価している。このプロセスにより、エージェントはほぼすべての段階で貢献し自己修正を行いながら、重要なタイミングで人間の意見と検証を求めることができる。「AIが目標を設定し、AIが証明を生成し、AI自身が書いたテストを通過するだけの世界は望んでいない。その中間地点が存在する」
