DeFi Security 101 2023 - 12 - Tomer Ganor
三句話摘要
使用 CVL 形式化驗證語言改進區塊鏈協議安全性的完整實踐方法 透過將 CVL 屬性驗證集成到開發流程，可在開發階段系統性地發現所有可能狀態下的協議漏洞，無需依賴人工測試的完整性，大幅降低上線後的安全風險。 CVL 通過形式化驗證覆蓋傳統測試的盲點。開發者用與 Solidity 相似的語法編寫屬性規則，驗證程式在所有可能輸入和初始狀態下的行為是否符合預期。驗證器窮舉所有狀態組合，單次驗證的覆蓋度遠超手工測試。
重點整理
重點- 1
CVL 通過形式化驗證覆蓋傳統測試的盲點。開發者用與 Solidity 相似的語法編寫屬性規則，驗證程式在所有可能輸入和初始狀態下的行為是否符合預期。驗證器窮舉所有狀態組合，單次驗證的覆蓋度遠超手工測試。
- 2
屬性驗證發現難以捕捉的真實漏洞。演講展示在 ERC-20 代幣中發現的漏洞：當用戶向自己轉移代幣時，代碼誤執行兩次，導致無限複製代幣。此類邊界情況在傳統黑盒測試中幾乎無法察覺。
- 3
不變量用歸納法證明系統的永恆真理。以「不存在的提案狀態必為 None」為例，先證明構造函數後屬性成立，再證明任意函數執行後仍成立，最終確立該屬性永遠有效。治理協議中的「已執行提案無法重新激活」等關鍵屬性都用此法保證。
- 4
CI 集成實現持續自動化驗證。規則集成後，每次開發者 PR 提交都自動重新驗證代碼，防止任何修改（無論多細微）引入屬性違反。演講中 BGD Lab 的案例顯示，一個被集成的規則在 PR 提交時失敗，立即暴露了新漏洞。
實用技巧與重點
乾貨- CVL 驗證模式
- Rule（規則）：檢查函數執行前後狀態變化，參數為任意地址、任意金額、任意區塊時間戳
- Invariant（不變量）：使用歸納法證明某屬性永遠成立
- Parametric Rule（參數化規則）：涵蓋合約中所有外部/公開函數的所有輸入組合
- 已檢測到的真實漏洞
- ERC-20 轉移漏洞：msg.sender == recipient 時余額翻倍（用戶可無限增發代幣）
- 委託邏輯漏洞：委託給零地址被誤處理，規則初次失敗於 Bob 為零地址情況
- 治理提案漏洞：過期提案被誤轉為「已排隊」狀態，允許重新執行
- 治理 V3 屬性示例
- 不存在提案（ID > 計數器）狀態必為 None
- 已執行、已取消、已過期狀態為終止狀態，無法轉移到其他狀態
- 委託完整性：委託人 A 委託給 B 時，A 投票權減少、B 投票權增加，其他用戶不受影響
- 驗證結果類型
- 綠色對勾 ✓：屬性驗證通過，所有狀態和輸入都無法破壞該屬性
- 紅色 X ✗：發現反例，伴隨具體的輸入值、地址、區塊狀態顯示漏洞發生路徑
- 性能與超時處理
- 增加不變量條件縮小可能狀態空間，加速驗證
- 函數摘要（Summarization）：用 CVL 實現替代原生 Solidity 代碼，減少驗證開銷
- 調整前置條件（Require 語句）篩選有意義的測試場景
結論
結論“透過將 CVL 屬性驗證集成到開發流程，可在開發階段系統性地發現所有可能狀態下的協議漏洞，無需依賴人工測試的完整性，大幅降低上線後的安全風險。”
完整解析
詳細CVL（Certora 驗證語言）是一套形式化驗證框架，核心目標是解決智能合約難以通過傳統測試全面驗證的根本問題。與單元測試只檢驗具體場景不同，CVL 驗證器窮舉所有可能的輸入組合與系統狀態，若屬性在任何情況下都成立，則生成通過證明；否則輸出具體反例。
形式化驗證從屬性定義開始。以 ERC-20 轉移為例，基本屬性是「轉移前後，發送方和接收方余額之和應保持不變」。CVL 規則宣告任意地址、任意轉移金額，從任意初始狀態開始執行轉移，然後斷言余額守恆性。演講展示的真實漏洞正是這樣被發現的：當 msg.sender 等於 recipient 時，代碼誤將轉移邏輯執行兩次，導致接收者余額增加超過預期。這類邊界情況在普通黑盒測試中極難發現，因為開發者通常不會主動測試「向自己轉移代幣」這種看似無意義的場景。
不變量是更強形式的屬性證明，採用數學歸納法。治理協議中的關鍵不變量例如「不存在的提案 ID 狀態必為 None」。證明過程分兩步：首先驗證構造函數執行後該屬性成立（基礎步），然後從任意狀態假設屬性已成立，執行任意函數與任意輸入後，再驗證屬性仍成立（歸納步）。若兩步都通過，即可確立該屬性永恆成立。另一個治理相關的不變量是「已執行、已取消或已過期提案為終止狀態」。這背後的安全理由是防止已過期提案被重新激活而重複執行（如重複支付）——一旦提案進入終止狀態，系統中任何函數都無法將其轉移到其他狀態。
實踐中的關鍵洞察是邊界情況的精確處理。講者展示的委託規則初次驗證失敗，原因是規則考慮了零地址作為委託對象。在以太坊，零地址有特殊含義（無法發起交易、無法投票），所以委託給零地址實際上等於委託給自己或未委託。修復方案是在規則的前置條件（Require 語句）中明確排除零地址，確保規則只驗證有語義的情況。這體現了形式化驗證的嚴謹性——必須精確定義邊界假設，否則規則可能在邊界情況下得出虛假結論。
CVL 最大的實踐價值在於 CI 集成。將驗證規則添加到持續集成流程後，每次開發者提交 PR 都自動重新驗證代碼。這種機制確保任何修改（無論多細微）都無法悄悄引入屬性違反。演講中提及 BGD Lab 的案例：一個已驗證的規則在某次 PR 提交時突然失敗，立即暴露了新代碼的漏洞。相比之下，如果只依賴人工審計和黑盒測試，這類漏洞往往要到部署後才被發現，代價遠高於開發階段的修復。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
