DeFi Security 101 - 2023 - 03 - Jaroslav Bendik
三句話摘要
用形式驗證技術數學證明智能合約的正確性，發現傳統測試漏掉的安全漏洞。 形式驗證的成敗關鍵不在工具而在規範——寫對規範比進行驗證本身更難、更重要。 規範定義決定驗證品質——即使驗證工具完美，若規範寫錯也驗證不出實際問題，這是形式驗證最難的部分。
重點整理
重點- 1
規範定義決定驗證品質——即使驗證工具完美，若規範寫錯也驗證不出實際問題，這是形式驗證最難的部分。
- 2
驗證不是一次性檢查，應在代碼初期就寫好規範，每次改動都自動跑驗證，規範與代碼一起演進。
- 3
並非靈丹妙藥，形式驗證、測試、審計三者應搭配使用，各自填補彼此的盲點。
實用技巧與重點
乾貨- 工具分類：
- 證明助手(Proof Assistants)：Isabelle, Daphne, Coq, Cake — 功能強大，使用難度高，改代碼需調整證明
- 模糊測試+靜態分析：速度快易用，但可能有假陽性/假陰性，非窮舉檢驗
- Certora Prover — 中間方案，提供完全保證，用戶不需懂形式驗證但必須寫規範
- 驗證管道步驟：
- 對比 Solidity 源碼 ↔ EVM 字節碼（不同編譯器產生不同字節碼）
- 轉譯為 Three Address Code（自訂中間表示，指令簡化易分析）
- 靜態分析：指針分析、程式切片、值域分析（簡化驗證空間）
- 生成驗證條件（邏輯公式）
- 轉換為 SMT（Satisfiability Modulo Theory）格式
- SMT 求解器求解（支援並行執行多個求解器）
- 輸出：數學證明 or 反例(包含具體數值 + 完整執行跡)
- 規範撰寫模板：
- 定義初始狀態、環境變數（sender、balance等）
- 設定前置條件(assumptions)，如帳户最少餘額
- 呼叫智能合約函數
- 設定後置條件(requirements)，驗證結果狀態
- 添加斷言(assertion)，如「轉帳前後總額不變」
- 具體案例： 轉帳函數自轉時增加餘額的bug可被「sum of balances 不變」規則捕獲；初始狀態：Alice 7 個代幣；自轉 5 個；結果變成 12 個（應為 7 個）→ 規則被違反 → 反例報告輸出。
結論
結論“形式驗證的成敗關鍵不在工具而在規範——寫對規範比進行驗證本身更難、更重要。”
完整解析
詳細智能合約安全一直是區塊鏈生態的痛點。從小合約到大項目，無數次的 bug 導致數百萬美元損失，同時摧毀社區信任。傳統測試和模糊測試雖在軟件業廣泛應用，但往往無法覆蓋所有邊界情況。形式驗證提供了一條不同的道路：用數學方法嚴格檢驗代碼的所有可能執行。
形式驗證的定義很直白：用形式方法在數學基礎上證明或反駁算法相對於規範的正確性。關鍵字是「證明」——這表示獲得數學保證，不存在違反規範的執行。但前提是規範本身必須精確無歧義。如果開發者規範寫錯了，再嚴密的驗證也無法捕獲實際問題。這就是為什麼形式驗證的難點不在工具而在規範定義。
業界對形式驗證充滿誤解。有人說它只能證明不能反駁、有人說複雜度太高無法實用、有人期望它產生「無懈可擊」的代碼、有人認為它能完全替代審計和測試。實際上，形式驗證既是發現 bug 的強大武器，也是驗證安全屬性的有效工具，但絕不是銀彈。它應該與傳統測試和人工審計分層配合。
Certora 等工具位於光譜的中間。相比 Isabelle、Coq 等證明助手需要專家手工構造冗長證明，Certora 大幅降低門檻——用戶無需精通形式驗證理論，但必須明確描述合約的安全性質。例如，某轉帳函數在自轉時會增加餘額。驗證工具通過「轉帳前後所有用戶餘額總和不變」的規則就能捕獲，因為違反這條規則的執行會被直接報告出來，附帶具體數值和完整的執行步驟。
驗證過程涉及多環節。首先對比 Solidity 源碼與 EVM 字節碼，因為編譯器差異可能導致不同字節碼行為。隨後轉譯為 Three Address Code（自訂中間表示），進行指針分析、程式切片、值域分析等靜態優化，大幅簡化問題規模。然後生成驗證條件——一個邏輯公式，其可滿足性當且僅當存在違反規範的執行。最後交給 SMT 求解器，得到數學證明或具體反例。反例報告包含賦值表和執行跡，讓開發者清楚看到 bug 是如何發生的。
形式驗證應在開發初期就集成，而非只在上線前運行。規範應與代碼同步演進，每次改動都自動驗證。Certora 提供的競賽和免費試用方案，目的就是降低開發者採用成本，推動形式驗證在 DeFi 的實踐。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
