Formal Verification of Foundry Tests, Everett Hildenbrandt - DeFi Security Summit 2022
三句話摘要
Foundry 測試框架如何透過 KEVM（K framework）進行形式化驗證，以及性能最佳化的進展。 形式化驗證正透過自動化工具與性能最佳化邁向實用化，未來幾個月的性能改進將使 KEVM 足以驗證複雜的區塊鏈協議邏輯。 Foundry 的測試設計簡潔高效：透過 setup 初始化狀態，test 前綴函數搭配模糊測試參數，能在短時間內用數百種參數組合驗證邏輯。這種方式無須對合約插樁，只在運行時最小化干擾。
重點整理
重點- 1
Foundry 的測試設計簡潔高效：透過 setup 初始化狀態，test 前綴函數搭配模糊測試參數，能在短時間內用數百種參數組合驗證邏輯。這種方式無須對合約插樁，只在運行時最小化干擾。
- 2
形式化驗證的自動化轉換：KEVM 能自動將 Foundry 測試編譯為 K 規範，免除手寫形式化規範的負擔。但生成的規範規模龐大（曾見 23000 行），需編譯 2 分鐘才能成為機器可讀的 Core 代碼。
- 3
性能瓶頸與改進策略：KEVM 當前比 Foundry 慢 3-4 個數量級（如求和到 20 萬測試，Foundry 需 10 秒，KEVM 遠超此時間），但新的基於語義的編譯方式將性能提升 2 個數量級，使兩者差距收窄至可接受範圍。
- 4
符號執行的實質突破：新性能改進除適用全部案例語義，也同時加速符號執行。可達到用相同時間計算數千個結果（原本只能計算 10 個），對複雜驗證屬性極為關鍵。
實用技巧與重點
乾貨- 工具與框架：
- Foundry：Solidity 測試框架
- KEVM：K framework 的 EVM 實現
- K framework：形式化驗證框架
- 資源：kframework.org、Discord 服務器、Twitter 帳號（RV Inc）
- 性能數據：
- Foundry 求和到 20 耗時：364 微秒
- Foundry 求和到 20 萬耗時：10 秒
- KEVM 與 Foundry 當前速度差：3-4 個數量級
- 新性能改進：提升 2 個數量級
- 改進後差距：1 個數量級
- 技術步驟：
- 編寫 Foundry 測試（setup + test 函數）
- 執行模糊測試（Forge Test 自動運行多組參數）
- 使用 `KVM Foundry Decay` 生成 K 規範
- 編譯規範為 Core 代碼（約 2 分鐘）
- 調用 KVM prove 函數驗證規範
- 開發進度：
- 已支持 1 個 cheatcode，已提交 PR 支持接下來 8 個最常用 cheatcode
- 需支持 setup 函數（預計數週時間）
- 性能改進將於未來數月推出
結論
結論“形式化驗證正透過自動化工具與性能最佳化邁向實用化，未來幾個月的性能改進將使 KEVM 足以驗證複雜的區塊鏈協議邏輯。”
完整解析
詳細Foundry 是現代 Solidity 開發的主流測試框架，其核心優勢在於簡潔的設計與快速的執行。一個典型的 Foundry 測試套件由 setup 函數與多個 test 前綴的函數組成。Setup 函數負責初始化測試場景，而各個測試函數可接收由框架自動生成的參數值。Foundry 的模糊測試機制會對這些參數進行自動化掃描，用不同的輸入值多次運行同一測試，以確保邏輯在各種場景下都能成立。例如一個簡單測試可能只運行一次，但同樣的測試啟用模糊測試後，會自動在 256 組不同參數下執行。這種輕量級的插樁方式（只在運行時最小化干擾，不對合約本身進行插樁）使 Foundry 能保持極高的執行速度。
然而，快速的單元測試並不能保證合約邏輯在所有邊界情況下都符合預期。這正是形式化驗證發揮作用的地方。KEVM（K framework 對 EVM 的實現）能將 Foundry 測試自動轉換為形式化規範，進而進行數學上嚴格的驗證。講者的團隊開發了 `KVM Foundry Decay` 工具，自動從 Foundry 測試套件生成 K 規範代碼。然而這個過程面臨挑戰：即使簡單的測試套件也會產生巨大的規範（曾見 23000 行 K 代碼），且這些規範需要編譯成機器可讀的 Core 代碼，通常耗時約 2 分鐘。編譯完成後，KEVM 的 prove 函數會驗證這些規範，若驗證通過則返回真，若失敗則需要專家級調試。
性能一直是形式化驗證的瓶頸。講者公開了關鍵數據：Foundry 執行求和到 20 的測試耗時 364 微秒，求和到 20 萬則需 10 秒。同一測試在 KEVM 上運行慢了 3-4 個數量級。這種性能差異曾令人望而卻步，但團隊正在推出重大改進。透過新的基於語義的編譯方式，性能改進幅度達 2 個數量級，此改進不僅適用於 EVM 語義，也適用所有案例語義，並同時加速符號執行。改進後，KEVM 與 Foundry 的差距將縮至 1 個數量級，使得形式化驗證在實用性上變得可行。更重要的是，符號執行能力大幅躍進：相同時間內可計算數千個結果，而之前同樣時間只能計算 10 個。
當前仍有工作待完成：團隊已實現 1 個 cheatcode 支持，已提交 PR 支持接下來 8 個最常用的，還需實現 setup 函數支持（預計數週）。後續焦點轉向性能最佳化。講者邀請社群參與，可透過 kframework.org 完成教程（通常需 2 週），或在 Discord 與 Twitter（RV Inc）跟進進展。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
