DeFi 合約安全的新模式：關注協議不變性

摘要

不要只為特定的函數寫require 語句；為你的協議寫require 語句。函數遵循檢查(requirements)- 生效(Effects)- 交互(INteractions)+ 協議不變性(Invariants) 或FREI-PI 模式可以幫助你的合約更加安全，因為它迫使開發人員除了關注函數級別的安全之外，還要關注協議級別的不變性。

動機

2023 年3 月，Euler Finance 被黑客攻擊，損失2 億美元。 Euler Finance 是一個借貸市場，用戶可以存入抵押品並以其為抵押進行借款。它有一些獨特的功能，實際上他們是一個可與Compound Finance 和Aave 媲美的借貸市場。

你可以閱讀關於這個黑客的事後總結。它的主要內容是在一個特定的函數中缺少健康檢查，允許用戶打破借貸市場的基礎不變性。

基礎不變性（Fundamental Invariants）

大多數DeFi 協議的核心都有一個不變性，即程序狀態的一個屬性，它被期望永遠是真的。也可能有多個不變性，但一般來說，它們是圍繞著一個核心思想建立的。這裡是一些例子：

• 如在藉貸市場中：用戶不能採取任何行動，使任何賬戶處於不安全或更不安全的抵押品倉位（「更不安全」意味著它已經低於最低安全閾值，因此不能進一步提取）。

• AMM DEX 中：x * y == k，x + y == k，等等。

• 流動性挖礦抵押中：用戶應該只能提取他們存入的抵押代幣數量。

Euler Finance 出錯的地方不一定是他們增加了功能，沒有寫測試，或者沒有遵循傳統的最佳實踐。他們對升級進行了審計，並有測試，但還是被漏掉了。核心問題是他們忘記了借貸市場的核心不變性（審計人員也是如此！）。

注：我不是要挑刺Euler，他們是一個有才華的團隊，但這是一個最近的案例。

問題的核心

你可能在想「嗯，沒錯。這就是他們被黑的原因；他們忘了一個require 語句」。是也不是。

但為什麼他們會忘記require 語句呢？

檢查- 生效- 交互不夠好

推薦給solidity 開發者使用的一個常見模式是Checks-Effects-Interactions（檢查- 生效- 交互）模式。它對於消除與重入有關的錯誤非常有用，而且通常會增加開發人員去執行輸入驗證的的數量。 _但是_，它容易出現只見樹木不見森林的問題。

它教給開發人員的是：「首先我寫我的require 語句，然後我做生效，然後也許我做任何交互，然後我就安全了」。問題是，通常情況下，它變成了檢查和效果的混合體– 不錯吧？交互仍然是最後的，所以重入性不是一個問題。但它迫使用戶關注更具體的功能和個別的狀態轉換，而不是全局的、更廣泛的背景。這就是說：

僅僅是檢查- 生效- 交互模式就會使開發者忘記他們協議的核心不變性。

對於開發者來說，它仍然是一個出色的模式，但總是應該確保（服務於）協議的不變性（說真的，你還是應該使用CEI！）。

正確做法：FREI-PI 模式

以dYdX 的SoloMargin 合約（源碼）中的這個片段為例，它是藉貸市場和槓桿交易合約。這是一個很好的例子，我稱之為功能檢查- 生效- 交互+ 協議不變性（Function Requirements-Effects-Interactions + Protocol Invariants ）模式，或FREI-PI 模式。

因此，我相信這是早期借貸市場中唯一沒有任何市場相關漏洞的借貸市場。 Compound 和Aave 沒有直接出現問題，但他們的分叉代碼有關於過問題。而bZx 則被黑了多次。

檢查下面的代碼，注意以下的抽象概念：

1. 檢查輸入參數（_verifyInputs）。

2. 動作（數據轉換，狀態操作）

3. 檢查最終狀態（_verifyFinalState）。

仍然執行常用的Checks-Effects-Interactions。值得注意的是，帶有額外檢查的檢查- 生效- 交互並不等同於FREI-PI– 它們是相似的，但服務於根本不同的目標。因此，開發者應該認為它們是不同的：FREI-PI 作為一個更高的抽象，旨在實現協議安全，而CEI 旨在實現功能安全。

這個合約的結構真的很有趣– 用戶可以在一連串的行動中執行他們想要的行動（存款、借款、交易、轉讓、清算等）。想存入3 個不同的代幣，提取第4 個，並清算一個賬戶？這是一個單一的調用。

這就是FREI-PI 的力量：用戶可以在協議內做任何他們想做的事情，只要核心借貸市場的不變性在調用結束時成立：一個用戶不能採取任何行動，將任何賬戶置於不安全或更不安全的抵押品倉位。對於這個合約，這是在_verifyFinalState 中執行的，檢查每個受影響賬戶的抵押情況，確保協議比交易開始時更好。

該函數中包括一些額外的不變性，這些不變性是對核心不變性的補充，有助於實現關閉市場等附屬功能，但真正保持協議安全的是核心檢查。

以實體為中心的FREI-PI

FREI-PI 的另一個問題是以實體為中心的概念。以一個借貸市場和假定的核心不變性為例：

從技術上講，這不是唯一的不變性，但它是針對用戶實體的（它仍然是核心協議不變性，通常用戶不變性是核心協議不變性）。借貸市場通常也會有2 個額外的實體：

• 預言機

• 管理/ 治理

每一個額外的不變性都會使協議更加難以保障，因此越少越好。這實際上就是Dan Elitzer 在他那篇題為：為什麼DeFi 已壞以及如何修復它#1 無預言機協議文章中所說的（提示：這篇文章實際上並沒有說預言機是問題所在）。

預言機

