From High-Level DeFi Properties to Concrete Security Bugs, Nurit Dor - DeFi Security Summit 2022
三句話摘要
DeFi 智能合約中使用形式驗證屬性來系統性地發現漏洞的方法論。 規範品質決定測試品質；系統化的屬性定義與漏洞注入驗證，是發現 DeFi 合約隱蔽漏洞的最實用方法。 屬性分類提供系統化思維框架——從最基礎的單元測試到抽象的高級屬性，不同層級的屬性針對不同類型的漏洞，覆蓋範圍互補而非重複。
重點整理
重點- 1
屬性分類提供系統化思維框架——從最基礎的單元測試到抽象的高級屬性，不同層級的屬性針對不同類型的漏洞，覆蓋範圍互補而非重複。
- 2
有效狀態屬性發現了 Compound V3 的位運算錯誤——通過檢查「若餘額 > 0 則相關位必開啟」這一簡單不變式，發現約 50% 的抵押品未被正確計入，這類漏洞用傳統代碼覆蓋率無法捕捉。
- 3
漏洞注入研究是衡量屬性品質的實測方法——與其假設屬性有效，不如故意注入已知漏洞，看屬性是否能檢測到，Silo Finance 的案例顯示 20 個屬性對 6 個注入漏洞的覆蓋率無重疊。
- 4
屬性定義本身就能發現漏洞——即使未執行形式驗證工具，仔細思考「什麼應該永遠成立」這個問題，就能透過邏輯推理在代碼審查時發現錯誤。
實用技巧與重點
乾貨- 屬性的 6 大類型
- 單元測試：檢查特定函數行為
- 有效狀態：系統必須始終滿足的條件
- 變量轉換：什麼能變、誰能變、何時必須變
- 狀態轉換：系統在狀態間的合法轉移
- 高級屬性：不依賴具體實現的抽象條件
- 風險評估：思考最糟情況與反面情境
- 屬性規範化方式
- 邏輯形式：「如果 P 成立，執行操作 X 後，Q 必成立」（霍爾邏輯）
- Certora 驗證語言（CVL）：程序式語法
- Fuzzing 框架：另一種屬性編寫方式
- 真實案例的發現
- OpenSea：函數簽名推導屬性，無需查看實現
- Compound V3：一個位向量屬性同時發現 2 個漏洞（其中 1 個高危）
- Silo Finance：總供應量變化推導存款變化，發現計算錯誤
- SushiSwap 荷蘭拍卷：「人不得申領兩次」這一簡單規則捕捉地址使用錯誤
- 覆蓋率測試結果
- Silo：6 個漏洞注入，20 個屬性，無單一屬性捕捉全部漏洞
- 不同屬性間覆蓋率無重疊區域，組合價值高
結論
結論“規範品質決定測試品質；系統化的屬性定義與漏洞注入驗證，是發現 DeFi 合約隱蔽漏洞的最實用方法。”
完整解析
詳細Certora 產品副總裁 Nurith Tydor 在此演講中闡述了一套系統化的屬性定義方法論，用於在 DeFi 合約中發現深層漏洞。她開篇指出，所有系統都存在漏洞，問題不在於漏洞是否存在，而在於能否有效地定義與檢測它們。
她首先將屬性概念類比到電梯系統：單元測試只檢查門是否能打開，有效狀態則要求運行中門始終關閉，變量轉換關注樓層號何時改變，狀態轉換則把整個系統視為自動機。這層層遞進的分類避免了盲目測試，使團隊能針對不同風險維度進行檢驗。在代碼覆蓋率方面，Tydor 指出傳統的行覆蓋率或路徑覆蓋率都不足以保證安全性，因為漏洞往往出現在特定數值組合下，無法計算但可通過漏洞注入研究來評估。
在具體案例中，Compound V3 的例子最具說服力。該協議使用 uint16 位向量追蹤用戶的抵押品類型，同時用映射表存儲具體額度。一個簡單的不變式「若餘額 > 0 則位必開啟」揭示了位計算中的計數錯誤，導致約 50% 的抵押品未被正確記錄。這個漏洞不僅高危（用戶可被不正當清算），而且該屬性甚至發現了另一個相關漏洞（清算時位未置零）。同樣，Silo Finance 的例子展示了「總供應量變化推導存款變化」這一簡單規則如何捕捉到計算錯誤，導致協議喪失所有流動性。
Tydor 強調，屬性本質上是邏輯命題，可用霍爾邏輯或 CVL（Certora 驗證語言）等形式化語言表達，但即使不用工具驗證，僅通過思考「什麼應該永遠成立」就能在代碼審查時發現漏洞。SushiSwap 荷蘭拍卖的案例說明，「任何人不得申領兩次」這一簡單規則能捕捉到多簽地址被誤用的漏洞——這類漏洞會被傳統單元測試忽略，因為測試通常只考慮 msg.sender，而非其他可能的調用者。
最後，她引入漏洞注入研究來量化屬性的覆蓋率。Silo 的研究顯示 20 個精心設計的屬性對 6 個注入漏洞的檢測覆蓋率中，沒有任何屬性能捕捉全部漏洞，但也沒有重疊冗余——這說明多維度屬性組合的價值在於互補，而非堆疊。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
