在SymCrypt中驗證Rust密碼學：從標準到程式碼

微軟SymCrypt團隊近日宣佈了一項新的形式化驗證方法論，旨在確保用Rust編寫的密碼學程式碼的功能正確性。這一方法結合了Lean證明助手和Aeneas工具鏈，使得密碼學實現能夠從公共標準（如NIST規範）直接對映到可執行的Lean規範，並進一步與工程師編寫的Rust程式碼連線。該方法的核心思想是，透過將標準轉化為形式化規範，然後利用Aeneas將Rust程式碼翻譯為純函式式的Lean模型，再使用定理證明這些模型精煉了規範，從而保證程式碼的行為與標準一致。

形式化驗證的必要性在於，密碼學程式碼是現代計算安全的基礎，微小的錯誤可能導致嚴重後果。傳統的測試和審計雖然重要，但不足以應對最佳化的、體系結構特定的低階程式碼。形式化驗證透過機器檢查的證明來填補這一空白，確保對於所有滿足前置條件的輸入，程式碼的行為完全符合數學規範。微軟在去年六月宣佈了這一計劃，首先針對後量子密碼演算法，因為這類演算法需要快速且安全的實現。Rust提供了記憶體安全保障，而Lean則提供功能正確性證明，兩者結合為生產級密碼學提供了雙重保障。

目前，驗證工作已經取得了實際成果。SymCrypt已開源了一個包含形式規範和證明的分支，其中首批發布包括對ML-KEM和SHA-3的完整證明，這些演算法的Rust實現已隨Windows Insider版本釋出。SymCrypt正在將相同的Rust、Lean和Aeneas工作流擴充套件到更多演算法，如AES-GCM、FrodoKEM和ML-DSA，並整合到Windows和Linux的生產版本中。

方法論的第一步是將公開標準轉化為形式化的Lean規範。設計目標是保持規範與標準在語法上的接近性，以便於審計。例如，對於ML-KEM中的數論變換（NTT），標準描述了具有三個巢狀迴圈的就地變換，Lean規範模仿了相同的迴圈結構和係數更新，允許逐行比較。同時，規範是可執行的，可以透過官方測試向量進行測試，甚至證明高階數學性質。

第二步是透過Aeneas將Rust程式碼連線至規範。Aeneas將Rust的中間表示翻譯為純函式式的Lean模型，利用Rust的所有權和借用規則簡化指標別名和可變性推理。例如，一個就地更新陣列的Rust函式在Lean中變為顯式接收並返回陣列的函式。然後，工程師可以附加定理，證明該模型精煉了規範。這保持了職責分離：軟體工程師繼續編寫慣用的高效能Rust程式碼，驗證工程師則針對生成的Lean模型進行證明。

為了擴充套件到實際密碼學程式碼中的所有函式，團隊利用了Lean的可擴充套件性，構建了一個自動化梯度，包括符號執行、算術、陣列和位向量推理的策略。自動化處理常規的證明義務，工程師則在自動證明失敗時進行檢查和修正。

支援硬體行內函數和多種架構是生產級密碼學的關鍵。SymCrypt必須在嵌入式、核心和雲環境等不同平臺上執行，並利用平臺特定的指令，如SIMD行內函數。驗證不能只適用於可移植的參考實現，而必須覆蓋實際分發的程式碼，包括排程邏輯和最佳化變體。為此，工具鏈針對每個需要驗證的編譯目標多次編譯程式碼，然後合併模型，將靜態排程轉換為Lean模型中的動態排程。行內函數透過小型的、經過仔細審查的Lean規範或透過可測試的Rust程式碼建模，周圍的安全Rust程式碼則針對這些模型進行驗證。這樣在保持驗證覆蓋面窄的同時，保留了硬體加速的效能優勢。

最後，為了讓驗證結果對開發者可見，團隊提供了自動生成的儀表板，以開發者友好的術語總結定理、前置條件、後置條件和剩餘假設。工程師無需開啟Lean即可瞭解哪些程式碼已被驗證。這種方法使得形式驗證不再是黑盒，而是與日常開發流程緊密結合的工具。總之，這一方法論為生產級密碼學軟體的形式驗證提供了可擴充套件的路徑，既保證了安全性，又兼顧了實際部署中的效能和靈活性。