DeFi Security summit 2023 - Session 1: DeFi Protocols 1 - Anton Permenev
三句話摘要
用並發對象理論檢測智能合約的重入攻擊與設計缺陷。 智能合約的重入安全問題無法只靠設計模式解決，必須用並發理論檢查操作衝突，並驗證實現是否滿足開發者所定義的合約規範。 外部呼叫是並發系統的yield——當智能合約調用不受信任的地址時，就像把執行權交給另一個線程，被呼叫者的fallback函數可能會重新進入合約，執行任何函數。
重點整理
重點- 1
外部呼叫是並發系統的yield——當智能合約調用不受信任的地址時，就像把執行權交給另一個線程，被呼叫者的fallback函數可能會重新進入合約，執行任何函數。
- 2
線性化是安全的必要條件——若合約的所有並發執行都等價於某種順序執行（符合開發者設計時的線性規範），則重入不會破壞合約的不變式。開發者只需按順序方式設計，系統會自動安全。
- 3
衝突檢測需要三個條件——兩個操作來自不同執行線程、操作同一資料項、至少一個是寫操作。需要比對執行前後（pre/post）的所有操作，判斷是否與其他線程的操作衝突。
- 4
規範優先於模式——checks-effects-interactions只是修復方案，但若開發者心中的規範就不符合這個模式的假設，再好的模式也無法工作。無法準確檢測重入，核心原因是缺少對合約規範的理解。
實用技巧與重點
乾貨- Chain Security：2017年成立，專注智能合約安全審計
- 經典重入例子：withdraw函數在外部呼叫時被fallback函數重入
- 修復模式名稱：checks-effects-interactions pattern
- 並發機制：mutex（互斥鎖）、re-entrant修飾符
- 線性化定義：並發執行 ≡ 相對於某順序規範的合法順序執行
- 不變式例子：balance_sum = contract.balance（假設無強制轉入以太幣）
- 衝突檢測的三項條件：不同線程 + 同一資料項 + 至少一個寫操作
- 三類操作：pre-call（外呼前）、post-call（外呼後）、其他函數操作
- 案例函數：deposit（寫）、withdraw（讀-外呼-寫）、getBalance（讀）都操作同一balance mapping
結論
結論“智能合約的重入安全問題無法只靠設計模式解決，必須用並發理論檢查操作衝突，並驗證實現是否滿足開發者所定義的合約規範。”
完整解析
詳細Chain Security的工程師Anton在演講中指出，智能合約的重入攻擊問題根本上源於開發者對並發執行的誤解。傳統開發思維是順序的——先執行A，再執行B，最後執行C。但當智能合約進行外部呼叫時，就像在並發系統中執行yield操作一樣，將控制權交給不信任的代碼，被呼叫方可以通過fallback函數重新進入合約，執行任何公開函數。這個特性讓大多數開發者在設計時措手不及。
講者強調，解決方案不是簡單應用checks-effects-interactions模式，而是需要理解線性化（linearizability）的概念。線性化是並發理論中的核心屬性，意思是所有並發執行的結果都等價於某種順序執行。如果開發者在設計合約時就考慮到線性化，那麼無論發生多少次重入，都不會破壞合約的不變式。舉例來說，如果合約的規範是「balance_sum必須等於contract_balance」，那麼只要設計符合這個線性規範，重入自然就是安全的。
檢測重入風險的方法是進行衝突分析。兩個操作會產生衝突，當且僅當：它們來自不同的執行線程、操作同一個資料項、至少有一個是寫操作。講者通過balance mapping的例子展示，如果deposit、withdraw、getBalance都在讀寫同一個資料結構，那麼一次重入呼叫中，這些操作可能會衝突，導致合約狀態不一致。比如在執行withdraw的外部呼叫期間，攻擊者可以再次呼叫deposit或withdraw，導致余額計算錯誤。
但這裡有個關鍵轉折：同樣的衝突操作，在不同規範下有不同結論。講者示範了兩個看似相同的合約——都在最後讀取余額，都有外部呼叫——但因為規範不同（一個定義的不變式讓重入不影響，另一個則會被破壞），所以安全性完全相反。這說明checks-effects-interactions模式治標不治本，除非開發者同時理解自己的合約規範。因此，若要準確檢測重入風險，必須結合並發理論的衝突分析與合約規範的驗證。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
