Google DeepMind 的 AlphaProof Code 以形式化方法驗證 Signal 加密協定

Google DeepMind 表示，其在軟體安全領域達成了一項長期被視為重大挑戰的里程碑：該公司的研究人員引導 AI 代理，以數學方式證明 Signal 協定底層實際程式碼的關鍵安全特性。Signal 協定透過端對端加密訊息，使只有發送者與預期接收者能夠閱讀內容，是保護 Signal 與 Google Messages 等應用中數十億私人對話的技術。這項公告由 Pushmeet Kohli 與 Swarat Chaudhuri 發表於 Google DeepMind 部落格。

這項成果是透過 AlphaProof Code 達成的——這是一個新穎的代理式框架，結合人類專業知識與 AI 代理，可進行前所未有的深度形式化驗證。形式化驗證——即以數學方式證明程式碼無缺陷地正確運行——是安全保證的最高標準，但過程困難且往往耗費大量人力。傳統測試僅對程式的行為進行抽樣；而形式化證明則排除所有可能執行路徑上的缺陷——這種等級的保證成本極高，因此鮮少應用於廣泛部署的軟體。

據該公司表示，這項工作是 AI 首次在此深度上對廣泛部署的加密協定進行形式化驗證，也是此類廣泛部署協定的實作首次以任何方法——無論是否使用 AI——獲得形式化驗證。

Google DeepMind 如何驗證 Signal

AlphaProof Code 是一個多 LLM 代理式框架，其分工方式如同研究團隊：由人類專家與 AI 共同決定要證明的目標，再由一組 AI 代理執行證明。

首先，Google DeepMind 的研究人員與多種模型協作，將 Signal 的安全目標轉換為正式的數學規格，每一項都經人類專家審查。接著，由 Gemini Carbon 驅動的代理執行證明，生成了超過六百萬行的 Lean 程式碼——Lean 是一種以數學方式證明程式碼正確性的電腦語言。

代理隨後對證明進行審計，並標記出需要人類再次檢視的部分——僅佔程式碼庫的百分之一，該公司稱此為巨大的時間節省。由於 Lean 會自動檢查其餘部分，專家得以將審查重心放在最需要人類判斷的地方。

將安全證明深入至實際運行的程式碼

加密協定支撐著幾乎所有的數位通訊，從網路銀行到網頁瀏覽，單一缺陷就可能同時讓數百萬人暴露於風險之中。這正是專家們數十年來持續對其進行形式化分析的原因，但大多數協定驗證僅止於設計層面。

Google DeepMind 的代理更進一步，證明編譯後的程式碼在裝置上實際執行的層級上，仍然滿足關鍵安全特性——例如在裝置暫時遭入侵之前與之後都能保護訊息安全，密碼學家所稱的前向保密與入侵後安全。現實世界的漏洞往往隱藏在設計與實作之間的落差中，而彌合這一落差使這些證明的複雜度大幅提升。

即便如此複雜，整個驗證過程僅耗時四週——據該公司表示，此類任務過去通常需要專家團隊耗費數年——證實了 Signal 的核心加密程式碼確實具備研究人員所指定的安全防護。

為了確認 AlphaProof Code 能區分正確與有缺陷的程式碼，團隊將兩個先前已修復的真實漏洞重新植入 Signal 程式碼的隔離版本中。在這兩種情況下，系統都產生了經機器檢驗的證明，證明該缺陷版本並不安全——這項檢驗至關重要，因為無法標記出缺陷程式碼的驗證工具只會提供虛假的安全保證。

在 AlphaProof Code 中，AI 代理協助使用者撰寫規格，然後自主證明實作符合該規格。每一項證明都由 Lean 檢驗，以驗證代理的工作成果。

Signal 的回應

Signal 技術長 Ehren Kret 表示：「過去的形式化驗證僅聚焦於程式碼的較小範圍，Google DeepMind 的方法則能實現顯著的擴展。使用 AI 代理將實際程式碼轉換為有效的 Lean 定理是一項重大突破。隨著 AI 驅動的安全威脅日益增長，對 Signal 協定實作進行嚴謹驗證，讓我們對程式碼的隱私保證更具信心。」

安全的未來

Google DeepMind 認為，攻克這一長期挑戰證明了 AI 能為企業、政府與關鍵基礎設施帶來頂級的安全保證，協助抵禦由代理驅動的網路威脅。該公司表示，驗證 Signal 的核心加密技術，為保護其他重要系統奠定了基礎，範圍從醫療裝置韌體到電網軟體。

這些技術的擴展應用仍需持續研究。若與 CodeMender 等自動化防禦代理結合，形式化驗證有助於對抗現代網路威脅的速度與規模，創造出其防護機制經數學證明有效的軟體。

Google DeepMind 正將其形式化驗證成果開源供社群使用，託管於 google-deepmind.github.io/code-verification。完整技術論文可透過 PDF 取得。對安全研究社群而言，該論文提供了直接檢視經機器檢驗的證明與方法論的途徑——而這種深度的驗證技術未來能擴展至 Signal 之外多遠，延伸至該公司點名的醫療、工業與基礎設施系統，是接下來值得關注的發展。

致謝

這項研究由 Swarat Chaudhuri、Andrew Ferraiuolo、Anton Kovsharov、Tej Chajed、Sam Schlesinger、Karn Seth、Jonathan Katz、Charles Sutton 與 Pushmeet Kohli 開發。

團隊感謝 Eric Wieser 協助開源程式碼、Owen Jones 提供專案管理支持，以及 Martín Abadi、Christopher Henson、Katerina Hristova、Henryk Michalewski、Jonathan Protzenko 與 George Tsoukalas 的寶貴討論。研究人員也感謝 Signal 的 Rolfe Schmidt、Michael Rosenberg 與 Ehren Kret 對方法論提供的意見，以及 Tulsee Doshi、Four Flynn、Kate Olszewska、Alicia Huang、Andy Liu、Benoit Schillings、Raluca Ada Popa、Melvin Johnson、Koray Kavukcuoglu、Demis Hassabis 與 Sundar Pichai 對本專案的支持。