Rust、Lean、Aeneas 和 AI 代理如何協助微軟 SymCrypt 擴展生產級加密演算法的形式化驗證。
微軟 SymCrypt 運用 Rust、Aeneas 和 Lean 開發新的驗證加密技術，以提供更高的安全保證。我們證明其程式碼安全且正確地實作了標準演算法，特別是針對後量子密碼學。
我們正在發布經過驗證的程式碼、規範、屬性和證明，初期涵蓋 SHA-3 和 ML-KEM。Aeneas 允許驗證大部分 Rust 程式碼，並在 Lean 中提供高效自動化，以支援證明工作。AI 代理則透過撰寫可獨立驗證的證明來擴展自動化能力。
加密程式碼是現代運算基礎的核心，它保護著作業系統、雲端服務、韌體、訊息系統以及連接它們的協定。微小的錯誤可能導致巨大的後果：單一的算術失誤、遺漏的邊界檢查或不正確的狀態轉換，都可能破壞原本健全設計的安全性。
測試和稽核仍然至關重要，但它們本身並不足夠。加密實作通常經過最佳化、具備常數時間特性、針對特定架構，且刻意保持低階。實際交付的程式碼很少像標準中描述的簡潔演算法那樣：它包含簡化、位元操作、SIMD 內建指令、精心設計的迴圈以及針對多種環境的可攜性層。
形式化驗證透過部署機器檢查的證明來彌補這個差距，而非僅依賴測試。它不僅僅檢查程式碼通常是否行為正確，而是針對所有滿足預設條件的輸入，實作精確的數學規範。
去年六月，微軟宣布將在 SymCrypt 中對用 Rust 編寫的新演算法進行形式化驗證。SymCrypt 是 Windows 和 Azure 等產品與服務中使用的加密提供者。新的加密實作正在以安全的 Rust 編寫，然後使用 Aeneas 工具鏈在 Lean 形式證明框架中進行驗證。這特別適用於後量子密碼學，它需要複雜演算法的快速安全實作。
這種組合為我們提供了兩層保證：Rust 排除了廣泛的記憶體安全錯誤類別，而 Lean 證明則根據從標準衍生的形式規範建立了功能正確性。其結果是一種針對生產級加密技術的新驗證方法：在開發人員編寫程式碼時進行驗證，保留以效能為導向的實作選擇，並使證明過程具有足夠的可擴展性，以跟上不斷演進的程式碼庫。
我們已經開源了一個 SymCrypt 分支，其中包含形式規範和證明。這個公開分支將證明產物與其驗證的 Rust 演算法實作一起提供，展示了該方法如何應用於生產級加密程式碼。SymCrypt 並非獨立的研究原型；它是微軟的開源加密函式庫，廣泛應用於 Windows 和 Azure Linux 等產品與服務。
首次發布包含了目前在 Windows 內部版本中使用的 Rust ML-KEM 和 SHA3 程式碼的完整證明。SymCrypt 正在將相同的基於 Rust、Lean 和 Aeneas 的工作流程擴展到更多 Rust 原生演算法，並將它們整合到 Windows 和 Linux 的生產版本中，例如經過驗證的 AES-GCM、FrodoKEM 和 ML-DSA 的 Rust 程式碼。
本文的其餘部分將以 SymCrypt 的這項工作作為具體範例，從公共標準如何轉變為可執行的 Lean 規範開始。
第一步是將演算法應執行的功能形式化。對於加密原語，事實的來源通常是公共標準：NIST 規範、IETF RFC 或其他經過仔細審查的演算法描述。在我們的方法中，Lean 規範旨在與標準保持高度一致。
當標準描述一個迴圈、陣列更新或數學運算時，Lean 模型會盡可能遵循相同的結構。這種語法上的接近性很重要：它使形式規範更容易審核，因為審閱者可以並排比較標準和 Lean。Lean 還允許我們編寫可執行的規範。
這意味著我們可以根據官方測試向量執行形式模型，以捕捉轉錄錯誤、差一錯誤或對標準的誤解。對於像 ML-KEM 這樣的演算法，我們可以進一步證明高階數學屬性，例如證明數論轉換 (NTT) 的形式模型與相關多項式環上的預期運算相對應。
一個代表性的例子是 ML-KEM 中的數論轉換 (NTT)。標準將該演算法描述為對 256 個係數模 q 進行的原地轉換，包含三個巢狀迴圈，使用常數 ζ (= 17) 的連續冪次更新成對的係數。Lean 版本刻意模仿了標準的結構：相同的巢狀迴圈、相同的 zeta 選擇和相同的係數更新，便於逐行人工審查。
同時，它是可執行的並使用數學類型，因此可以根據已知向量進行測試，並連接到有關 NTT 代數意義的更高層次定理。總之，Lean 規範是一個簡潔、可執行、具有數學意義的模型，它與標準保持足夠的接近，可以由密碼學家和證明工程師共同審查。
一旦規範形式化，下一個挑戰就是將其與實作連接起來。我們不要求開發人員用面向驗證的語言重寫生產級加密程式碼，也不生成產品團隊必須擁有的程式碼。相反，我們驗證工程師編寫的 Rust 程式碼，完全按照他們編寫的方式。
Aeneas 透過將 Rust 的中階表示轉換為純 Lean 模型來實現這一點。Rust 的所有權和借用紀律在這裡至關重要。它們讓 Aeneas 能夠安全地消除許多關於指標別名、生命週期和變異的推理，而這些推理使得 C 風格程式碼的驗證成本高昂。
例如，一個在 Rust 中原地更新陣列的函數，在 Lean 中變成一個明確接受並返回功能性陣列的函數。可變借用被轉換為值轉換。這保留了重要的行為，同時為證明工程師提供了一個更容易推理的功能模型。
一旦進入 Lean，該函數就可以配備一個定理，說明它細化了一個形式規範。換句話說，對於每個滿足所需邊界和良好形式條件的輸入，實作函數返回與標準衍生的 Lean 規範相同的數學結果。
這種風格保持了職責的清晰分離。軟體工程師繼續編寫慣用且高效能的 Rust 程式碼。驗證工程師則針對生成的 Lean 模型工作，並證明關於它們的定理。Rust 程式碼和證明並存，但證明負擔不會將程式碼塑造成不自然的樣子。
回到 NTT 的例子，其 Rust 實作是一個函數 `fn ntt(&mut [u16; 256])`，它使用可變借用原地更新陣列。Lean 翻譯將其淨化為一個函數 `ntt : Array U16 256#usize → Result (Array U16 256#usize)`，直接輸出更新後的陣列，同時將其包裝在 `Result` 類型中，以明確捕捉 Rust 函數可能發生 panic 的事實。
在這種情況下，定理指出，如果陣列滿足良好形式不變量（確保它代表一個有效的多項式），那麼執行 Rust 模型 `ntt` 將返回數學規範 `Spec.ntt` 結果的良好形式表示，但需經過從低階陣列到高階多項式的轉換。
將此擴展到實際加密程式碼中的每個函數需要大量的自動化。Lean 的可擴展性使我們能夠建立一個具有符號執行、算術、陣列和位元向量推理策略的自動化梯度。這種體驗變得更接近於除錯：自動化處理常規的證明義務，而工程師可以在目標未自動關閉時檢查和完善證明。
生產級加密技術不能忽視硬體。SymCrypt 必須在從嵌入式和核心環境到雲端服務的各種環境中運行。它還需要利用可用的平台特定指令，包括 SIMD 內建指令和針對特定架構的最佳化路徑。
因此，僅適用於可攜式參考實作的驗證方案是不完整的。我們需要驗證實際交付的程式碼：包括分派邏輯、最佳化例程和目標特定變體。由於 rustc 的輸出本質上是針對特定目標的，我們的工具鏈會針對每個需要驗證的編譯目標多次編譯程式碼，然後合併相應的模型。
實際上，這種合併操作將 Rust 程式碼中 `cfg` 屬性允許的靜態分派，轉變為 Lean 模型中 x86-64 和 aarch64 之間的第一層動態分派。遵循 Rust 程式碼的做法，這些目標特定模型隨後會動態分派到 XMM、Neon 和通用實作的模型。
內建指令需要稍微不同的處理。一些低階封裝器，特別是那些操作原始指標或暴露平台指令的，由小型、經過仔細審查的 Lean 規範建模。其他則可以使用 Rust 程式碼建模，這些程式碼可以根據硬體參考文件進行測試，然後進行翻譯和驗證。周圍的安全 Rust 程式碼隨後根據這些模型進行驗證。
這使得信任表面狹窄，同時保留了硬體加速的效能優勢。重要的是，驗證不需要放棄最佳化。該方法旨在保留生產程式碼的複雜性——包括內建指令、分派和平台特定實作——同時仍然證明一個單一、可審核的正確性聲明。
形式化驗證只有在工程組織中，開發人員能夠理解已證明了什麼時才能擴展。僅僅在儲存庫中存在證明是不夠的；保證必須是可見的、可審查的，並與工程師維護的程式碼同步。為了支援這一點，我們透過自動生成的儀表板公開驗證結果。這些儀表板以面向開發人員的術語總結定理：前置條件、後置條件、涵蓋的函數、受信任的模型和剩餘的假設。工程師無需打開 Lean 即可查看這些資訊。