近日， Verus 這一 Rust 程式碼靜態驗證工具的釋出引發了開發者社群內關於形式化驗證在已強調安全性的程式語言中所扮演角色的熱烈討論。隨著 Rust 因其記憶體安全保證而持續獲得歡迎，像 Verus 這樣的工具旨在透過數學證明程式碼符合其規範，將程式碼正確性提升到新的水平。
Rust 驗證工具生態系統的不斷壯大
Verus 加入了不斷壯大的 Rust 驗證工具生態系統，其中包括 Prusti 和 Creusot。雖然這些工具都有驗證程式碼正確性的共同目標，但它們採用了不同的解決方案。正如一位評論者所指出的，主要的工具有 Verus、Prusti 和 Creusot，但它們採取了完全不同的方法。這並不是重複工作。根據評論中提到的 SOSP 2024 論文，驗證速度似乎是 Verus 相對於類似工具的主要優勢之一。
這些工具允許開發者編寫程式碼應該做什麼的規範，然後靜態驗證程式碼在所有可能的執行情況下都符合這些規範。與只能檢查特定輸入的傳統測試不同，像 Verus 這樣的形式化驗證工具可以證明在整個輸入空間中的正確性。
Rust 驗證工具比較
- Verus：靜態驗證工具，可以檢查程式碼是否符合所有可能執行情況下的規範。目前支援 Rust 的一個子集，並允許驗證操作原始指標的程式碼。
- Prusti：另一種採用不同方法的 Rust 驗證工具。
- Creusot：Rust 生態系統中的第三種驗證工具。
- Kani：用於驗證 Rust 標準庫的模型檢查器。
關鍵討論點：
- 驗證速度作為工具之間的區別因素
- 需要一種通用的規範語言
- 與 Rust 即將推出的效果系統的整合
- 內建依賴型別與外部驗證工具之間的權衡
 |
|---|
| 一張 Verus 的 GitHub 倉庫截圖，突顯了其在 Rust 驗證工具生態系統中的開發和持續貢獻 |
爭論：形式化驗證與測試
這一公告引發了一場關於像 Rust 這樣已經提供強大安全保證的語言是否需要形式化驗證的哲學爭論。一些開發者質疑在 Rust 之上新增驗證工具是否過度，認為對大多數用例來說，測試應該已經足夠。
「測試驗證程式碼在特定輸入上的工作情況。形式化驗證檢查程式碼在每一個輸入上是否都能正常工作。」
這一觀點突顯了測試和驗證之間的根本區別。測試可以證明程式碼在某些輸入下能正常工作，而形式化驗證可以證明程式碼在所有可能的輸入下都能正常工作，包括測試可能遺漏的邊緣情況。
依賴型別的角色
討論中另一個有趣的線索圍繞依賴型別以及它們是否應該內置於語言本身。依賴型別允許型別依賴於值，從而在型別層面實現更精確的規範。然而，正如一位評論者指出的那樣，向 Rust 新增依賴型別可能會顯著增加這個已經很複雜的型別系統的複雜性。
一些開發者表示擔憂，將形式化驗證作為 Rust 的核心部分可能會使入門門檻過高。正如一位評論者解釋的：我的感覺是，依賴型別會增加一個已經以型別系統複雜著稱的語言的複雜性，所以我擔心會超出複雜性預算。他們建議，保持驗證工具的獨立性可以讓需要它們的開發者使用它們，而不會給其他人增加複雜性負擔。
未來方向：通用規範語言
評論中反覆出現的一個主題是不同驗證工具之間需要一種通用的規範語言。隨著這一領域多種工具的出現，開發者表達了對於需要學習不同規範語法來完成類似驗證任務的不滿。
像確保函式永不崩潰這樣的簡單保證可以從所有驗證工具中的標準化語法中受益。一些評論者建議，這種基本保證最終可能會被整合到 Rust 的核心語言中，可能作為即將推出的效果系統（以前稱為關鍵字泛型）的一部分。
討論還涉及到 Rust 正在進行的使用 Kani 等模型檢查器驗證其標準庫的努力。這項工作表明形式化驗證在確保關鍵程式碼可靠性方面的重要性日益增長。
隨著 Verus 繼續發展並擴充套件其功能，它代表了將形式化驗證技術帶給更廣泛的 Rust 開發者群體的重要一步。雖然並非每個專案都需要形式化驗證提供的保證級別，但擁有這些工具豐富了 Rust 生態系統，併為開發者提供了更多確保程式碼正確性的選擇。
參考：Verus