DeFi Security 101 2023 - 08 - Josselin Feist
三句話摘要
使用Echidna進行Property-Based Testing與Fuzzing，發現智能合約中的漏洞。 Property-Based Testing用不變量定義系統的應有之義，讓Echidna自動探索能破壞這些承諾的邊界情況，比任何單一審計技術更能發現複雜漏洞。 尋找合約漏洞的四層技術金字塔：單元測試容易偏向快樂路徑，無法發現邊界情況；手工審查效率低且仰賴專家；全自動工具（如Slither）只能找已知的常見漏洞模式；Property-Based Testing則透過定義系統應始終滿足的不變量，由Echidna隨機生成輸入逼迫合約違反這些不變量。
重點整理
重點- 1
尋找合約漏洞的四層技術金字塔：單元測試容易偏向快樂路徑，無法發現邊界情況；手工審查效率低且仰賴專家；全自動工具（如Slither）只能找已知的常見漏洞模式；Property-Based Testing則透過定義系統應始終滿足的不變量，由Echidna隨機生成輸入逼迫合約違反這些不變量。
- 2
不變量的本質是多交易序列才會被破壞的狀態性質：單一交易內的漏洞相對容易發現，但像「Owner被放棄後無法恢復Pause狀態」這類需要多步操作的bug，只能透過讓Echidna自主嘗試不同的函數調用序列才能發現。
- 3
定義不變量是從英文敘述開始的迭代過程：不應直接寫Solidity，而應先用自然語言描述系統的期望行為（如ERC20的「使用者餘額不應超過總供應量」），再轉譯為Solidity的Boolean條件或Assertion，然後執行Echidna檢驗是否被破壞。
- 4
Echidna不是純隨機，而是配備啟發式的智能Fuzzer：會使用代碼覆蓋率反饋來選擇更有價值的交易序列，並自動探索合約內已知的常量與地址，減少無效探索，同時支援序列長度、目標函數等配置來加速搜索。
實用技巧與重點
乾貨- 工具與平台
- Echidna：Trail of Bits開源的智能合約Fuzzer
- Slither：Solidity的靜態分析工具，可作GitHub Action整合到CI
- Medusa：Echidna的Go版本重寫（MVP階段）
- Etheno：用於回放Unit Test並輔助Echidna的工具
- Properties Repo：預定義的常見不變量庫，可直接引入
- 三種Echidna API模式
- Boolean Properties：返回true/false的不變量函數
- Assertion：在代碼中內嵌assert檢查
- Foundry-style：使用setUp()初始化的測試框架風格
- 配置與最佳實踐
- 從最簡單的無狀態不變量開始（Stateless Invariants）
- 定義系統層不變量（System-level）而非單函數層（Function-level）
- 使用`--all-contracts`標籤測試多合約組合問題
- 序列長度（Sequence Length）預設前重置狀態，如設為1000則執行1000次調用後重置
- 使用Module操作或Require進行輸入範圍限制，避免浪費計算資源
- 真實案例
- ERC20 Under/Overflow：轉帳時無檢查會導致餘額溢出，不變量「使用者餘額 ≤ 總供應量」可被破壞
- Owner Renounce Bug：Owner放棄所有權後合約被Pause但無法恢復，需多交易序列才顯現
- 除法捨入漏洞：購買公式 `amount = (ether / price) * 10^18` 中若分子小於10，整除結果為0，導致可以零成本購買代幣
結論
結論“Property-Based Testing用不變量定義系統的應有之義，讓Echidna自動探索能破壞這些承諾的邊界情況，比任何單一審計技術更能發現複雜漏洞。”
完整解析
詳細在智能合約安全審計中，開發者通常依賴四種技術發現漏洞。最基礎的Unit Test能測試具體場景但無法覆蓋邊界情況；手工審查由專家檢視代碼但成本高昂且受限於快照時間點；靜態分析工具如Slither透過模式匹配查找已知漏洞，快速但被限於工具資料庫；而Property-Based Testing則透過讓機器自動化地嘗試各種輸入組合，系統地逼迫不變量被破壞。
Echidna的核心概念是不變量（Invariant）——一個在任何合法操作序列後都應恆成立的邏輯條件。與傳統軟體的Fuzzing目標是找尋導致程式崩潰的輸入不同，智能合約沒有「崩潰」的概念，代之以狀態違反預期。例如ERC20合約中「使用者餘額不應超過總供應量」就是不變量；若Echidna找到能違反此條件的交易序列，則代表轉帳或鑄幣函數存在算術漏洞。
Echidna不是純隨機的猴子在鍵盤上敲擊，而是搭載多項啟發式的智能Fuzzer。它使用代碼覆蓋率反饋來優先選擇能探索新分支的交易序列，利用靜態分析提取合約內的常量與地址作為參數候選，甚至在發現不變量違反後會執行序列最小化，從20次交易削減至3次，幫助開發者快速定位根本原因。這種方法已在Trail of Bits的生產審計中驗證超過五年。
定義不變量的藝術在於從自然語言開始的迭代過程。開發者不應直接編寫Solidity，而應先以英文列舉系統應滿足的性質。以轉帳為例，看似直白的「轉帳應減少發送者餘額、增加接收者餘額」其實暗藏自轉移（Self-transfer）場景被忽視的細節。系統層的複雜不變量（如抵押借貸協議的多合約組合不變量）可能需要五個合約交互並需複雜初始化，此時可在Foundry框架中寫setUp()函數初始化，或使用Etheno回放既有測試快照為Echidna提供起始狀態。最後，透過配置檔可指定目標函數、序列長度、輸入範圍等，避免Fuzzer在無關函數或無效輸入上浪費計算資源。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
