MakerDAO Smart Contract Safety - When Billions are at Stake, Kurt Barry - DeFi Secuirty Summit 2022

MakerDAO 面臨的根本挑戰是在保護數十億美元抵押品和未償債務的同時發布和維護去中心化金融協議。發布代碼本質上危險重重——可能直接出現 bug，新舊代碼交互可能產生意外結果，代碼語義會隨 EVM 硬分叉改變，即使完全按設計實現也可能出現經濟漏洞，更別提網路擁塞或區塊鏈故障。完全不發布代碼顯然不現實，而完全信任任何單一防御措施也是致命危險。

Kurt Berry 因此闡述了 MakerDAO 採用的「瑞士奶酪」纵深防御戰略。這個比喻的核心是：每一層防線（每塊奶酪）都有漏洞，沒有任何防御技巧是完美或萬能的，但通過組合足夠多的防線，漏洞就不會對齐，大多數問題都能在進入生產前被過濾掉。同時必須準備好應對生產問題的出現，因為它們不可避免。

這個整體工程方法從原則開始。MakerDAO 強調保障（safeguarding）優先於安全（security），因為不安全的代碼可能既損害用戶利益又可能被攻擊——例如錯誤的合約可能直接鎖定資金，用戶會像擔心被駭客攻擊一樣擔心損失資金。其次是意圖-設計-實現的層次結構，用於組織不同抽象層級。例如意圖是實現無需許可的資產交換，設計是恆定產品 AMM，實現是 Uniswap V2 合約。許多 bug 出現在層次的邊界上——可能設計完美但實現不正確，也可能實現完美但機制設計缺乏適當的博弈論基礎。MakerDAO 黑色星期四的拍賣損失就是設計未能匹配區塊鏈環境的典型案例，後來他們重寫了拍賣流程以解決流動性和網路擁塞的限制。

在工程流程上，任何代碼變更都需要兩次簽字確認。對複雜代碼進行逐行審查會議，團隊採取紅隊般的對抗性思維——「我們沒有測試這段代碼，現在試著把它搞壞」。所有標準化流程（如每週治理行動）配備檢查清單，這些在其他安全關鍵領域早已廣泛使用，在 DeFi 中同樣有效。最關鍵的是進行事後分析，建立持續改進的反饋循環——無論員工多優秀都不可能完美，必須通過事後分析不斷改進流程。

測試是基礎之基礎。全面的單元測試覆蓋是基本要求——成本相對於潛在的十億美元損失極低。針對主網分叉版本運行的 RPC 或模擬測試至關重要，因為涉及與鏈上已有代碼的集成，必須在實際狀態下驗證。模糊測試特別適合數值方法，這些方法經常隱藏棘手的舍入問題，肉眼根本發現不了。測試網部署對 MakerDAO 自身和集成夥伴都有價值——後者可能希望在實際運行的共識層上進行測試。關鍵的測試原則是不僅測試每個函數的個別行為，還要定義合約或系統的某些屬性。屬性定義的過程本身就常常能發現原本會忽略的問題，這些屬性對接下來的形式化驗證也極其有用。

形式化驗證使用符號執行或其他形式化方法驗證代碼屬性，但通常耗時且可能昂貴，取決於使用的解決方案。因此 MakerDAO 優先將其用於更關鍵的合約——高風險合約、難以升級的合約或需要 gas 優化的合約。Gas 優化本身是個容易引入 bug 的過程（Solc 優化器就存在一些 bug），所以每當發布 WE View 時都存在額外風險，應進行字節碼級別的形式化驗證。驗證可在多個層級進行：字節碼級別、函數級別、行為級別、合約級別或多合約系統級別。MakerDAO 的工具也在演變。早期使用基於 K 框架、KVM 和 ACT 語言的堆棧（ACT 語言由早期 Maker 開發者創建），現在使用 Sartura 進行許多日常形式化驗證，因為它更易被工程師學習且速度非常快，同時 Sartura 的結構團隊也很出色。他們還在研究 Foundry 與各種開源工具的整合，以提高可訪問性——因為工具複雜性通常是採用的最大障礙。

但形式化驗證本身也不是萬能的。MCD 系統曾進行過完整形式化驗證，但仍然發現 bugs——這正是瑞士奶酪模型的說明。最大的一類 bug 是不同函數或合約間的交互問題（約 5 個），因為形式化驗證只驗證了原始版本每個函數的個別行為，指定得完美無瑕符合預期，但當這些合約或函數組合在一起時，就會出現有趣的現象。有個 bug 甚至在形式化規範中也有體現——代碼和規範都寫了，但兩者都有同樣的 bug，本應有單元測試卻最終被集成測試捕捉到。一個有趣的例子是幻象溢出問題：某些計算即使給出合理的值也會回滾，規範只是說「溢出就回滾」，但應該檢查如果值在某些範圍內是否應該回滾——這也可以透過形式化驗證實現，只是沒有做。最近的發現是他們之前認為核心記賬邏輯中存在某個特定的不變式，但實際上它並不存在，Kurt 純粹為了好玩想證明一下（因為他們準備在 L2 層部署），結果發現它是錯誤的。幸運的是這在生產中不是問題，是那種永遠不會被利用的情況。

