DeFi Security Summit 2023 - Session 17: Focused Talks 4 - Alon Ram
三句話摘要
使用符號執行技術檢測和暴露DeFi智能合約詐騙的方法論。 符號執行提供自動化、客觀的方式檢測智能合約中的隱藏詐騙機制，無需原始碼也能有效驗證代幣合約的公平性。 DeFi的「無信任」性實際上不代表「可信任」——去中心化承諾依然依賴智能合約的安全性和開發者的誠信，任何人都能編寫合約，包括詐騙者，導致地毯拉扯（rug pull）、隱藏鑄造和強制轉帳等多種詐騙方式。
重點整理
重點- 1
DeFi的「無信任」性實際上不代表「可信任」——去中心化承諾依然依賴智能合約的安全性和開發者的誠信，任何人都能編寫合約，包括詐騙者，導致地毯拉扯（rug pull）、隱藏鑄造和強制轉帳等多種詐騙方式。
- 2
符號執行通過系統化探索所有執行路徑來發現隱藏後門——用符號輸入替代具體值，收集路徑約束條件，再用SMT求解器找出觸發詐騙功能的具體輸入值，使隱匿的惡意代碼無所遁形。
- 3
兩類高風險操作可被精確檢測——無限制鑄造會導致代幣通脹和價格下跌，未授權轉帳允許特權用戶直接竊取他人資金，這些都能透過設置適當的約束條件被符號執行識別出來。
- 4
符號執行補足傳統驗證的缺陷——即使有原始碼、經過Etherscan驗證，詐騙代碼仍可能被隱藏或混淆，但符號執行在位元碼層運作，提供獨立於人工審計的客觀驗證。
實用技巧與重點
乾貨- 詐騙規模：過去三年20億美元以上被盜，詐騙代幣超過100,000個
- 常見詐騙類型：地毯拉扯(rug pull)、防止出售(prevent selling)、隱藏鑄造(hidden mint)、強制轉帳(force transfer)
- 符號執行的四步流程：
- 用符號輸入替代具體輸入
- 執行程式並進行符號運算
- 從if陳述句收集路徑約束條件
- 使用SMT(Satisfiability Modulo Theories)約束求解器求解
- ERC-20標準只定義介面，實際功能可任意擴展
- 檢測無限鑄造的約束條件：
- total supply > 起始值
- caller的balance > 起始值
- value = 0（無代價）
- allowance = 0（無授權）
- 檢測代幣盜取的約束條件：
- caller ≠ holder
- caller的balance減少
- allowance = 0（無授權）
- 案例1詐騙代碼：burn函數中設置if(amount == 11)返回大數字，反而進行鑄造而非銷毀
- 案例2詐騙代碼：使用大寫Approve函數（非標準ERC-20的小寫approve），允許owner任意設置任何holder的餘額
- redefine服務：自動化尽職調查API，已與Gnosis Safe整合
結論
結論“符號執行提供自動化、客觀的方式檢測智能合約中的隱藏詐騙機制，無需原始碼也能有效驗證代幣合約的公平性。”
完整解析
詳細DeFi吸引人之處在於其去中心化和無需信任的承諾，但這個承諾卻常被濫用。任何人都可以編寫智能合約，包括心懷不軌的人。過去三年，DeFi詐騙已造成超過20億美元損失，市場流通著超過10萬個詐騙代幣。最常見的詐騙手法是「地毯拉扯」：詐騙者開發智能合約誘導用戶購買代幣，待價格上升後突然提取所有資金，投資者血本無歸。除此之外還有防止出售、隱藏鑄造、強制轉帳等多種詐騙方式。
面對這些隱藏在代碼深處的詐騙機制，傳統審計變得困難。符號執行（symbolic execution）正是解決之道。它是一種軟體測試技術，不用具體數值執行程式，而用符號值代替。想像你有一隻魔法鳥同時看到迷宮的所有可能路徑，無需實際走過每一條——符號執行正是如此：分析程式所有可能執行路徑，收集每條路徑上的約束條件（如if陳述句），再用SMT約束求解器找出具體輸入值，確定是否存在違反預期行為的執行路徑。
應用於智能合約檢測時，首先對代幣合約的關鍵變數（餘額、總供應量、授權額度）設置約束。第一個案例檢測無限鑄造：演講者展示詐騙代幣的burn函數在特定條件（amount == 11）下會執行相反操作，無限鑄造而非銷毀代幣。通過設置約束條件——代幣供應量增加、調用者無代價獲得代幣——符號執行輕易識別出隱藏後門。第二個案例檢測代幣盜取：詐騙者實現了大寫Approve函數（非標準ERC-20的小寫approve），允許擁有者任意改變任何人的餘額，直接盜取用戶資金。
符號執行的強大之處在於不依賴原始碼，可直接分析編譯後的位元碼，即使詐騙者試圖隱藏代碼也無法逃脫檢測。redefine公司已將此技術自動化規模化，開發尽職調查API為用戶、交易所和錢包提供商提供服務，最近與Gnosis Safe整合使其用戶都能受益於這項防護。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
