Google DeepMind以AI形式化驗證Signal協定，未發現新漏洞

根據《連線》(Wired)報導，Google DeepMind的研究人員使用名為AlphaProof Code的代理式AI框架，以數學方式證明了Signal協定的數項關鍵密碼學保證。這項在四週內完成的概念驗證工作屬於形式化驗證：它運用數學來檢查軟體是否如預期運作，而不是只測試部分案例。

Signal協定是Signal應用程式背後的加密方案，如《連線》所指出，它同樣保護Google Messages與WhatsApp中的通訊。因此，這項分析被視為對一套保護海量訊息的密碼學的又一次獨立驗證。《連線》稱其對密碼學與AI本身都是一個里程碑，同時強調其範圍有限。

DeepMind究竟證明了什麼？

團隊證明的是協定的「數項」關鍵保證，而不是全部。《連線》明確指出，這次分析並未對整個Signal行動應用程式進行形式化驗證，研究人員也把結果描述為更大進程中的一個節點。DeepMind研究科學家史瓦拉特·喬杜里(Swarat Chaudhuri)對《連線》表示：「我們對這個結果非常興奮，但要把它推廣到全世界所有軟體還有很長的路要走，而我們想做到這一點。」

同一篇報導指出，這次分析在所檢查的協定部分中沒有發現新漏洞。研究人員還把AlphaProof Code用於含有已知且早已修補漏洞的舊版Signal：工具正確辨識了這些漏洞，並顯示這些版本無法通過形式化驗證。這項測試很重要，因為它說明該方法在存在缺陷時會失敗，而不只是在沒有缺陷時成功。

• 工具：AlphaProof Code，Google DeepMind的新型代理式AI框架。
• 耗時：四週，屬於概念驗證專案。
• 結果：證明了關鍵密碼學保證；在所分析的部分中未發現新漏洞。
• 舊版本：偵測出已知且早已修補的缺陷，並顯示協定無法通過驗證。
• 公開：規格與證明將發布，以協助其他形式化驗證工作。
• 成本：未揭露；作為研究專案免費完成。

AI與人類如何分工？

在AI時代之前，人們需要描述想要證明的性質，把這些描述轉成公式，再建構證明。《連線》解釋，代理式AI可以大幅縮短最後一步所需的時間，這讓四週內完成Signal評估成為可能。DeepMind的研究人員補充，他們起步時占了一些先機，因為Signal基金會先前已對程式碼中較小的部分做過形式化驗證。

Signal技術長艾倫·克雷特(Ehren Kret)在《連線》引述的聲明中表示：「先前的形式化驗證只集中在程式碼的較小部分，而Google DeepMind的方法能夠顯著擴大範圍。」他還說，隨著由AI驅動的資安威脅增加，對實作進行嚴格驗證，讓Signal對其程式碼的隱私保證更有信心。

DeepMind認為自己的主要進展是一種「人機協作流程」：代理幾乎在每個階段都有所貢獻並自我修正，而人類在關鍵節點進行審查。喬杜里說：「我們不想要一個由AI產生目標、又由AI產生證明的世界。」形式化證明只保證已寫下的性質，因此人類對規格的審查仍然至關重要。

圍繞Signal的另一項並行工作

DeepMind的工作並不是證明Signal密碼學的唯一嘗試。Beneficial AI Foundation與Signal的羅爾夫·施密特(Rolfe Schmidt)以及Lean FRO合作，發起公開專案「Signal Shot」，計畫用證明輔助工具Lean驗證該協定及其Rust實作。該專案打算用Aeneas工具把Signal的Rust程式碼翻譯成Lean，並列出待驗證的元件，包括後量子金鑰交換PQXDH、Double Ratchet以及SPQR/Triple Ratchet。《連線》並未把這項倡議與DeepMind的工作連結起來，兩者是各自獨立的努力。

還有哪些不確定之處？

《連線》指出，懸而未決的問題是：由AI自動化的形式化驗證能否以可行的成本擴大規模。Google拒絕透露Signal分析的成本，也拒絕說明是否計畫推出形式化驗證的商業產品或服務。Google Cloud首席科學家、DeepMind研究副總裁普什米特·科利(Pushmeet Kohli)設想，擔心程式錯誤的銀行與其他公司將來可以說自己能證明軟體的某些性質。這是一種設想，而不是已宣布的產品。

這對企業意味著什麼？

對選擇通訊工具或以Signal協定開發產品的企業而言，這項結果是對協定設計的一個令人安心的訊號，而不是對所有使用該協定的應用程式的認證：完整的Signal應用程式並未被驗證，產品的部署方式、伺服器與設定也都不在證明範圍內。公開的規格與證明為資安團隊提供了可研究與重複利用的材料。由於成本與商業化方案都未知，企業暫時還不能指望用這種方法對自家程式碼做形式化驗證，但現在就可以向關鍵軟體供應商詢問，哪些性質已被明確規定並獲得證明。