數學證明取代傳統測試：Apple 如何為後量子加密建立新驗證標準

Apple 近日開源其核心加密函式庫 corecrypto 的後量子密碼學（post-quantum cryptography）實作，並同步釋出數學證明與驗證工具，供外部研究人員獨立審查與重現分析。此舉的技術核心，在於 Apple 採用正式驗證（formal verification）方法，以數學手段在既定條件下證明軟體行為符合預期，並在部署前成功攔截一項傳統測試難以偵測的實作缺陷。

為何後量子加密需要更嚴格的驗證

corecrypto 是 Apple 作業系統與服務的底層加密函式庫，提供加密、雜湊（hashing）、亂數生成與數位簽章等功能，運行於逾 25 億台活躍裝置之上。Apple 在公告中指出，corecrypto 一旦出現關鍵漏洞，將影響所有依賴該函式庫的應用程式與功能的安全性與可靠性。

Apple 於 2024 年為 corecrypto 加入後量子密碼學支援，應用範圍涵蓋 iMessage、VPN 與 TLS 網路連線等涉及加密通訊與敏感資料處理的情境。後量子密碼學的目標，是降低未來量子電腦可能破解現有公開金鑰加密演算法所帶來的風險。

考量 corecrypto 須在不同 Apple 裝置與晶片上一致運行，Apple 以可移植的 C 語言撰寫加密程式碼，同時針對時序攻擊（timing attack）採取防護，並在部分內部運算中引入隨機化機制以提高攻擊難度。導入新程式碼時，Apple 採取保守策略，並投入大量資源進行全面測試。

選用 NIST 標準算法的考量

此次開源實作採用美國國家標準與技術研究院（NIST）標準化的後量子演算法 ML-KEM 與 ML-DSA。Apple 表示，兩者因安全性、效能、金鑰與密文尺寸緊湊，以及功能正確性而獲選。

Apple 的驗證流程結合四種方法：傳統測試、模擬、獨立審查，以及正式驗證。其中正式驗證透過數學方法，在既定條件下證明軟體行為符合預期，是整套架構中保證層級最高的環節。

Apple 在評估現有驗證工具與已驗證實作後，自行建立一套客製化系統，可支援多種程式語言、程式碼庫與既有開發流程。Apple 認為，最高程度的保證來自正式驗證與傳統方法的結合，並對端對端結果進行嚴格評估。

與 Galois 合作打造工具鏈

在工具開發方面，Apple 與專注於正式驗證的研究工程公司 Galois 合作，開發可將 Cryptol 模型轉換為 Isabelle 理論的工具，並將可移植 C 程式碼與 Cryptol 串接。Apple 也自行開發 Isabelle 函式庫，以及手動最佳化的 ARM64 組合語言子程式。

Cryptol 至 Isabelle 的轉換工具，讓外部研究人員得以在 Isabelle 環境中重建 Cryptol 模型並進行獨立分析，此次隨 corecrypto 實作一同公開釋出。

正式驗證在部署前攔截真實缺陷

此套驗證架構的實際效益，已在開發過程中獲得印證。正式驗證流程在部署前發現一項傳統測試不易察覺的問題：早期 ML-DSA 實作中缺少一個步驟，在極少數情況下可能導致輸入值超出預期範圍，進而產生錯誤輸出。該問題已在部署前識別並完成修正。

這一案例說明，正式驗證並非僅具理論價值，而是能在密碼學工程的實際開發流程中發揮具體防護作用。

開源釋出的意義

Apple 此次同步釋出數學證明、驗證工具與 Cryptol 至 Isabelle 轉換工具，使外部研究人員得以獨立重現分析結果，而非僅依賴 Apple 的內部保證。對密碼學工程社群而言，這套結合正式驗證與傳統測試的完整工具鏈，提供了一個可參考的後量子密碼學實踐範例。

在各大科技平台積極部署後量子加密的當下，Apple 將正式驗證納入核心開發流程、並以開源方式接受外部檢驗的做法，為業界提供了密碼學工程透明度的具體參照。

本文轉載自 HelpNetSecurity。