經濟建模透過基於代理的模擬或其他金融計算，在各種金融條件下（如價格暴跌）尋找系統的涌現特性。這方法最適合大型複雜升級，會顯著改變底層機制和激勵。MakerDAO 與 Gauntlet 合作進行清算系統升級，是非常好的經驗。Maker 還有內部風險核心部門進行金融建模。記住所有模型都有局限性，關鍵是確保測試了所有需要的場景，代理邏輯內置了正確的激勵。

審計是另一層重要防線，但不應是驅動開發的——所謂「審計驅動開發」（ADD）是個笑話（Kurt 說這是從推特上的 Marillion 那裡偷來的）。審計在代碼精雕細琢時最有效。與審計公司簽訂長期合作協議非常有價值，能保證審計人員的連續性，意味著他們對協議有更深入的理解，更可能發現細微的交互問題——這正是他們重點關注的 bug 類型。MakerDAO 特別推薦 Chain Security。關於漏洞賞金，理想情況下應在發布前將代碼開放給賞金計畫，這樣能在 bug 進入生產前發現它們。但也必須設置生產後漏洞賞金。例如 Multilateral Die 的發布前漏洞賞金計畫發現了 4 個嚴重和高危問題，雖然審計中有些遺漏，但這不能完全歸咎於審計——其中一次審計確實發現了問題的前提條件，但沒有發現問題的全部嚴重性。這說明沒有萬全之策，一切都像瑞士奶酪一樣到處是漏洞，希望奶酪洞越多越好，因為它能提高安全性。目前 MakerDAO 與 Immunify 合作管理其漏洞賞金計畫。

生產問題處理面臨去中心化環境的獨特挑戰。首先是時間鎖——為了防止治理攻擊，大多數協議在操作生效前設置某種延遲，但如果協議被積極利用，可能根本不希望有這個延遲。其次是不可篡改性——有時根本無法升級某些東西，不可篡改性能讓人們真正信任代碼不會未授權被篡改，長期來看擁有不可篡改的金融系統應是目標，規則不能隨意更改，但短期解決漏洞時，某東西有漏洞又無法替換就成了問題。第三是透明度——大多數機構治理流程非常開放，例如在公開論壇上，但如果公開說「這裡有漏洞可能需要修復」，恶意行為者會看到並可能利用它。

MakerDAO 的解決方案包括多個層面。首先是即時訪問模塊，允許管理層採取一些經過特定選擇的特定即時操作，不受時間限制，但當然也嚴格受限，防止在治理攻擊時攻擊者造成太大傷害。這通常結合其他措施，例如確保治理機制能在一定時間窗口內採取行動。如果熟悉 Maker，會知道它使用 1 小時延遲的預言機價格，這讓政府能及時觸發即時訪問模塊，在攻擊或故障時凍結預言機。其次是對無法升級或難以升級的組件進行額外審查。第三是治理流程中的投票委託人，簡化協調工作——投票權可委託給少數人（但不能太少以防風險），與協調可能有很多其他事要做的大型代幣持有者相比容易得多。對於極端生產問題，終極解決方案是「黑暗魔法」機制。基本上可以部署（或雖然不部署但可以創建）一個合約，預先提交到已部署的地址，使用 EVM 中的 CREATE 操作代碼完成。然後需要找信任的人（如審計員或知名社區成員）測試修復方案的安全性。之後可以快速投票通過這個「咒語」，它在部署後立即生效，而不暴露漏洞，也不讓漏洞在時間鎖期間被攻擊。

最後是 MakerDAO 的精選最佳實踐。首先是 Wrapped Ether 基本上在所有情況下都優於 Raw Ether。它更安全——使用 Wrapped Ether 永遠不會出現重入攻擊；代碼路徑少——嘗試同時處理 ERC20 和 Raw Ether 意味著多個代碼路徑，代碼路徑越多風險越大；可組合性強——Wrapped Ether 不需要像普通以太幣那樣進行轉賬審批；ERC20 兼容性廣泛。反駁總是「如果 Wrapped Ether 合約有漏洞怎麼辦」，但 WETH 已經運行多年鎖定數十億價值、代碼簡單沒有管理功能無法升級，這種風險目前極低。除非真的需要 Raw Ether 的 gas 效率，否則用 Wrapped Ether 會更輕鬆。其次，延遲是可以接受的。發布和快速發布的壓力很大確實有合理性，但通常如果有人對某事有不好預感，延遲一週通常比發布有缺陷的東西好得多。第三，逐步降低風險。發布新代碼時應盡量限制系統財務風險，類似傳統 Web 開發的分階段發布或分批推出。更重要的是關乎協議和用戶面臨多大風險，應循序漸進升級——不要一次升級所有東西、不要達到債務上限等等。第四，最小化外部依賴、調用和合約導入，減少導入和外部調用。這樣代碼更易讀、測試和驗證。當然某些複雜性不可避免地存在，但應盡量減少。