Formal Verification of Uniswap v4 Hooks - DeFi Security Summit 2025
三句話摘要
使用 Certora 形式化驗證工具對 Uniswap V4 Hooks 進行數學級別的安全性證明。 形式化驗證不只是安全審計的加分項，它能在官方教學範例中找到類型轉換漏洞這類人工審計容易漏掉的邊界案例，而 Certora Prover 的 CVL 語言讓會寫 Solidity 的開發者都能直接上手。 形式化驗證不是「找漏洞」也不是「零 bug 保證」，而是在明確假設下（如 ERC20 代幣行為正常、預言機公平）證明指定屬性永遠成立。屬性設計錯誤才是最大風險，因為屬性不完整就會漏掉漏洞。
重點整理
重點- 1
形式化驗證不是「找漏洞」也不是「零 bug 保證」，而是在明確假設下（如 ERC20 代幣行為正常、預言機公平）證明指定屬性永遠成立。屬性設計錯誤才是最大風險，因為屬性不完整就會漏掉漏洞。
- 2
摘要（Summary）替換是驗證大型合約的關鍵技巧。Uniswap v4 的內部 swap 函數遍歷所有 tick 且極為複雜，直接驗證會超時；改用非初始化變數（讓求解器自由猜值）表示「任意可能的交換結果」，既保留完整性又讓驗證可行。
- 3
不變量（Invariant）比 require 更嚴謹。Hook 必須部署到特定地址才有權限；與其在每條規則加 `require`，不如先用不變量證明「地址永遠正確」，後續規則直接引用，避免錯誤 require 掩蓋 bug。
- 4
Uniswap V4 教學範例 Points Hook 存在真實漏洞：添加流動性時若手續費大於投入量，`amount0` 可為負值，強制轉型為 `uint256` 導致巨額溢出，攻擊者可藉此鑄造天文數字的積分代幣。
實用技巧與重點
乾貨- 工具名稱：Certora Prover（雲端執行，Python 套件安裝）
- 規格語言：CVL（Certora Verification Language），語法近似 Solidity
- 獲取免費試用金鑰：sora.com 右上角，輸入 email，獲得 3 分鐘免費額度
- 驗證流程：Solidity 合約 + `.spec` 規格檔 → Certora Prover → 雲端求解 → 網頁介面看反例
- 幽靈變數（Ghost Variable）：只存在於驗證過程的虛擬變數，不影響實際合約控制流
- Uniswap V4 Hook 權限機制：權限位元硬編碼於 Hook 合約地址的最後幾位，需暴力搜尋部署地址
- 發現漏洞：Points Hook 的 `modifyLiquidity` 中 `int256 → uint256` 不安全轉型，當 fee > liquidity 時 amount0 為負，觸發環繞溢出可鑄造 2^256 級別代幣
- 通用 Hook 規則庫：所有 Hook 都應驗證「只有 Pool Manager 可呼叫非 view 函數」、「Hook 部署地址權限標誌正確設定」
結論
結論“形式化驗證不只是安全審計的加分項，它能在官方教學範例中找到類型轉換漏洞這類人工審計容易漏掉的邊界案例，而 Certora Prover 的 CVL 語言讓會寫 Solidity 的開發者都能直接上手。”
完整解析
詳細形式化驗證長期被誤解為「需要博士學位」或「可以保證零漏洞」，但 Certora 的研究員在這場演講中澄清了這兩點。形式化驗證的本質是：在給定假設前提下，用數學方式證明合約的指定屬性永遠成立。假設可能是「ERC20 轉帳不收手續費」、「預言機報公允價」，或「治理不作惡」；屬性則是「用戶隨時可提款」、「鑄造數量與投入以太幣 1:1」。只要假設與屬性設計正確，工具就能對所有可能輸入窮舉驗證，反例一旦出現便是真實 bug，修完再跑一次即可確認修復。
實作上，講者以 Uniswap V4 官方教學的 Points Hook 為例，說明完整的驗證流程。Points Hook 邏輯很簡單：用戶在池中花費以太幣（token 0）時，以 1:1 比例鑄造積分代幣；添加流動性時同樣鑄造積分。驗證的第一步是決定測試邊界——理論上應含 Pool Manager，但 Uniswap 內部 swap 函數遍歷所有 tick 過於複雜，因此改用「摘要」替換：以未初始化的 `delta0`、`delta1` 符號變數代表「任意可能的交換輸出」，讓求解器在所有可能交換結果中搜尋違反屬性的情況。
第一次驗證失敗，反例顯示以太幣餘額變化但積分代幣供給不動。追蹤呼叫鏈後發現問題出在 Uniswap v4 Core 內部：若 `msg.sender == address(self)`（即 Hook 本身發起交換），uni swap 不會通知 Hook，屬於隱藏假設，加入 `require(msg.sender != address(hook))` 後再跑。第二次仍失敗，原因是 Hook 的交換後標誌（`afterSwap` 權限位元）未設定，等同 Hook 部署到錯誤地址，Pool Manager 根本不呼叫它。補上地址驗證的 Invariant 後，交換驗證終於出現綠勾。
接著驗證流動性添加函數時再次出現紅叉，反例中以太幣餘額出現超大負數而積分代幣卻暴增，特徵正是整數環繞溢出。深入分析後確認：Uniswap V4 在添加流動性的同時會結算手續費，若累積手續費大於本次添加的流動性量，`amount0` 實際上是負值（`int256`），而 Points Hook 直接將其轉型為 `uint256` 並鑄造代幣——這是官方教學合約中的真實安全漏洞，攻擊者可透過精心設計的流動性操作，以極低成本鑄造天文數字的積分代幣。修復方式是在轉型前加入負數判斷；規格同樣需要更新反映正確的業務邏輯，再跑一次即可收到最終綠勾。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
