Signal加密通過AI撰寫的650萬行數學證明

Signal 的加密程式碼如今多了一項幾乎沒有任何廣泛使用的軟體能夠宣稱的成果：一份數學證明，證實它確實做到了承諾的事。一組 AI 代理深入檢驗了負責執行 Signal 協定的函式庫 libsignal，證明其中的一對一對話能維持機密、確認通訊另一端的身分，並在金鑰遭竊後再次阻擋攻擊者。他們沒有發現任何新的漏洞。

這項成果的意義遠超 Signal 的使用者。這套協定是全球端對端加密通訊的標準，其變體也保護著 WhatsApp、Messenger 和 Google Messages 的對話。要深入檢驗實際部署的程式碼，過去耗時極長，幾乎沒有人嘗試：這個領域最重要的成就之一，是一個經過驗證的作業系統核心，耗費了相當於 20 個人年才完成。這次的工作只花了四週。

這項工具由 Google DeepMind 打造，名為 AlphaProof Code。人類專家和 AI 模型先將 Signal 的安全目標轉化為 Lean 中的形式化陳述；Lean 是一種專為數學證明設計的程式語言，而每一項陳述都經過人工審核。接著，由 Gemini Carbon 驅動、每組 40 至 80 個代理的團隊撰寫證明，每次在單一機器上連續運作 24 至 72 小時。最終成果約有 650 萬行 Lean 程式碼。

沒有人需要相信這數百萬行程式碼。Lean 的核心會檢查每一個步驟，並剔除任何不成立的證明，因此無論是由哪個模型撰寫，或過程中出錯多少次，都不會影響結果。人們真正需要信任的部分小得多：大約 26,000 行規格，以及一個描述 ARM 處理器如何執行程式碼的模型。

這些證明涵蓋了 Signal 用來守護對話的部分：建立聊天連線的 PQXDH 握手程序，以及每則訊息都會更換金鑰的 Triple Ratchet，其中也包括旨在抵禦未來量子電腦的後量子層。實際上，這代表即使有人竊取手機目前使用的金鑰，也無法解鎖較早之前的訊息；而在通訊雙方交換新的金鑰後，竊賊也會再次失去存取權。

為了證明系統能分辨好程式碼和有問題的程式碼，研究人員重新加入了 libsignal 中兩個早已修正的舊漏洞。其中一個會讓函式庫保留一份本應刪除的秘密金鑰副本。兩種情況下，AlphaProof Code 都產生了經機器檢查的證明，證實含有漏洞的版本並不安全。

這項成果的限制也很明確。證明只涵蓋一對一通訊，DeepMind 將群組訊息列為未來工作。它適用於 libsignal 0.105.4 版，該版本是在小型測試程式中，使用標準 Rust 編譯器為 ARM Linux 編譯；並不涵蓋 iPhone、Android 或桌面版的完整 Signal 應用程式。低階密碼學元件被假定為安全，並未經過證明。若經人類核准的規格有誤，保證的效力就會減弱；而 WhatsApp 和其他應用程式各自執行協定的不同版本，因此這項成果不會自動適用於它們。Google 也拒絕向 Wired 透露這項分析耗資多少，或是否打算將它作為服務出售。

Signal 對這項成果表示肯定。Signal 技術長埃倫·克雷特（Ehren Kret）在聲明中表示：「隨著 AI 驅動的安全威脅日益增加，嚴謹驗證 Signal 協定的實作，讓我們對程式碼所提供的隱私保障更有信心。」DeepMind 研究科學家斯瓦拉特·喬杜里（Swarat Chaudhuri）則較為謹慎。他告訴 Wired，要讓這種方法擴展到「全世界所有軟體」，「還有很長一段路要走」。

對 Signal 使用者來說，無須安裝任何東西，也不用更改設定。這份證明針對的是應用程式中早已存在的程式碼。

DeepMind 於 11 月 10 日公開這項研究，並同步發布技術論文；規格與證明也已在 GitHub 上以開源方式釋出。DeepMind 將 Signal 專案形容為朝著 4 月提出的形式化驗證重大挑戰邁進的重要里程碑，並指出醫療器材韌體和電網軟體是接下來希望檢驗的系統類型。

喬杜里也談到，應該讓機器負責多少工作。他告訴 Wired：「我們不希望走向這種由 AI 生成目標、再由 AI 生成證明的『氛圍式』世界。」安全標準仍由人類決定，AI 的工作只是證明它。

標籤: 網路安全, Google DeepMind, AlphaProof Code, libsignal, Signal, 形式驗證