Formal Verification with the Certora Prover, Michael George - DeFi Security Summit 2022
三句話摘要
Certora Prover 是一套形式驗證工具，透過邏輯推理而非測試執行，找出智能合約中的所有可能漏洞。 Certora Prover 用數學邏輯推理取代隨機測試，為智能合約提供完整且高效的漏洞驗證能力。 規格定義比單元測試強大許多倍。 CVL 規格只需一條就能取代無限多個傳統單元測試，因為規格檢驗涵蓋所有可能的輸入與儲存狀態組合，而測試永遠只能驗證有限個案例。
重點整理
重點- 1
規格定義比單元測試強大許多倍。 CVL 規格只需一條就能取代無限多個傳統單元測試，因為規格檢驗涵蓋所有可能的輸入與儲存狀態組合，而測試永遠只能驗證有限個案例。
- 2
邏輯推理取代隨機執行。 模糊測試透過產生大量範例並觀察執行結果來尋找漏洞；Certora 則將程式碼與規格轉換為數學邏輯公式，由 SMT solver 判斷是否存在違反條件的情況，可產生具體反例或證明不可能違反。
- 3
CVL 語言提供超越 Solidity 的推理能力。 支援任意值推理、儲存狀態變化追蹤、回滾測試、內部狀態存取、不變量寫法、回滾撤銷等功能，使規格能表達更複雜的合約行為要求。
- 4
驗證時間換取完整性保證。 模糊測試跑數天仍無法確保發現所有漏洞；Certora 驗證通常在兩小時內完成，若逾時則提供簡化技術協助開發者改進規格。
實用技巧與重點
乾貨- 工具名稱：Certora Prover
- 規格語言：CVL（Certora Verification Language）
- 驗證引擎：多個 SMT solver（第三方）
- 可能的輸出結果：(1) 具體反例，(2) 完整證明，(3) 逾時
- 典型驗證時間：最長約 2 小時
- CVL 支援的語法：require（前置條件）、assert（正確行為）、internal 狀態存取、storage 回滾、任意方法呼叫語法
- 整數型別：math int（無溢出整數）
結論
結論“Certora Prover 用數學邏輯推理取代隨機測試，為智能合約提供完整且高效的漏洞驗證能力。”
完整解析
詳細Certora Prover 是一套智能合約安全工具，解決傳統單元測試無法窮盡所有邊界情況的問題。開發者不需寫成千上萬的測試案例，只需用 CVL 域特定語言撰寫一份規格，用自然的程式碼語法描述合約應有的行為——例如指定前置條件、記錄狀態變化、寫出斷言。單一條規格便能涵蓋無限多個測試情境。
其驗證原理與模糊測試截然不同。模糊測試採取試錯法：產生隨機輸入、執行程式碼、觀察是否出錯，重複數天後累積信心。Certora 則採形式驗證策略：將合約程式碼與規格共同轉換為邏輯公式，由 SMT（Satisfiability Modulo Theories）求解器判斷是否存在違反規格的情況。求解器可給出三種答案：(1) 一組具體變數值組合，導致規格失敗，轉換為可執行的交易反例；(2) 數學證明，說明無論如何賦值都不可能違反規格；(3) 逾時。典型驗證耗時最多兩小時，相較模糊測試的多日執行有顯著效率優勢。
CVL 語言設計兼具易用與表達力。語法貼近 Solidity，開發者直觀上手，卻支援 Solidity 無法做到的推理能力：任意值推理（聲明變數不初始化，驗證器遍歷所有可能值）、儲存狀態追蹤與修改、任意方法呼叫語法（如檢驗「任何增加額度的方法」是否滿足某性質）、內部狀態存取、回滾撤銷交易後重新執行的對比測試、不變量的簡潔語法、以及明確的不可回滾路徑規格。
講者舉例說明：ERC20 transfer 方法的規格聲明發送者、接收者、金額三個任意值，記錄轉帳前後的餘額，assert 發送者餘額減少、接收者餘額增加。驗證器發現規格違反並給出反例——發送者與接收者相同。加上前置條件排除此情況後，規格通過驗證。這說明驗證品質取決於規格質量，Certora 正開發工具檢驗規格本身的完整性。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
