Google DeepMindの研究者は、AIシステムを使ってメッセージアプリSignalのプロトコルに関する重要なセキュリティ特性を数学的に証明できることを示した。チームはAlphaProof Codeと呼ばれる新たな枠組みを用い、複数の暗号学的な保証を形式検証した。研究にかかった期間は約4週間で、商用製品の開発ではなく研究プロジェクトとして行われた。検証した範囲では新たなバグは見つからなかった一方、プロトコルの旧バージョンを調べた際には、すでに修正済みの過去の脆弱性をAIが正しく検出した。
形式検証とは、ソフトウェアが意図どおりに動作することを数学的に確認し、潜在的な脆弱性が入り込む余地をなくす手法だ。従来は専門家が詳細な仕様を書き、それを数式に置き換えたうえで証明を組み立てる必要があり、手間のかかる作業に何カ月もかかることがあった。自ら小さな目標を立てて達成を目指す「エージェント型AI」に作業の大部分を任せることで、DeepMindは期間を数週間に短縮した。研究者によると、重要な段階では依然として人間の監督が必要だが、AIは自ら証明を提案し、誤りを修正することもできた。
Signalの最高技術責任者（CTO）、Ehren Kret氏は、従来の検証では対象がコードの小さな断片に限られていたと指摘した。DeepMindの手法によって検証できる範囲を「大幅に拡大」できると同氏は述べた。チームは、他の研究グループが活用できるよう、作成した仕様と証明を公開する。成果は有望だが、アプリ全体やソフトウェアのサプライチェーン全体に適用するには、なお課題があるとDeepMindは警告している。また、AIを活用した検証にかかる費用は明らかにされていない。
注目される理由
AIが暗号プロトコルの安全性を確実に証明できるようになれば、Signal、Google Messages、WhatsAppなどを使う日常のユーザーは、メッセージのプライバシーが守られているという確信をより強く持てるようになる可能性がある。銀行、医療機関、ジャーナリストなど、暗号化通信に依存する組織にとっては、将来的に、自社ソフトウェアに重大な欠陥がないことを法的に検証可能な形で保証する手段になるかもしれない。
なぜ重要か
一般ユーザーにとって今回の成果は、チャットを守る暗号化が新たな数学的検証によって裏付けられ、隠れたバグの可能性が低くなることを意味する。プライバシー規制への準拠を証明する必要がある企業にとっては、AIを活用した検証が、長時間の手作業による監査に頼らず安全性を示す新たな手段になる可能性がある。
