Formally verifying Morpho - Quentin Garchery, DeFi Security Summit 2023
三句話摘要
形式化驗證在 DeFi 協議中的應用，以 Morpho 借貸優化器為例說明如何用數學方法確保智能合約的正確性。 形式化驗證通過將代碼與數學規範嚴格匹配，成為 DeFi 時代不可繞過的安全防線，尤其當協議涉及複雜交互和大額資金時更為關鍵。 形式化驗證的核心概念：區別於非正式文檔，形式化驗證要求用數學語言精確定義程序應該做什麼，然後用自動化工具驗證代碼實際是否符合這個規範。例如不只說「返回有效值」，而是明確定義「對每個輸入 X，函數 F 應用於 X 時返回值大於 10」。
重點整理
重點- 1
形式化驗證的核心概念：區別於非正式文檔，形式化驗證要求用數學語言精確定義程序應該做什麼，然後用自動化工具驗證代碼實際是否符合這個規範。例如不只說「返回有效值」，而是明確定義「對每個輸入 X，函數 F 應用於 X 時返回值大於 10」。
- 2
Morpho 的設計邏輯：傳統借貸池因借款人少導致利差大（供應方年收益率遠低於借款方），Morpho 在其上層實現點對點配對，讓雙方在利率上「各讓一步」，同時提供備用方案和持續供給機制應對單方退出。
- 3
為何 DeFi 特別需要形式化驗證：三個關鍵原因——智能合約規模相對小且代碼開源易讀，管理的資金量龐大要求高可靠性，區塊鏈無法改寫歷史意味著錯誤永久存在，因此必須「第一次就做對」。
- 4
驗證工具的分工：Certora 擅長驗證數據結構與代碼優化的等價性；Why3 是通用驗證工具可驗證複雜邏輯（如迴圈任意次迭代）但需轉換語言；Halmos 與 Forge 深度整合提供符號執行能力，用於驗證數據結構不變性。
實用技巧與重點
乾貨- Morpho 優化器的核心機制：
- 傳統池：供應年收益率 < 借款年收益率（原因：借款人少）
- Morpho 方案：點對點配對 → 將利率設在中間值 → 雙方都獲利
- 需要備用機制應對單方退出和持續供給
- 三套驗證工具及應用場景：
- Certora
- 用途：數據結構驗證、優化版本等價性驗證
- Morpho Token 案例：驗證只有「設置用戶角色」函數能改變用戶的角色屬性
- 規則寫法：存儲初始布爾值 → 執行任意函數 → 存儲最終布爾值 → 如布爾值變化則必為特定函數調用
- Why3
- 特性：通用驗證工具、演繹驗證、可驗證迴圈任意次數迭代
- Morpho 案例：證明協議清算不變性——供應量 × 清算閾值 ≥ 實際借款額
- 難點：處理算術運算和舍入誤差
- Halmos
- 特性：與 Forge 模糊測試深度整合，Forge 測試可直接在 Halmos 上運行
- Morpho AAVE3 案例：驗證「桶」數據結構（範圍邊界為 2 的冪連續倍數）
- 驗證內容：邊界確實為 2 的冪，所有值都在邊界內
- 驗證程序的三步流程：
- 制定正式規範
- 應用形式化驗證工具（自動生成驗證條件）
- 驗證條件（有時需手工完成，如 2000 行代碼的驗證條件）
- 演講中提到的時間與資源：
- 完整驗證所有內容：可能需要數年
- 專注核心協議邏輯驗證：可快速完成
- 驗證時間取決於：對協議的理解深度、可用工具、驗證深入程度
- 跨協議驗證的策略：
- 從小處著手：先驗證依賴協議的模擬版本
- 建立規範分離：依賴協議需遵循特定規範，再用該規範驗證實際協議
- 工具支援：Certora 提供調度器機制明確指定依賴關係
結論
結論“形式化驗證通過將代碼與數學規範嚴格匹配，成為 DeFi 時代不可繞過的安全防線，尤其當協議涉及複雜交互和大額資金時更為關鍵。”
完整解析
詳細Morpho 是建立在現有借貸協議（如 Compound、Aave）上的點對點優化層。傳統借貸池存在利差問題：因為借款人通常少於供應方，所有借款利息必須在眾多供應方間分配，導致供應者獲得的年收益率遠低於借款者支付的年收益率。Morpho 通過在協議上層實現點對點配對機制解決這一問題——當供應方和借款方的金額匹配時，雙方可自行決定利率，Morpho 優化器將利率設在中間值，使借款人支付更少利息，供應方賺取更多收益，實現雙贏。但這個設計引入額外的智能合約層，帶來額外風險，因此需要嚴格的安全措施。
形式化驗證是解決這類風險的關鍵技術。它本質上是數學與計算機科學的交集，核心理念是用嚴格的數學方式確保代碼與其規範完全匹配。傳統代碼文檔往往不夠精確——例如「返回有效值」這樣的描述模糊不清，而形式化規範要求精確定義每個條件，比如「對所有輸入 X，若 X 大於 2，則函數返回值必須大於 10」。一旦制定了正式規範，驗證工具會自動生成驗證條件（一個數學公式），通過驗證這個公式，就能保證代碼符合規範。
DeFi 領域特別適合使用形式化驗證，主要有三個原因。首先，以太坊智能合約規模相對較小且代碼開源，具有高可讀性，有利於進行形式化推理。其次，DeFi 協議往往管理龐大資金量，必須確保高度可靠性。第三，也是最關鍵的，區塊鏈無法改寫歷史意味著智能合約的任何錯誤都將永久存在於鏈上，因此「第一次就做對」至關重要。
Morpho 使用了三套專業驗證工具，各有側重。Certora 擅長驗證數據結構和優化版本的正確性，例如驗證 Morpho Token 中只有特定函數能修改用戶角色。Why3 是通用驗證工具，不限於 Solidity，能驗證複雜的協議邏輯，如證明 Morpho 在清算時不會被底層協議清算掉——這需要驗證供應量乘以清算閾值永遠大於實際借款額，涉及算術和舍入誤差的處理。Halmos 則與 Forge 模糊測試框架緊密整合，用於驗證數據結構不變性，例如確保 AAVE3 中的「桶」數據結構（用 2 的冪邊界分割範圍以提升效率和公平性）的邊界確實遵循預期規則。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
