TopicBase
Google DeepMindは、人間の専門家とAIエージェントが協働する「AlphaProof Code」を開発し、Signalの暗号プロトコルの実装について、主要な安全性を数学的に証明しました。通信の設計に加え、端末で動くコンパイル済みコードまで検証し、作業を4週間で完了しました。
広く利用される暗号プロトコルの実装をこの深さで形式検証したのは、AIの有無を問わず初めてです。検証対象のSignalプロトコルは、メッセージアプリのSignalやGoogle Messagesで会話を保護する技術です。
人が仕様を確認し、AIが600万行超の証明を生成
形式検証とは、プログラムの動作が、機械で読める形にした仕様に従うことを数学的に証明する手法です。今回は、端末が一時的に侵害された場合でも、その前後のメッセージを保護する性質などを検証しました。
AlphaProof Codeは、複数の大規模言語モデルで検証作業を分担します。まず研究者がモデルと協力してSignalの安全性の目標を数学的な仕様へ変換し、専門家がすべての仕様を確認しました。
続いて、Gemini Carbonを使うエージェントが証明を作成し、証明用の言語・システムであるLeanのコードを600万行超生成しました。各証明はLeanが自動で検査します。
その後、エージェントが証明を監査し、人間による再確認が必要な箇所を抽出しました。その範囲はコードベースの1％で、専門家は判断を要する部分に確認作業を集中させました。
不具合のあるコードを区別できるかも試しています。過去に修正された実際のバグ2件を、隔離したSignalのコードに再導入したところ、どちらについても安全でないことを示す証明を生成し、機械で検査しました。
侵害の前後を守る鍵の更新
今回検証した端末侵害前後のメッセージ保護に関わるのが、Signalの「Double Ratchet」です。これは、共有した秘密鍵を出発点として、2者が暗号化メッセージをやり取りしながら鍵を更新するアルゴリズムです。
Double Ratchetはメッセージごとに新しい鍵を導出し、後の鍵から以前の鍵を計算できないようにします。ある時点で鍵を知られても過去のメッセージを守る前方秘匿性は、この一方向の更新に支えられています。
侵害後の保護には、別の更新も組み合わせます。双方が新しい公開鍵を交換し、Diffie-Hellmanという鍵共有の計算結果を使って、送信用と受信用の鍵の系列を更新します。
一時的な侵害で秘密鍵を知られても、その鍵が侵害されていない新しい鍵に置き換わると、攻撃者が知らない値を鍵の生成に取り込めます。この仕組みによって、その後のメッセージの安全性を回復させます。
暗号部品の検証からプロトコルの実装へ
既存の形式検証済み暗号ライブラリーには、HACL*やEverCryptがあります。これらは暗号処理の部品を提供し、メモリーの不正操作を防ぐ性質、数学的な仕様どおりに計算する性質、実行時間やメモリーへのアクセス先が秘密情報に依存しない性質などを検証します。
HACL*では、暗号規格を高水準の数学的仕様に置き換え、最適化した実装がその仕様と同じ計算結果を返すことを証明します。その実装をC言語のコードへ変換します。EverCryptは、C言語向けの実装とアセンブリー向けの実装を、共通の検証基盤で結び付けています。
今回のAlphaProof Codeは、Signalの中核となる暗号コードについて、専門家が定めたプロトコルの安全性を、実際に動く実装が満たすことを証明しました。暗号部品の計算が仕様と一致することに加え、通信で求める安全性と実装を結び付ける検証です。
暗号研究者のManuel Barbosa氏らは、期待する安全性を明確に仕様化し、その性質を実装が満たすことを独立に検証できる証拠を用意すべきだと提案しています。AlphaProof Codeでも、証明に先立って人間が安全性の目標と仕様を確認する工程を設けています。
実行時の情報漏えいも、暗号コードで扱う検証課題の一つです。タイミング・サイドチャネル攻撃は、秘密情報によって変わる処理時間を手掛かりに、秘密を推測します。対策となる定数時間プログラミングでは、処理の分岐やメモリーへのアクセス先が秘密情報に依存しないようにします。
この性質を検証する研究では、秘密情報がプログラム内のどこへ伝わるかを追跡する解析と、安全性の検証を組み合わせた「CT-Prover」が開発されています。HACL*やEverCryptでも、実行時間やメモリーへのアクセス先が秘密情報に依存しないことを、検証する性質として定めています。
検証成果物を公開し、ほかのシステムへの応用を研究
Signalの最高技術責任者であるEhren Kret氏は、従来は小さな範囲に限られていた形式検証を広げる手法だと評価しています。また、実運用のコードを有効なLeanの定理へ変換するAIエージェントの利用によって、コードのプライバシー保護への確信が高まると述べています。
Google DeepMindは、形式検証の成果物をコミュニティーが利用できるようオープンソースで公開します。同社は、医療機器のファームウェアや電力網のソフトウェアも応用先として挙げており、技術の適用規模を広げる研究を続ける方針です。
