DeFi invariants: Examples and Challenges, Anton Permenev - DeFi Security 101 2023

Chain Security是智能合約安全審計領域的資深參與者，自2017年成立以來保持高度的團隊穩定性。講者Andrew在演講中強調了一個對審計師和開發者都至關重要的思維工具——「不變式」，即程序某個性質在任何情況下都應保持為真的概念。

最直觀的例子是ERC20代幣的供應量守恆：所有持有者的餘額之和必須等於代幣總供應量。這看似簡單的性質實際上是代幣合約最核心的信任基礎。當審計ERC20代碼時，審計師只需檢查每個涉及轉賬或鑄造的函數是否保持了這個不變式。

但在借貸協議Compound中，不變式變得複雜得多。Compound由三個元素構成：DAI是外部穩定幣、cDAI是Compound內部憑證代幣、COMP是治理代幣。供給方將DAI存入協議，獲得cDAI作為持份證明，隨著時間推移cDAI可以兌換越來越多的DAI（利息積累）。借款方則需提供其他代幣作為抵押品，以此換取DAI借款並承諾支付額外費用。

Compound最基礎的不變式是：系統內的價值不會憑空產生。貸款人的所有收益都精確來自借款人支付的費用。如果你用公式表示，系統的流入應該等於流出：借入供給 + 償還借款 = 提供供給 + 收取費用。這個零和遊戲的設計確保了協議的可持續性——沒有人在透支未來的收益。

隨著時間推移，當借款人的抵押品價值下降時，協議需要一個清液機制來防止風險。這裡引入了另一個關鍵角色——清液人。清液人可以通過償還部分借款來清償風險頭寸，作為交換獲得價值更高的抵押品。協議設定的抵押率（通常為0.8或80%）確保了清液人的激勵始終存在。具體來說，當抵押品數量乘以其價格乘以抵押率小於需要償還的金額時，清液人缺乏激勵，此時協議面臨壞賬風險。因此不變式變為：抵押品價值應始終足以激勵清液介入。

Andrew強調，理解這些不變式對審計和開發同樣重要。傳統的單元測試只檢驗一個或少數輸入值，容易遺漏邊界情況。更有效的方法是「基於屬性的測試」——用數千個隨機輸入轟炸函數，每次都驗證相同的屬性是否保持。為輸入參數設定範圍（如最小值、最大值），測試框架會自動生成邊界值進行檢驗。此外，還可以針對特定場景設計測試，例如測試「當抵押率恰好為1時」或「當跨越流動性池邊界時」這類极端情況。

更高級的測試方法是形式化驗證。它不是用具體的數值進行測試，而是將系統規範轉化為數學公式，用符號和邏輯推導來證明函數對於所有可能的輸入都成立。這提供了最強的數學保證，但成本和複雜度也最高，主要適用於協議層面的關鍵邏輯。

最後談到監控，Andrew指出現有的挑戰在於黑客可以通過MEV服務隱藏交易，使監控往往發現得太晚。有效的監控必須與協議設計相結合，例如設置限流器防止异常流量、安裝斷路器在檢測到異常後立即停止交易。Maker的Teleporter合約就是這樣的例子，它限制了從Optimism到主網的代幣吞吐量。單純的事後監控不足以防止攻擊，只有在設計階段就考慮應急機制，監控才能真正發揮作用。