在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即可瞭解哪些代碼已被驗證。這種方法使得形式驗證不再是黑盒，而是與日常開發流程緊密結合的工具。總之，這一方法論為生產級密碼學軟件的形式驗證提供了可擴展的路徑，既保證了安全性，又兼顧了實際部署中的性能和靈活性。