AlphaProof Code：AIがSignalのコードの安全性を証明
· BehindLines 編集部
Google DeepMindの研究者らは、人工知能のエージェントを使って、メッセージングプロトコルSignalの土台となる実際のコードについて、複数の安全保証を証明したと述べています。DeepMindの投稿によると、広く使われている暗号プロトコルをAIがこれほど詳細な水準で形式検証したのは初めてとされ、The Registerは、これが研究者らの主張だと伝えています。
チームによる手法
このシステムはAlphaProof Codeと呼ばれます。DeepMindによると、まず人間の専門家と複数の言語モデルがSignalの安全目標を数学的な仕様に変換し、人がそれを一つずつ確認します。次にエージェントがLeanで証明を書きます。Leanは、検証器が推論を自動的に確かめる言語です。The Registerによると、エージェントは650万行のLeanを生成し、DeepMindは600万行超としています。その後、エージェントはこれらの証明を監査し、コードの約1%を人間が再確認すべき箇所として示しました。DeepMindは、これで大幅に時間が節約されたとしています。
何が証明されたか
DeepMindは、証明がプロトコルの理論的な設計だけでなく、コンパイル後のコードを対象にしていると強調します。たとえば、端末が一時的に侵害された前後でメッセージを守る性質が含まれます。The Registerは、前方秘匿性、認証、最初の鍵交換の秘匿性にも触れています。手法が正しいコードと不具合のあるコードを区別できるか確かめるため、チームは修正済みの実際の欠陥を2件、Signalのコードを隔離した版に戻しました。どちらの場合も、システムはその版が安全でないことを示す、機械で検証された証明を出しました。
認められている限界
The Registerは、結果は理論上のものだと説明しています。完全な暗号を前提としており、バイト列の計算上の秘匿性は保証しません。同サイトが引用する著者らによると、作業には5人で4週間かかり、「かなりの数のトークン」を使いました。著者らは、seL4マイクロカーネルの検証に20人年、CompCertコンパイラの開発に6年を要したことを挙げています。
Signalの最高技術責任者Ehren Kretは、DeepMindの投稿の中で、この手法は形式検証の対象範囲を大きく広げるものだと述べています。研究者の一人Swarat ChaudhuriはThe Registerに対し、次の難題は証明を作ることよりも、何を仕様として定めるかを決めることだと語りました。
なぜ重要か
DeepMindは、現実の脆弱性がプロトコルの設計と実装の間の隔たりに潜むことが多く、今回の証明はその隔たりを埋めようとするものだと述べています。同社は、医療機器のファームウェアや電力網のソフトウェアなど、他の重要なシステムを守る土台になると見ていますが、より大きな規模への展開にはさらなる研究が必要だとしています。