DeFi Security 101 2023 - 11 - Ernesto Boado

Aave 協議的複雜性遠超大眾對「流動性協議」的認知。它不僅提供借貸功能，而是一個完整的金融生態，包含五大子系統：核心流動性協議讓用戶質押資產並借貸；治理系統控制協議升級和決策；智能合約部署系統執行治理決議；激勵管理系統分配獎勵；安全模組在協議遭攻擊時通過扣除代幣來補償。這種多層結構加上用戶可選擇啟用/停用抵押品這類非對稱性設計，導致系統的狀態空間呈指數級增長。開發團隊的坦誠承認是關鍵：系統上線後，他們對自己構建的系統的理解度只有 50%，剩下的 50% 由真實用戶的使用方式決定。

正因為這種根本的不可預測性，傳統的安全檢查流程——單元測試、集成測試、同行評審、外部審計——都陷入了同一個窘境：它們依賴開發者和審計者主動想象邊界情況。但在指數級的狀態空間中，這種「想象式」檢查必然遺漏。即使是頂級安全公司也會遺漏某些場景，因為那些邊界情況往往源自開發者從未想過的狀態組合——這被稱為「隱蔽錯誤」。

形式驗證提供了根本不同的保證機制。它要求開發者不是預測邊界情況，而是定義系統在任何情況下都必須滿足的數學性質（例如「代幣總供應量不變」「用戶余額非負」）。然後工具自動驗證代碼是否可能違反這些性質。這種方法的妙處在於：它不依賴於開發者的想象力，而是依賴於系統的根本約束。一個屬性檢查可以替代數百個手工編寫的測試場景，因為它覆蓋的是所有可能的代碼執行路徑，而非枚舉式的測試用例。

採用形式驗證還改變了開發實踐本身。在編寫代碼之前，開發者被迫用自然語言定義系統應該滿足的屬性。這似乎是額外工作，但實際上它促進了更清晰的思維：團隊成員圍繞屬性進行討論，達成對系統行為的共識。更重要的是，屬性檢查不是事後的驗收測試，而是整合在開發流程中的——每當有人提交 PR，屬性檢查會立即運行，若發現改動破壞了某個屬性，整個團隊會立即知道。這種「早期發現」的威力在複雜系統中尤其明顯。開發者在高層次思考時往往忽視低層次的狀態轉移細節（比如遺漏某個鍵的初始化），但屬性檢查會毫不留情地指出每一個不變性違反。對於需要頻繁升級的系統（如 Aave Token），這種保證尤其寶貴，因為大規模重構時開發者有信心知道自己是否意外破壞了什麼。

然而，形式驗證並非銀彈。演講者強調了明確的適用邊界。首先是記賬系統（代幣轉帳、流動性池）：這類系統的邊界情況有限但難以測試——例如浮點精度問題、溢出、餘額不一致。形式驗證可以數學上保證這些永遠不會發生。其次是複雜的資產流動系統（如 Aave 內部五個協議間的資金轉移）：可以定義清晰的全局平衡約束（「流入=流出」），形式驗證會確保任何代碼改動都不會破壞這個約束。相反，三類場景不值得投入：純任意邏輯系統（無法定義有意義的屬性，因為什麼都可能發生）；跨鏈互操作性複雜的系統（設置本身就複雜，邊界難以定義）；小型治理提案的執行邏輯（成本高但收益低）。這要求開發者精準評估，而非盲目全面應用。