Google DeepMind 研究團隊在 libsignal 重現一項已修復缺陷：新 session 解密失敗、改用舊 session 成功後，程式仍儲存新 session 尚未確認的狀態，包含簽署預密鑰秘密副本。AlphaProof Code 對缺陷版本產生 Lean 證明，核對結果顯示它違反指定安全定理。這項結果只針對特定程式與性質，並不代表整個 Signal 應用沒有漏洞。詳見研究論文。

研究團隊產生約 650 萬行 Lean 證明。這類證明如何連到實際程式，又有哪些限制？

AlphaProof Code 的重點，是把特定程式的安全性質寫成數學規格，再由證明檢查器驗算程式是否符合。一般程式代理的任務差異可參考科研程式代理的比較方式。

AlphaProof Code 驗證 Signal，證明連到哪一層程式？

AI 代理協助建立 Lean 規格與證明，再由 Lean 核心檢查證明是否符合核准規格。DeepMind 驗證的是特定 libsignal 命令列程式的 AArch64 機器碼及列明的安全性質。

形式化驗證是把程式要求寫成數學命題，再證明程式符合命題。Lean 是檢查數學證明的程式語言與證明器。人員核准規格後，代理協助產生證明，Lean 核心負責檢查；證明成立不代表規格正確。

研究者將 Rust libsignal 編譯為 Linux AArch64 執行檔，以 Lean 描述指令和程式執行，證明模型中的協定行為符合二進位程式。驗證性質包括訊息機密性、真實性、前向保密及遭入侵後安全性；符號模型另涵蓋特定 PQXDH 握手的量子攻擊機密性。

驗證範圍是 libsignal-cli 一對一訊息流程和特定 AArch64 Linux 執行檔，未涵蓋群組訊息；部分低階密碼及輸出函式以合約描述。Android、iOS 是否符合相同結論，還取決於編譯、連結與作業系統介面。

形式化驗證補上哪些程式審查缺口？

測試與程式碼審查能發現實際缺陷；形式化證明則針對已定義性質，檢查模型條件下的所有執行路徑。它提供特定規格範圍內的保證，不能取代其他檢查。

測試執行選定案例，弱點掃描尋找已知模式，人工審查判斷程式和威脅模型。形式化證明則檢查符合前提的執行路徑是否都滿足命題，例如遭入侵後的協定安全性。

方法主要檢查方式結果如何解讀
測試執行選定案例僅回報已測情況
弱點掃描搜尋已知模式提供待調查線索
人工審查閱讀程式與設計判斷規格與情境是否合理
形式化驗證證明模型內程式符合規格結論限於已建模範圍與假設

DeepMind 論文呈現兩種缺陷。其一，舊 session 解密成功後，程式仍儲存新 session 未確認的狀態及簽署預密鑰秘密副本；Lean 證明該版本違反安全定理。

其二，PQXDH 回應端未拒絕格式錯誤的 X25519 基底金鑰，攻擊者可藉修改編碼建立共用秘密相同的第二個 session。Lean 證明該版本違反安全定理；兩例都限於論文設定的 Signal 範圍。

seL4 團隊以機器檢查證明微核心 C 程式符合規格，部分設定也證明處理器執行的二進位碼具完整性與機密性等性質。官方文件限定這些結果適用於特定平台與設定。seL4 證明範圍

CompCert 是 INRIA 與 AbsInt 團隊開發的 C 編譯器，將 CompCert C 編譯為多種處理器的組合語言。團隊以 Coq 證明產生的程式與來源程式語義等價，降低編譯轉換引入錯誤的疑慮；結果不涵蓋來源程式本身，且限於 CompCert C 支援範圍。CompCert 官方文件

DeepMind 論文提到，seL4 約投入 20 人年，AlphaProof Code 團隊五人用四週驗證 Signal；兩案範圍不同，不能直接比較成本。延伸閱讀：Lean 證明檢查重點。

DeepMind 論文指出，若假設過強或安全性質定義過弱，有缺陷的程式仍可能符合定理。Lean 核對命題與證明是否相符，不替組織判斷安全需求是否完整。

四欄依序呈現測試、弱點掃描、人工程式審查與形式化驗證，各欄列出檢查對象及結果能支持的結論。
四種方法回答的問題不同，形式化證明的結論也只限於已建模的範圍。

