Google DeepMind 以 AI 四星期證明 Signal 加密保護

Google DeepMind 以 AI 證明 Signal 加密程式碼的關鍵保護成立

據 Google DeepMind 11 月 10 日發表的網誌，團隊以新框架 AlphaProof Code，用數學證明 Signal 協議參考程式庫 libsignal 的多項關鍵安全性質成立。Signal 協議是端對端加密通訊的通用標準，除 Signal 應用程式外，WhatsApp、Messenger 及 Google Messages 亦採用其變體。

Google DeepMind 研究副總裁 Pushmeet Kohli 同日在 X 表示，這是首次有廣泛使用的通訊協議，其實際運行的程式碼被形式驗證（以數學證明程式在任何情況下都符合指定要求）到這個深度，無論有否用上 AI。

驗證一直查到手機執行的機器碼

據團隊同日公開的技術論文，驗證對象是編譯後在 AArch64（Arm 架構）處理器上執行的機器碼，而非只停留在設計層面。論文指，現實中的漏洞常藏在設計與實作之間的落差。

證明涵蓋 Signal 的後量子握手程序 PQXDH 及 Triple Ratchet，確立前向保密、身份驗證，以及裝置一度被入侵後仍能恢復保護等性質。

放回舊漏洞，系統證明該版本不安全

Google DeepMind 網誌指，研究員把兩個早已修補的真實漏洞放回一個隔離的 Signal 程式碼版本，系統兩次都證明該版本不安全。據《WIRED》11 月 10 日報道，今次驗證的部分未有發現新漏洞，範圍亦不包括整個 Signal 手機應用程式。

Signal 技術總監 Ehren Kret 在聲明中表示，過往的形式驗證只集中於較小部分的程式碼，今次的方法令範圍大幅擴展。

過往同類工作以年計

論文指，形式驗證史上最成功的 seL4 微核心花了 20 人年完成，CompCert 編譯器則花了 6 人年。《WIRED》報道指，Google 拒絕透露今次驗證的成本，亦未有回應會否推出商業產品。Google DeepMind 研究科學家 Swarat Chaudhuri 向該刊表示，要把技術擴展到全世界的軟件，仍有很長的路要走。團隊表示會開源規格及驗證成果。

來源

• Introducing AlphaProof Code: a breakthrough in verifying complex software at depth（Google DeepMind）
• AlphaProof Code: Verifying Signal's Security at the Machine-Code Level（技術論文）
• A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure（WIRED）