AlphaProof CodeがSignalの暗号プロトコルを形式検証する

Google DeepMindの研究チームはこのたび、新規エージェント型フレームワークAlphaProof Codeを使い、Signalプロトコルの実際のコア暗号実装コードの主要セキュリティ特性を数学的に証明した。Signalは数十億件のメッセージを保護する基盤技術で、実装コードの形式検証は長年の課題だった。人間専門家とAIが分担し、セキュリティ目標をLean仕様に翻訳して全件を人間審査し、Gemini Carbonエージェントが600万行超の証明を生成した。監査エージェントにより人間再確認箇所は全体の1％に抑えられ、残りはLeanが自動検証した。設計と実装のギャップを越え、端末一時侵害前後の保護まで実コードで保証し、作業を通常数年から4週間に短縮。修正済みバグ2種を再導入した検証でも危険性を機械検証で確認した。広く利用される暗号プロトコルの実装をAIで深層形式検証した初の事例であり、オンラインバンキングなどデジタル通信の脆弱性リスク低減に貢献する。研究はSwarat ChaudhuriやPushmeet Kohliらが主導した。