Google DeepMindは、AIエージェントを活用した形式検証フレームワーク「AlphaProof Code」を公開し、暗号化メッセンジャーSignalの中核ライブラリ「libsignal」を機械語レベルまで検証した。実際にコンパイルした実行コードの安全性を数学的に確認した点が特徴だ。

DeepMindは、Signalの暗号化プロトコルを支えるlibsignalを検証対象に選定した。12日付の台湾メディアIT Homeの報道によると、今回の検証では、手を加えていない実装コードそのものを対象とした。従来はプロトコル設計や改変版コードの検証が中心で、実運用に近い成果物まで確認することは限られていた。

形式検証は、プログラムが満たすべきセキュリティ要件を数学的に定義し、実際のコードがそれを満たしていることを証明する手法。今回、研究チームはRustで実装されたlibsignalをコマンドラインのテストプログラムと組み合わせ、AArch64 Linux向けの機械語にコンパイルした上で、その実行動作を解析した。

5人の研究者はAIエージェントを活用し、4週間で約650万行のLean証明コードを作成した。人間の研究者がセキュリティ要件をレビューして承認し、Gemini CarbonベースのAIエージェントが証明を生成、Leanの検証器が数学的な妥当性を確認する流れだ。

検証対象には、初期鍵を確立する「PQXDH」と、メッセージのやり取りに応じて鍵を更新する「トリプル・ラチェット」が含まれた。研究チームは、過去の通信内容を保護する前方秘匿性、メッセージ認証、一部の鍵漏えい後の安全性回復といった要件を検証したとしている。

誤りの検出能力も確認した。過去に修正済みだった脆弱性2件をテストプログラムに意図的に組み込んだところ、いずれも所定のセキュリティ要件に違反することを数学的に証明できたという。

もっとも、今回の結果はSignalアプリ全体の安全性を保証するものではない。対象は特定バージョンのlibsignalを組み込んだテストプログラムに限られ、グループチャットや複数端末環境、あらゆる量子計算機攻撃を網羅しているわけではない。

また、一部の暗号演算の安全性は前提条件に依存する。DeepMindは関連する証明とコードを公開しており、今後は医療機器や電力網など、重要システムのセキュリティ検証への応用可能性も示した。