Foundry-based Formal Verification | Juan Conejero (Runtime Verification) - DSS 101 2024
三句話摘要
Control形式化驗證工具的原理講解與完整使用指南。 符號執行配合循環變體才能達到完全形式化驗證，Control透過直觀的Web視圖和與Foundry的無縫整合，讓開發者用相對平易近人的方式進行嚴格的數學驗證。 形式化驗證工具的光譜
重點整理
重點- 1
形式化驗證工具的光譜
- 2
形式化驗證工具從完全自動化到完全交互式存在連續光譜。自動化工具（如Halmos）易用但反饋有限、無法處理複雜性質；交互式工具（如Lean）能驗證任意複雜性質但學習曲線陡峭、需大量人工。Control介於兩者之間，既提供自動化便利又給出詳細執行樹反饋，是務實的折衷方案。
- 3
符號執行 vs 具體執行的根本差異
- 4
具體執行（模糊測試）只能測試特定輸入值，無論測試多久都只是有限樣本。符號執行用符號變量代替具體值執行代碼，生成執行樹的每個分支都概括了許多具體測試場景，若符號執行通過即證明所有可能輸入都滿足性質。
- 5
Control的交互式驗證循環
- 6
流程為：構建程式→執行驗證生成符號執行樹→檢查樹中節點（各節點是EVM狀態快照）→基於發現編寫引理→重新構建並驗證。用戶通過檢查執行樹的具體狀態變化決定需要什麼引理，形成迭代反饋。
- 7
循環變體是突破無限循環的關鍵
- 8
BMC深度（Bounded Model Checking）只能限制循環執行次數，若惡意代碼在深度外才出現問題就無法發現。循環變體透過證明循環每次迭代前後的狀態轉換公式，一旦證明正確就能一次性涵蓋無限次迭代。這是形式化驗證最難的部分，需要理解代碼的數學性質。
實用技巧與重點
乾貨- 安裝與基本命令
- 安裝：bash命令執行K包管理器
- 替換規則：`control build` 替換 `forge build`；`control proof` 替換 `forge test`
- 測試前綴相容性：支持 `proof:` (HBN)、`check:` (HAL)，增強跨工具互操作性
- Cheat Code對應
- Control特有：SetArbitraryStorage（整個存儲符號化）、CopyStorage、MockFunction（用模型替換複雜函數）、FreshRandomU/Address/Bytes（生成新符號變量）
- Foundry新增（受Control啟發）：SetArbitraryStorage、CopyStorage、MockFunction、RandomUintInBuAddress
- 硬件需求
- 最低16GB內存（Windows子系統for Linux、Docker容器需特別檢查）
- 並行驗證每個證明分配8GB
- 主要命令選項
- `--auxiliary-lemmas` 包含輔助引理增強推理
- `--require <K文件>` 導入自定義引理
- `--bmc-depth N` 限制循環展開為N次
- `--loop-invariant` 指定循環不變量
- `--optimize-performance` 快速驗證模式
- `--branch-parallel N` 並行探索N個分支
- 查看結果工具
- `control view KCFG` 終端UI交互查看器（點擊節點查看分支）
- `control panel` 純命令行輸出
- K服務提供Web視圖（使用者友善）
- 示例程式：sumToN
- ```
- 計算0到n的和，閉合公式 = n*(n+1)/2
- 循環結構需設置BMC深度或循環變體才能完全驗證
- ```
- K語言引理寫法
- `requires` 子句導入Foundry和EVM正式定義
- `module` 包含引理集合
- `rule` 定義重寫規則
- `requires` 條件限制規則應用條件
- `simplification` 屬性標記簡化規則
- `rewrite` 符號表示狀態轉換（左側→右側）
結論
結論“符號執行配合循環變體才能達到完全形式化驗證，Control透過直觀的Web視圖和與Foundry的無縫整合，讓開發者用相對平易近人的方式進行嚴格的數學驗證。”
完整解析
詳細Control是Runtime Verification公司為以太坊生態開發的形式化驗證工具，核心創新是將符號執行引入智能合約驗證。講者Juan說明了為什麼符號執行比傳統模糊測試更強大：具體執行只能測試有限輸入組合，而符號執行用符號變量執行代碼，生成執行樹的每條分支都概括了大量具體場景，若通過則證明所有可能輸入都滿足要求。
Control的工作流程形成一個反饋循環：先用 `control build` 構建程式，再用 `control proof` 執行驗證。驗證後Control生成符號執行樹，樹中每個節點是EVM狀態的快照。用戶可用 `control view KCFG` 或Web視圖檢查節點，觀察特定執行路徑的狀態變化。基於檢查結果，用戶用K語言編寫引理（lemmas）來增強Control的推理能力，然後重新構建和驗證。這個迭代過程最終能達到完整的形式化證明。
最大的挑戰是處理循環。Control默認不限制循環迭代次數，會產生無限執行樹。解決方案有二：一是用 `--bmc-depth N` 只驗證前N次迭代（但無法捕捉深層bug）；二是編寫循環變體——即循環每次迭代前後的狀態轉換公式。講者用sumToN函數示範如何構造循環變體：觀察初始狀態（result=0, i=0）與退出時狀態（i=n, result=n*(n+1)/2）的關係，證明這個轉換對所有迭代都成立，就能一次性驗證無限次迭代。這個過程需要深入理解代碼的數學性質，是形式化驗證最難的部分。
講座強調Control的易用性優勢：它與Foundry完全相容，Foundry測試可直接轉為Control證明，支持Foundry的Cheat Code並提供自己的符號執行特化Cheat Code。硬件需求（最低16GB內存）和詳細文檔（可查詢或加入Discord社群）也是支持。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
