Billion Dollar Bugs, Neville Grech - DeFi Security Summit 2022
三句話摘要
智能合約安全審計的科學方法：從漏洞發現到代碼審計最佳實踐 智能合約審計的未來不在單次人工審查，而在科學化的靜態動態混合分析搭配持續自動化監控，且清晰的不變性文檔可將審計效率提升數倍。 靜態與動態分析的交集發現高價值漏洞：團隊使用宣告式程序分析（Datalog）將字節碼轉換為SQL類似的關係模型，查詢所有可能執行路徑；同時透過區塊鏈瀏覽器分析歷史執行記錄。兩種方法交集極小，卻能精準鎖定掌控大量資金卻極度脆弱的合約。
重點整理
重點- 1
靜態與動態分析的交集發現高價值漏洞：團隊使用宣告式程序分析（Datalog）將字節碼轉換為SQL類似的關係模型，查詢所有可能執行路徑；同時透過區塊鏈瀏覽器分析歷史執行記錄。兩種方法交集極小，卻能精準鎖定掌控大量資金卻極度脆弱的合約。
- 2
Solidity的隱性設計差異導致類別的漏洞：`this.foo()`是外部調用（msg.sender改變），`foo()`是內部調用（msg.sender不變）。Multi-Chain橋的permit機制因WETH沒有實作而成為空操作，攻擊者可冒充已授權用戶提取資金，最終造成300萬美元損失。
- 3
閃電貸回調實現的標準化進展：早期開發者檢查回調方並驗證caller，但任何人都可發起閃電貸並構造惡意payload。直到最近一年，EIP-3156標準化API，要求檢查發起者身份，大幅降低此類漏洞。
- 4
易審計代碼優於依賴單次審計：審計只能證明特定時點的安全性，而協議持續演進。比持續人工審計更經濟的方案是以代碼中明確的不變性註釋（時間性、功能性、結構性）搭配自動化持續監控服務。
實用技巧與重點
乾貨- 工具與平台
- Watchdog：自動化漏洞檢測工具，Phantom將於年底部署至所有TVL>1000萬項目（免費）
- Contract Library（library.dw.com）：已部署智能合約反編譯庫，支持以太坊，數周內加入Phantom
- 交易調試器：比etx.info快100倍（特別是大型交易）
- 漏洞披露與賞金
- Harvest Finance、Primitive Finance、Defy Saver、Vesper、BT Finance、Multi-Chain Bridge
- Multi-Chain漏洞：自2021年共9個漏洞賞金，總額300萬美元
- 最大損失：Multi-Chain橋permit機制漏洞，批准額度10億美元，實損300萬美元
- Solidity常見陷阱
- `this.foo()` vs `foo()`：前者外部調用改變msg.sender，後者內部調用保持原msg.sender
- Permit濫用：WrapDeed的permit()無返回值搭配fallback，成為空操作（幻象函數）
- 閃電貸回調：標準化前缺少發起者檢查，允許任意payload執行兌換和資金轉移
- 不變性文檔分類
- 時間性：執行到代碼某部分前調用者檢查的條件
- 功能性：如代幣中金額的範圍規模
- 結構性：策略在執行特定操作時需實現的功能
結論
結論“智能合約審計的未來不在單次人工審查，而在科學化的靜態動態混合分析搭配持續自動化監控，且清晰的不變性文檔可將審計效率提升數倍。”
完整解析
詳細Neville團隊在過去一年多時間內，透過科學化的安全研究方法，成功揭露多個重大智能合約漏洞並獲得共計300萬美元的賞金。他們的核心技術創新在於整合靜態與動態分析。靜態分析採用宣告式程序分析技術，先將智能合約的字節碼（比源代碼低但比機器碼高的中間表示）轉換為關係型結構，類似SQL資料庫，然後對所有可能的執行路徑進行遞迴查詢。動態分析則透過專門為安全研究人員設計的區塊鏈瀏覽器，查詢所有已部署合約的歷史執行記錄。兩者交集往往極小，但恰好指向那些掌控鉅資卻存在關鍵漏洞的合約。
在具體案例中，Multi-Chain橋的漏洞完美展示了Solidity設計細節的危險性。該橋提供兩個存款函數：常規存款（安全轉帳）和permitDeposit。WETH代幣的permit機制因為沒有明確實作但存在fallback函數，導致`permit()`呼叫實際上是空操作——簽名驗證通過但不執行批准。攻擊者利用這一點，先對合約進行一般批准後，可以偽造permit簽名，冒充任何已授權用戶將其資金存入橋接。相似的漏洞也出現在Primitive Finance的閃電貸回調實現中：開發者檢查了回調方身份，卻沒驗證閃電貸發起者，任何人都能發起貸款並傳遞惡意payload執行竊取資金的兌換操作。
講者強調，編寫易於審計的代碼比盲目追求最安全的代碼更實用。審計本質上時間有限，關鍵在於讓審計員快速理解代碼意圖。這要求開發者明確記錄三類不變性：時間性（執行路徑上的前置條件檢查），功能性（數據範圍約束），結構性（組件之間的協議要求）。更重要的是，由於協議會持續演進，單次審計不足以維持長期安全。比持續昂貴的人工審計更經濟的方案是採用技術驅動的持續監控——Watchdog正是這一理想的具體實踐，將在Phantom生態內免費部署。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
