DeFi Security 101 2025 - From Fuzzing to Formal Verification | Kevin Lotz, Certora
三句話摘要
從模糊測試到形式化驗證：用 Foundry + Certora Prover 為智能合約提供數學級安全保證。 模糊測試快速易上手但靠機率，形式化驗證用數學公式一次涵蓋所有輸入——最佳實踐是兩者並用，讓 fuzz 覆蓋日常、讓 FV 守護核心經濟不變量。 模糊測試的本質是機率保證：Fuzz 再多次也只覆蓋輸入空間的極小比例，對於只有特定超大整數才能觸發的 bug（概率約 1/2²⁵⁶），實際上永遠找不到。
重點整理
重點- 1
模糊測試的本質是機率保證：Fuzz 再多次也只覆蓋輸入空間的極小比例，對於只有特定超大整數才能觸發的 bug（概率約 1/2²⁵⁶），實際上永遠找不到。
- 2
形式化驗證用公式取代枚舉：CVL 規格和 Solidity fast test 看起來幾乎相同，但 Prover 把程式碼與規格編譯成一個覆蓋所有輸入的邏輯公式再交給 solver 求解，不依賴隨機性。
- 3
Stateful invariant 的歸納法驗證：對有狀態合約，先證明 invariant 在建構後成立，再對每個改變狀態的函數證明「若 invariant 進入則 invariant 離開」，即可保證所有可達狀態均滿足。
- 4
FV 的假陽性問題與工程解法：形式化驗證會假設任意符合 invariant 的狀態，可能包含現實中不可達的狀態，需透過加入 `require` 前提（如 totalSupply == sum of balances）手動排除，或將程式碼模組化降低求解複雜度。
實用技巧與重點
乾貨- 工具：Foundry（forge fuzz）、Certora Prover / Storra EVM Prover、CVL（Certora Verification Language）
- 平台：Certora 提供雲端 SaaS prover，可免費申請 approver key（適合中小型合約）
- Bug 觸發數字：特定 uint256 大整數作為 popcount 輸入，efficient 實作回傳 0（應為 129）
- Forge fuzz 參數：`--fuzz-runs 100000`，本例跑 100,000 次未命中
- Vault fuzz：約 33,000 次函數呼叫（deposit/mint/redeem/withdraw），未觸發 solvency 違反
- Vault bug 根因：`convertToAssets` 使用 `mulDiv(..., ROUND_UP)` 應改為 `ROUND_DOWN`
- CVL invariant 語法：直接寫斷言表達式（無需 `assert`），如 `totalAssets() >= totalSupply()`
- 配置方式：`.conf` 檔指定 contract、spec 檔路徑及最佳化參數
- 開發建議流程：unit test → fuzz test → 確定核心 invariant → 對經濟關鍵屬性做 FV
- Prover 超時策略：拆分程式碼模組、增加人工投入寫模組化規格
結論
結論“模糊測試快速易上手但靠機率，形式化驗證用數學公式一次涵蓋所有輸入——最佳實踐是兩者並用，讓 fuzz 覆蓋日常、讓 FV 守護核心經濟不變量。”
完整解析
詳細這場演講的核心問題是：我們如何確信一段智能合約程式碼是正確的？講者以此為起點，帶領聽眾從模糊測試一路走到形式化驗證，並用兩個具體 demo 展示兩者的差異。
第一個 demo 以 popcount 函數為例。講者展示一段使用位元操作的高效組合語言實作，並依序嘗試三種驗證方式：第一是簡單的具體測試（4 個固定輸入），第二是 Forge fuzz 功能等效測試（與 naive 循環實作比較，跑 100,000 次），第三是對 popcount 的數學性質進行 fuzz（`popcount(2x) == popcount(x)`、`popcount(2x+1) == popcount(x)+1`）。三種方式均通過，但當改用 Certora Prover 以 CVL 規格語言寫出相同的屬性時，Prover 立即找到反例：一個特定的超大 uint256 整數，高效實作回傳 0 但正確答案是 129。這個整數出現的機率約為 1/2²⁵⁶，模糊測試幾乎不可能隨機命中，而形式化驗證的邏輯公式本身即涵蓋所有可能輸入，不需要「碰運氣」。
第二個 demo 轉向有狀態合約，以 ERC-4626 Vault 的償債能力（solvency）為例。Forge invariant test 呼叫約 33,000 次隨機函數序列，均未觸發 solvency 違反。接著講者寫出 CVL invariant（`totalAssets >= totalSupply`），並在 Certora Prover 上執行。Prover 很快在 `redeem` 函數上找到反例：Vault 的 `convertToAssets` 使用了向上取整（round up），導致用戶贖回時可能取走略多於應得的資產，最終造成 Vault 資不抵債。修正方式是改為向下取整（round down）。修正後再次驗證，Prover 對所有可達狀態均給出數學級保證。
講者最後整理兩者的根本差異：模糊測試只覆蓋隨機抽樣的狀態與輸入，提供機率性保證；形式化驗證用一個公式覆蓋所有可能輸入與狀態，提供數學性保證。FV 的代價是需要學習 CVL、可能產生假陽性（需手動排除不可達狀態），以及對複雜合約可能超時（解法是模組化）。實務建議是兩者並用：開發初期從單元測試與 fuzz 開始，確定核心經濟不變量後，針對最關鍵的屬性補上形式化驗證，並將兩者的規格同時作為回歸測試使用。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
