DeFi security Summit 2023 - Session 14: Formal Verification - Netanel Rubin Blaier
三句話摘要
通過形式驗證（Formal Verification）發現並修復 DeFi 數學庫的關鍵漏洞——以 PRBMath 四捨五入錯誤為案例。 對於 DeFi 涉及核心數學邏輯的代碼，形式驗證雖有學習成本但回報率極高，能有效發現傳統代碼審查和模糊測試容易遺漏的邏輯錯誤。 交易函數錯誤導致資金抽取攻擊：自動化做市商（AMM）通過數學函數決定交易是否可執行；交易函數中的算術錯誤讓攻擊者能系統性執行不利交易，使流動性提供者資金流失，類似於通貨膨脹效應。歷史案例包括 Alpha Homora、100Finance 等重大漏洞。
重點整理
重點- 1
交易函數錯誤導致資金抽取攻擊：自動化做市商（AMM）通過數學函數決定交易是否可執行；交易函數中的算術錯誤讓攻擊者能系統性執行不利交易，使流動性提供者資金流失，類似於通貨膨脹效應。歷史案例包括 Alpha Homora、100Finance 等重大漏洞。
- 2
優秀的庫仍存隱藏漏洞：PRBMath 是寫得很好的庫，擁有大量單元測試和活躍維護，但 mulDiv 函數的漏洞在版本 1.0-4.0 中潛伏近兩年。問題在於負數處理時應向負無窮舍入（floor 的數學定義），但實現卻向零舍入，例如 mulDiv(-180, 114, 1) 返回 -12 而非正確的 -13。
- 3
形式驗證相比模糊測試更適合數學代碼：形式驗證將代碼轉換為邏輯方程並證明正確性，不同於模糊測試的隨機探索；對於數學函數，規範寫作接近自動化，可在 CVL 語言中直接表達數學定義，無需專業驗證工程師。
- 4
系統化檢查無遺漏的關鍵：形式驗證通過觸及每個代碼路徑確保邏輯完整性；即使代碼有充分的單元測試，重構時容易忽略某些函數的測試，正式規範可補充這一盲點。
實用技巧與重點
乾貨- 受影響版本：PRBMath 1.0-4.0
- 修復版本：4.0.1（添加警告）
- 長期方案：支持多種舍入模式
- 相關歷史漏洞：Alpha Homora、SPL Token Lending Bank、ELD HDL Distribution Bug、100Finance、Minus Capital Exploit
- 驗證工具：Certora Prover
- 驗證語言：CVL（Certora Verification Language）
- CVL 特性：語法類似 Solidity；使用無邊界整數（unbounded integers）代替 uint256；自動生成反例
- Bug 範例：mulDiv(-180, 114, 1) 返回值錯誤（-12 vs. 正確的 -13）
- 核心算法基礎：Knuth's Algorithm M（針對無符號整數設計，向零舍入）
結論
結論“對於 DeFi 涉及核心數學邏輯的代碼，形式驗證雖有學習成本但回報率極高，能有效發現傳統代碼審查和模糊測試容易遺漏的邏輯錯誤。”
完整解析
詳細自動化做市商（AMM）是 DeFi 的核心基礎設施。通過恆函數做市商（CFMM）模型，AMM 使用數學函數判斷交易是否執行。最著名的例子是 Uniswap 的 x*y=k 公式。然而，交易函數中的算術錯誤成為攻擊向量：攻擊者能系統性誘導做市商接受不利交易，導致流動性提供者資金流失。攻擊者無需改變 LP 代幣數量，但持有者的實際購買力下降，類似於通貨膨脹。這類漏洞並非理論假設——Alpha Homora、100Finance 等重大攻擊都利用了四捨五入錯誤。
PRBMath 是一個廣泛使用的 Solidity 定點計算庫，提供高效的數學運算。講者團隊在審計中發現了一個隱藏的漏洞。mulDiv 函數用於精確計算 floor(x*y/d)，但其負數處理存在邏輯錯誤。該漏洞在版本 1.0-4.0 中潛伏了近兩年。問題的根源在於：mulDiv 基於 Knuth Algorithm M，這是針對無符號整數設計的，對無符號數進行向零舍入。當應用於有符號數時，應遵循 floor 的數學定義——向負無窮舍入。實際運行中，mulDiv(-180, 114, 1) 返回 -12，而數學上正確的結果應是 -13。
講者強調形式驗證區別於傳統的模糊測試。形式驗證將代碼轉換為邏輯方程，試圖自動證明其正確性。對於數學庫，編寫規範相對簡單——直接將數學定義轉錄為 CVL 語言即可。CVL 語法類似 Solidity，使用無邊界整數表示邏輯數字（無 uint256 限制）。檢測此漏洞所需的規範極為簡潔：調用函數、以邏輯形式計算預期結果、驗證相等性。Certora Prover 等工具自動生成反例（如 x=-180, y=114, d=1），驗證人員可直接在 Remix 中確認問題。
這個案例揭示了一個深刻的啟示：即便是寫得很好、經過充分測試的庫仍可能包含邏輯錯誤。人類在複雜的低級運算中容易出錯，尤其是在代碼重構時可能遺漏某些函數的測試。形式驗證的價值在於系統化地觸及每個代碼路徑，確保邏輯完整性。對於具有核心數學或經濟邏輯的代碼部分，形式驗證是理想選擇：無需深入了解函數細節，只需驗證其實現是否符合數學定義。講者認為半自動化驗證工具對提升 DeFi 生態的安全性至關重要。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