為什麼證明成立，仍可能沒有回答真正的安全問題？

Lean 能檢查證明是否由核准規格推出，卻不會判斷規格是否符合真實威脅、假設是否過強或模型是否漏掉重要環境。規格偏弱時，證明成立仍可能沒有回答實際安全疑問。

規格可能限制攻擊者能力，或只要求較弱的結果。DeepMind 安排人員審閱規格，也以可滿足性與變異測試檢查規格是否空洞；規格品質仍須由熟悉協定、實作與威脅情境的人判斷。

DeepMind 論文描述，使用者會在撰寫證明前審閱、修改並核准規格。這項責任決定證明所代表的安全保證。

研究以 Lean 模型描述 AArch64 指令和部分 Linux 系統呼叫，以合約代表外部函式；硬體、核心與密碼原語也有信任假設。模型和模擬器及實際執行的對照，不等同涵蓋所有環境。程式或環境變更後，團隊須重新確認證明適用性。

部署前應確認規格涵蓋的資料、攻擊者與狀態，哪些函式以合約抽象化，二進位檔和環境是否符合產品，以及改版後誰維護並審核證明。

哪些大型系統值得投入形式化驗證？

當安全性質可明確規格化、失效代價高、程式範圍可界定，且團隊能長期維護時，形式化驗證較值得評估。需求常變或責任分散時，先釐清規格與治理。

Signal 案例有既有協定模型、明確的程式和訊息流程，也有專家補足握手與後量子 ratchet 的組合規格。導入仍需協定、Rust、Lean、機器碼和環境等專業，以及明確的假設核准責任；其他系統不能直接套用其結論或工時。

成本包括規格審核、外部程式庫合約、改版追蹤和跨團隊協作。先挑關鍵性質與最小範圍試行，再評估是否擴大。

一條由左至右的決策流程依序檢查安全性質、程式範圍、信任假設、專家人力與後續維護，未通過時回到釐清或縮小範圍。
先確認性質與範圍，再盤點假設、人力和維護責任，才能判斷是否值得投入。

導入前可以用哪些問題判斷是否合適？

先寫清楚保證性質、程式與環境範圍、依賴假設，以及規格審核和改版維護責任。若無法回答，先縮小範圍再估工具和工時。

  1. 定義失效情境：列出要防止的錯誤或攻擊，以及保證成立的前提。
  2. 劃定程式邊界：列明程式、編譯產物、外部函式與環境，標示合約和假設。
  3. 審查規格：由安全與工程人員確認命題涵蓋真實攻擊，並以反例或變異測試檢查。
  4. 估算維護工作：指定規格、證明審查與改版維護責任人，估算人力及驗證成本。
  5. 小範圍試行：先選失效代價高、邊界明確的程式，確認證明能回答決策問題再擴大。

AlphaProof Code 顯示 AI 代理可協助證明工程，Lean 提供機器檢查。投入前先確認證明目標、涵蓋範圍與維護責任。

  • AlphaProof Code 的 Signal 案例把指定安全性質連到特定 libsignal 編譯後機器碼，範圍不等於完整 Signal 應用。
  • AI 代理產生證明，Lean 核心檢查證明；人員仍須定義、審核規格及信任假設。
  • 導入前應盤點程式邊界、執行環境、外部合約、責任人與改版維護成本。

常見問題

Q1：AlphaProof Code 是否證明 Signal 完全沒有漏洞？

沒有。研究驗證特定 libsignal 命令列程式及明列的安全性質，並依賴規格、密碼原語與執行環境等假設，不能解讀為整個 Signal 產品不存在漏洞。

Q2：Lean 核心檢查通過，代表 AI 代理寫的內容都可信嗎？

Lean 會檢查證明是否符合核准規格；這不表示代理草擬的規格本身正確，也不替團隊確認規格符合實際安全需求。規格仍須人工審核。

Q3：形式化驗證可以取代測試和程式碼審查嗎？

不宜取代。測試、弱點分析、程式碼審查與形式化驗證處理的問題不同；形式化證明只涵蓋已寫入規格和模型的範圍，其他方法仍可補足不同風險。