人が確認した仕様に基づき、エージェントがLeanの証明を生成しました。設計の抽象モデルから、実際の暗号コードの性質へ検証を進めています。 証明が保証するのは指定した性質と範囲です。仕様の妥当性、人のレビュー、変更時の再検証が導入時の焦点になります。 暗号の設計と実装の隔たりを検証する Google DeepMindは11月10日、AlphaProof CodeによるSignalの形式検証を発表しました。暗号プロトコルの設計が正しくても、実装の違いが問題になることがあります。今回の研究は、実際に使われるコードが指定した安全性を満たすかを数学的に確かめるものです。人の専門知識と複数のAIエージェントを組み合わせています。通常のテストが例を実行するのに対し、形式検証は定義された性質について証明を作ります。ただし、何を証明すべきかは別の判断です。原文でも人が仕様を確認したと説明しています。対象はSignalの中核となる暗号実装であり、アプリ全体のあらゆる不具合がなくなったという発表ではありません。 仕様を確認してから証明を機械で検査 研究者は複数のモデルと安全性の目標を数学的な仕様へ変換し、各仕様を人が確認しました。その後、Carbonを使うエージェントが600万行を超えるLeanの証明を生成しました。証明の検査はLeanが行い、エージェントは人が再確認すべき箇所を絞り込みます。原文ではコードベースの約1%がその対象になったと説明しています。検証には4週間を要しました。また、過去に修正された二つの不具合を隔離したコードへ戻し、安全でないことを機械検査可能な形で示しました。対象には端末が一時的に侵害された前後の保護などが含まれます。成果はセキュリティ担当者や暗号実装の開発者に関係します。形式検証の成果物も公開し、手法をコミュニティで確かめられるようにしています。 証明の範囲と保守の責任を明確にする 実務では証明の行数より、仕様が実際の脅威を表しているかが論点になります。生成された証明が正しくても、前提や対象外の部分が不十分なら保証の意味は限られると見られます。人が仕様を決める工程、機械が確認する工程、監査で判断する工程を分けて追える体制が必要になる可能性があります。製品更新でコードや依存先が変わる際には、証明の適用範囲も再確認することになります。原文は他の重要システムへの展開の可能性を示す一方、拡大には研究の継続が必要としています。そのため、医療機器や電力系統への適用が既に完了したとは読めません。既存のコードレビューや実行試験とどう接続するかを決め、証明が扱う性質を関係者へ説明できることが導入判断の材料になると見られます。対象外の機能や仮定を一覧にして共有できると、利用者が保証の意味を誤解しにくくなる可能性があります。証明の再利用にも、その前提の確認が伴います。