AI生成約650萬行Lean證明程式，Google DeepMind驗證Signal一對一加密協定

Google DeepMind運用AI代理程式，對Signal加密協定的一對一對話程式碼進行數學驗證，確認其中的核心安全性質。研究歷時4週，驗證範圍不包括群組對話或整個Signal應用程式。

Google DeepMind於10日透過官方部落格、技術論文及證明資料公布「AlphaProof Code」研究結果。AlphaProof Code是一套形式驗證框架，AI代理程式依照人員訂定的安全條件，為實際程式碼撰寫證明。

形式驗證和輸入部分資料、測試是否出錯並不相同。研究人員會以數學方式描述程式碼必須遵守的條件，再證明程式執行結果符合這些條件。

研究團隊由人員決定要證明哪些安全性質，並撰寫、檢查規格。AI代理程式產生的證明必須通過Lean檢查器，不能只憑代理程式的判斷得出結論。

研究對象是以libsignal 0.105.4和SPQR 1.6.0建立的一對一對話用可執行檔。研究人員沒有修改程式庫，而是將其包裝成命令列工具，再編譯為AArch64機器碼進行分析。

驗證項目包括對話開始時協商加密金鑰的PQXDH，以及每則訊息都會更新金鑰的Triple Ratchet。Signal協定系列除了用於Signal，也應用於Google訊息、WhatsApp和Meta Messenger。

論文列出的證明目標包括前向保密性，確保過去訊息不會因後續金鑰外洩而曝光；入侵後安全性，檢驗金鑰外洩後能否恢復保護；以及對方身分驗證和初始連線的保密性。訊息機密性與真實性也納入驗證項目。

研究團隊分別以符號模型和計算模型呈現結果。符號模型將加密運算視為理想化對象；計算模型則假設攻擊者的計算能力有限，據此分析安全性質。

兩種模型的保障範圍並不相同。符號模型涵蓋量子攻擊者破解Diffie–Hellman金鑰交換時的初始連線保密性；計算模型則未以量子攻擊者為分析對象，也未證明SPQR在量子攻擊下的恢復安全性。

這項研究沒有停留在協定設計文件，而是將編譯後可執行檔的行為與規格逐一比對。不過，證明對象是研究團隊製作的命令列可執行檔，不是Signal應用程式本身。

研究結果仍建立在若干前提上，包括加密運算和部分程式庫功能會依照約定條件運作；Lean檢查器及AArch64語意模型也屬於信任基礎的一部分。

驗證範圍僅限兩名使用者之間的對話，不包括群組訊息、多部裝置的狀態或Signal應用程式本身。研究團隊在論文中將這些項目列為範圍限制。

為了確認這套方法能否找出缺陷，研究人員將兩個已被發現並修復的錯誤重新放入隔離程式碼。兩種情況都得到機器驗證結果，顯示安全性命題不成立；研究並未發現新的漏洞。

研究團隊由5人並行工作4週，產生約650萬行Lean證明程式碼。論文指出，證明所需的信任規格與AArch64語意模型約有2萬6000行。

Signal技術長艾倫·克雷特（Ehren Kret）表示：「過去的形式驗證只聚焦在程式碼的一小部分，Google DeepMind的方法大幅擴大了驗證範圍。」這番話肯定了研究將實作驗證擴展至更大範圍。

WIRED指出，這項研究是否解決AI輔助形式驗證在實務上的擴展性與成本問題，目前仍不明確。Google未公布分析成本，也未說明是否計畫推出商用驗證產品或服務。

論文將群組訊息、寄件者身分隱私功能及伺服器端協定列為後續驗證方向。Google DeepMind已公開規格與證明資料。