Google DeepMind 在 11 月 10 日公布一項研究，真正值得注意的不是又一個新模型，而是一件過去幾乎做不到的事：把已經廣泛使用的加密程式，驗證到手機和伺服器真正執行的機器碼。過往要證明「實際跑起來的程式」符合安全規格，往往要耗費數年專家時間；這次團隊用名為 AlphaProof Code 的 AI 系統，由五個人在大約四星期內完成。DeepMind 稱，這是首次有已大規模部署的加密協定實作被驗證到這個深度，也是首次用 AI 做到。
為甚麼這件事重要？Signal 所用的加密方法，是現時端對端加密的事實標準：訊息在傳送途中，連服務供應商也無法閱讀。除了 Signal 應用程式本身，WhatsApp、Meta 的 Messenger 與 Google Messages 都採用這個協定的變體。今次驗證的，是各家所依據的參考實作 libsignal，不是整款 Signal App，也不是上述任何一間公司自己的分支，因此不能說「WhatsApp 已被證明安全」。但它首次把「人類訂下的安全規格」與「編譯之後真正會跑的程式」連起來——而設計與實作之間，正是過往最容易漏掉漏洞的地方。
還有一句必須先講清：AI 沒有「證明 Signal 安全」。它證明的是，在訂明的範圍內，這份參考實作編譯後的機器碼，符合人類審定的規格。團隊甚至把兩個已知、現已修復的舊漏洞加回去，系統能夠證明有漏洞的版本並不安全。人類仍然負責審核規格；最後把關的，是一套名為 Lean 的數學證明檢查系統，而不是模型自己說了算。
一、究竟證明了甚麼
形式化驗證的意思，是用數學證明來確認程式符合事先寫好的安全規格，而不是只靠測試去撞出漏洞。今次證明涵蓋四項使用者最關心的保證：
| 安全屬性 | 簡單來說 | 覆蓋範圍 |
|---|---|---|
| 前向保密 | 即使金鑰日後洩漏，先前的訊息仍然保密 | 兩套模型都有證明 |
| 認證 | 訊息與通訊雙方的身份不能被冒認 | 兩套模型都有證明 |
| 入侵後安全 | 裝置曾被短暫入侵，之後的訊息仍能恢復保護 | 兩套模型都有證明 |
| 握手保密 | 雙方建立連線時交換的內容，對未來的量子對手亦保密 | 只在符號模型中證明 |
團隊用了兩套常見的安全模型來交叉檢查：一套把加密元件當成不可打開的黑盒（符號模型），另一套則考慮這些元件在數學難題假設下的實際強度（計算模型）。對未來量子電腦仍能保密的那一項，只在前一套模型中得到證明。
驗證對象是 libsignal v0.105.4 與配套元件 spqr v1.6.0 的單對單通訊程式碼，也就是兩部裝置之間一條工作階段，不包括群組或整款應用程式。研究人員把未經修改的程式庫包進一個小型命令列工具，用原版編譯器編成 AArch64 執行檔——AArch64 是現時多數手機晶片所用的指令集，也就是程式編譯後、機器實際執行的那一層。驗證覆蓋建立工作階段、傳送與接收；產生金鑰的步驟沒有被驗證，金鑰改由證明的前提提供。被驗證的程式約 560 KB，約 14 萬條機器指令。
二、為甚麼一定要驗到「機器碼」
過去二十年，多數協定驗證停在設計圖，或停在為了方便驗證而改寫的程式，不一定等於市面上正在跑的那個版本。編譯器為了加速會重排指令，記憶體佈局會變，錯誤處理路徑也可能被忽略，真實漏洞往往就藏在這些縫隙裡。
今次證明直接針對編譯後的執行檔，而不是原始碼。好處是：連編譯器本身也不再被預設為可信；如果編譯過程改壞了程式，證明就會失敗。代價是推理難度遠高於只看原始碼。研究人員另外用模擬器和 Arm 官方模型，核對他們對機器指令的理解是否正確。
成本對比更能說明這次的變化。形式化驗證的經典案例中，seL4 微核心用了約 20 人年，CompCert 驗證編譯器用了約 6 人年，而且兩者的程式碼都是為驗證而寫。今次是五個人、四星期，對象是未經修改、已經在生產環境使用的程式庫。
三、人類寫規格，AI 寫證明，Lean 負責把關
Lean 是一套用來撰寫和檢查數學證明的系統，核心很小，可以獨立覆核。分工很清楚：人類決定要證甚麼、審閱並批准規格；AI 代理負責寫出數百萬行證明；最後由 Lean 的核心檢查這些證明，是否真的對上獲批的規格。代理寫錯就會被核心拒絕，所以這些由 AI 產出的證明本身被視為不可信的中間產物，真正要信任的是規格與檢查核心。
DeepMind 明言，團隊成員沒有寫任何一行證明。人類做的是劃定範圍、選定參考模型、批准受信任的陳述，以及裁決會改動信任假設的規格修訂。代理也會主動標出需要人手複查的部分，DeepMind 稱這部分約佔程式碼 1%。
四、650 萬行這個數字怎麼讀
公開倉庫接近 700 萬行 Lean 程式，當中約 650 萬行是證明。這個數字容易被讀成「安全保障有 650 萬行之厚」，但其實不然。保證來自兩處：人類批准的規格是否寫對，以及 Lean 核心是否可靠。真正需要人閱讀的，是規格、機器指令的語意，以及證明所依賴的定義，規模大約是數萬行，而不是數百萬行。
DeepMind 自己也承認，當證明變便宜，最難的問題變成「該證甚麼」。多數工作量落在規格，不在證明本身。
五、把兩個已修復的漏洞放回去
為了檢驗規格是否夠強，研究人員取出兩個 libsignal 曾經存在、現已修復的漏洞，把它們重新放回現時版本的程式裡，再編譯成「有漏洞的執行檔」，用同一套證明去跑。
- Weak state。新工作階段解密失敗時，程式錯誤地改用舊工作階段再試，結果可能把不該留下的密鑰狀態存下來。
- Small subgroup。建立連線時沒有檢查對方提供的金鑰是否合法，攻擊者可重播握手並建立第二個工作階段，卻共用同一秘密。
結果是：在符號模型中，安全定理對有漏洞的版本不成立，系統不但能指出它不安全，還能給出具體的反例。計算模型無法用同一方法反證，因為要推翻那一類定理，幾乎等於去證明某個數學難題本身，那是尚未解決的問題。因此今次「抓漏」的示範，是在符號模型中完成的。
六、五個必須說清的限制
- 沒有驗證整個 Signal 應用程式。對象只是
libsignal的單對單工作階段程式碼，包在命令列測試工具內，不是 Signal 的用戶端。介面、金鑰儲存、更新機制都不在範圍。 - 沒有覆蓋群組與多裝置。每次只處理一條工作階段，訊息長度固定，沒有多裝置狀態。身份金鑰採「首次使用即信任」，信任是如何建立起來的，並沒有被檢驗。
- 側通道不在範圍。例如從運算時間推斷秘密這類攻擊，並沒有被模型化。
- 後量子保證有限。符號模型證明握手對未來量子對手保密，但計算模型明確不保證這一點。另外，有關金鑰持續更新的證明，只說明新設計不弱於舊設計，不是證明後量子加固本身已足夠。
- 部分攻擊被模型排除。有些重播或尚未完成握手時的情況，並沒有寫進定理裡。稿件不能把模型以外的攻擊，說成已經被排除。
七、對香港讀者與企業的實際意義
對企業採購與風險管理，意義首先在成本結構。形式化驗證過去只出現在最高安全等級的系統，因為人力成本難以負擔。當大約四星期的代理工作，可以取代數年專家時間，把「請說明形式化驗證的範圍與信任基礎」寫進採購要求，就開始變得現實。但審閱時要看的是規格覆蓋了甚麼、哪些部分仍要預先假設，而不是證明寫了多少行。
對後量子遷移，今次驗證的握手設計把傳統金鑰交換與後量子方案混合使用，值得納入討論。本港金融機構正評估如何落實後量子路線圖，本站早前報道 IBM 在香港金融科技周的解說，當中提到銀行從 DART 走向量子安全的步驟。今年 10 月 Cloudflare 成為後量子公開憑證授權機構，反映憑證層的遷移已開始。量子運算時間表與密碼安全的關係，可參考離子阱量子運算與密碼安全時間表的分析。
對 AI 治理，今次也提供一個可複用的模式：讓代理大量生產不可信的工件，再由一個小而可審計的核心逐件檢查。這個模式在程式碼審查、合規文件、財務對帳都用得上。前提是核心夠小、夠確定，而規格由人負責。缺少規格，代理只會更快地產出無法審計的答案。
八、常見問題
AlphaProof Code 是否證明 Signal 應用程式整體安全？
不是。驗證對象是參考實作 libsignal 的單對單工作階段程式碼，再編譯成機器可執行的檔案。應用程式的介面、金鑰儲存、群組通訊、多裝置同步與更新機制都不在範圍。
650 萬行證明是否等於很高的安全保證？
不直接相等。證明的可靠性由 Lean 核心保證，AI 代理本身不可信。真正的保證取決於規格是否正確，以及有多少內容必須預先信任。
WhatsApp 或 Google Messages 的加密是否已被驗證？
沒有。DeepMind 驗證的是 libsignal 參考實作。WhatsApp、Messenger 與 Google Messages 使用該協定的變體，各有自己的分支與整合方式，這些分支沒有被驗證。
為何要驗證機器碼，而不是原始碼？
因為漏洞可能在編譯和優化時出現。把證明對準機器實際執行的程式，編譯器就不被預設為可信；編譯過程若改壞了程式，證明會失敗，錯誤不會被隱藏。
香港企業今天可以怎樣用這個結果？
三種用法：在採購條款要求供應商說明形式化驗證的範圍與信任基礎；在後量子遷移評估中，把傳統與後量子混合的握手設計納入討論；在內部 AI 治理上，採用「代理生產、小核心檢查」的流程，並要求人類負責規格。