Securing the Future: Apple's Blueprint for Formal Verification of corecrypto

向量子安全加密技術的轉型已不再是理論上的練習，而是生產環境中的必然需求。隨著將後量子加密整合至 iMessage 與其他關鍵服務中，Apple 面臨著在超過 25 億台活躍裝置上部署新演算法——ML-KEM 與 ML-DSA——的艱巨任務。

鑑於 corecrypto 中的單一關鍵錯誤就可能危及所有依賴它的應用程式與功能的安全性，Apple 已超越了傳統的測試方法。他們實施了一套嚴謹的正式驗證藍圖，以證明其實作的數學正確性，確保其忠實於 FIPS 203 與 FIPS 204 規範。

The High Bar for corecrypto

將新演算法加入 corecrypto 是一個非常保守的過程。Apple 會根據四項主要標準來評估候選演算法：提升安全性、經受過全球密碼分析的安全性設計、高效能（延遲與功耗）以及精簡的參數以最小化網路影響。

一旦演算法被選中，其實作必須滿足三個嚴格要求：

  1. Security: Code 必須防止資訊洩漏，特別是防範時序側信道攻擊（timing side-channels）。
  2. Optimization: 實作必須最大化 Apple silicon 的效率。
  3. Correctness: Code 必須忠實地實作標準，並且每次都能產生正確的輸出。

The Challenges of Formal Verification

雖然傳統測試至關重要，但它無法提供與正式驗證同等的保證程度。正式驗證使用數學證明來展示一個系統滿足特定屬性。然而，這個過程極其耗費資源，需要深厚的數學專業知識，以及對實作與規範進行精確的模型化。

對於 corecrypto，Apple 識別出在用於金鑰生成、封裝與簽署的特殊子程序序列中存在特定風險。這些子程序通常涉及具有大操作數（多項式與大數）的複雜算術運算，其中進位或借位可能會導致細微的錯誤。單獨驗證子程序是不夠的；驗證必須證明一個子程序的輸出與下一個子程序的輸入範圍完全相容。

A Custom Verification Pipeline

由於現有的工具通常缺乏對 ARM64 assembly 的支援，或者需要放棄現有的開發者工具，Apple 設計了一套結合了幾種專業工具的自定義方法：

The Toolchain

  • Cryptol: 一種用於建立演算法模型的正式語言。
  • Software Analysis Workbench (SAW): 用於驗證 Cryptol 模型是否與 C 實作相符。
  • Isabelle: 一種強大的證明助手，用於驗證複雜的數學證明。
  • cryptol-to-isabelle: 由 Galois 開發的自定義轉換器，用於彌合 Cryptol 模型與 Isabelle 公式之間的差距。

The Process Flow

  1. C to Cryptol: 可移植的 C 實作被手動轉換為 Cryptol。接著 SAW 會驗證 C code 碼是否與此 Cryptol 模型相符。
  2. Cryptol to Isabelle: Cryptol 模型被轉換為 Isabelle。同時，FIPS 規範也被手動轉換為 Isabelle。
  3. Equivalence Proof: 使用 Isabelle，工程師編寫了（超過 50,000 步的）證明，以展示實作模型與規範是等價的。為了擴展此規模，Apple 開發了一個可重複使用的 Isabelle 理論與引理（lemmas）函式庫。
  4. Assembly Verification: 為了處理手動優化的 ARM64 assembly，Apple 證明了每個 assembly 子程序與對應的已驗證 C 子程序是等價的。這避免了從頭開始針對高層級規範進行 assembly 驗證的必要性。

Real-World Impact and Results

這套嚴謹的過程帶來了實質性的安全性提升。Apple 發現了早期 ML-DSA 實作中的一個缺失步驟，該步驟可能導致輸入超出預期範圍，進而可能在無聲中損壞密碼學運算。他們也識別並修復了第三方證明中的一個錯誤。

正如社群所指出的，這些正是傳統測試會規避的錯誤類型：

"The missing-step bug in early ML-DSA is the perfect case for SAW. rare inputs that pass code review because the line that should be there doesn't look absent, it looks like the next line is correct."

Limitations and Complementary Methods

正式驗證並非萬靈丹。Apple 承認存在特定限制：

  • Compiler Trust: 這種方法假設編譯器能從已驗證的 C code 碼正確地產生 CPU 指令。
  • Tooling Gaps: SAW 的某些限制意味著 ML-DSA 的所有可能訊息大小都無法被驗證，因此在這些特定情況下需要退回到傳統測試。

為了填補這些差距，Apple 將正式驗證與模擬工具以及廣泛的傳統測試相結合，以防止資訊洩漏與其他非功能性漏洞。

透過開源其 Isabelle 理論與 Cryptol-to-Isabelle 轉換器，Apple 旨在鼓勵更廣泛地採用這些方法，推動產業向著一個標準邁進：即關鍵的密碼學軟體應透過設計來證明其正確性，而非僅透過測試來達到穩定性。

Sources