對於預言機，以1.3 億美元的Cream Finance 漏洞為例。預言機實體的核心不變性：

事實證明，用FREI-PI 在運行時驗證預言機是很棘手的，但是可以做到，需要一些預先考慮。一般來說，Chainlink 是一個很好的選擇，可以主要依靠，滿足大部分的不變性。在極少數的操縱或意外情況下，有一些保障措施可能是有益的，這些保障措施可以減少靈活性，而有利於準確性（比如檢查最後知道的值是否比當前值大百分數百）。同樣，dYdX 的SoloMargin 系統在他們的DAI 預言機方面做得很好， 這裡是代碼（如果你看不出來，我認為這是歷史上寫得最好的複雜智能合約系統）。

關於預言機評估的更多內容，以及突出Euler 團隊的能力，他們寫了一篇關於計算操縱Uniswap V3 TWAP 預言機價格的好文章。

管理/ 治理

為管理實體創建不變性是最棘手。這主要是由於他們的大部分作用是去改變現有的其他不變性。也就是說，如果你能避免使用管理角色，你應該這樣做。

從根本上說，一個管理實體的核心不變性可能是：

解讀：管理員可以做一些應該結果不會破壞不變性的事情，除非他們為了保護用戶的資金而大幅改變事情（例如：將資產轉移到救援合約中是對不變性的移除）。管理員也應該被認為是一個用戶，所以核心借貸市場的用戶不變性也應該對他們成立（意味著他們不能對其他用戶或協議進行攻擊）。目前，一些管理員的行為不可能在運行時通過FREI-PI 進行驗證，但如果在其他地方有足夠強大的不變性，希望大多數問題可以得到緩解。我說目前，因為人們可以想像使用zk 證明系統可能會檢查合約的整個狀態（每個用戶、每個預言機等）。

作為一個管理員破壞不變性的例子，以發生在2022 年8 月的borked the cETH market 的Compound 治理行動為例。從根本上說，這次升級破壞了Oracle 的不變性：Oracle 提供準確和( 相對) 實時的信息。由於功能的缺失，Oracle 可以提供不對的信息。一個運行時的FREI-PI 驗證，檢查受影響的Oracle 能否提供實時信息，可以防止升級的發生這樣的情況。這可以納入_setPriceOracle，檢查所有資產是否收到實時信息。 FREI-PI 對管理角色的好處是，管理角色對價格相對不敏感( 或者至少應該是這樣)，所以更多的Gas 使用量不應該是個大問題。

複雜是危險的

因此，雖然最重要的不變性是協議的核心不變性，但也可以有一些以實體為中心的不變性，這些不變性必須為核心不變性所持有。但是，最簡單（和最小）的不變性集可能是最安全的。簡單就是好的一個光輝榜樣是Uniswap …

為什麼Uniswap 從來沒有被黑過（大概）

AMMs 可以有任何DeFi 原語中最簡單的基本不變性：tokenBalanceX * tokenBalanceY == k（例如常量乘積模型）。 Uniswap V2 中的每個函數都是圍繞這個簡單的不變性：

1. Mint：添加到k 中

2. Burn：從k 中減去

3. Swap：轉移x 和y，不動k。

4. Skim：重新調整tokenBalanceX * tokenBalanceY，使其等於k，移除多餘的部分。

Uniswap V2 的安全秘訣：核心是一個簡單的不變性，所有功能都是為它服務的。唯一可以爭論的其他實體是治理，它可以打開一個收費開關，這並不觸及核心不變性，只是代幣餘額所有權的分配。他們的安全聲明中的這種簡單性是Uniswap 從未被黑過的原因。簡單其實並不是對Uniswap 的智能合約的優秀開發者的輕視，相反需要出色的工程師來找到簡單性。

Gas 問題

我的Twitter 上已經充滿了優化論者關於這些檢查是不必要的和低效的恐怖和痛苦的尖叫聲。關於這個問題有兩點：

1. 你知道還有什麼是低效的嗎？不得不通過etherscan 向~~Laurence~~朝鮮黑客發送信息，使用ETH 轉賬，並威脅說FBI 會介入。

2. 你可能已經從存儲中加載了所有需要的數據，所以在調用結束時，只是對這些熱數據加一點點require 檢查。你想讓你的協議貴那麼一點忽略不計的費用，還是讓它死於非命？

如果成本過高，請重新考慮核心變量，並嘗試簡化。

這對我來說意味著什麼？

作為一個開發者，要在開發過程中儘早地定義並表達出核心不變性。作為一個具體的建議：讓自己寫的第一個函數是_verifyAfter，在每次調用你的合約後驗證你的不變性。把它放在你的合約中，並在那裡進行部署。用更廣泛的不變性測試來補充這個不變性（以及其他以實體為中心的不變性），這些測試在部署前就被檢查過了（Foundry guide）。

瞬時存儲開啟了一些有趣的優化和改進，Nascent 將對此進行實驗– 我建議你考慮如何將瞬時存儲作為一種工具，以實現更好的跨調用上下文更安全。

在這篇文章中，沒有花太多時間在FREI-PI 模式的介紹輸入驗證，但這也是非常重要的。定義輸入的邊界是一項具有挑戰性的任務，以避免溢出和類似情況。可以考慮查看並關注我們的工具的進展：pyrometer（目前處於測試階段，請給我們一個星星）。它可以深入了解並幫助找到你可能沒有進行輸入驗證的地方。

結論

在任何朗朗上口的縮寫（FREI-PI）或模式名稱之上，真正重要的一點是：

在你的協議的核心不變性中找到簡單性。並拼命工作以確保它永遠不會被破壞（或在它被破壞之前就被捕獲）。