DeFi security Summit 2023 - Session 14: Formal Verification Panel
三句話摘要
形式驗證在Web3智能合約安全性中的應用與實踐指南。 形式驗證是提升Web3安全性的必要手段，但應配合屬性測試、模糊測試、審計等多層防禦，重點在於驗證規範正確性而非代碼，並持續集成到開發生命週期中。 形式驗證解決Web3的特有風險。Web3漏洞利用涉及金錢盜竊，修復需要複雜升級流程。代碼開源意味著更多攻擊者審視，形式驗證提供嚴格的數學證明確保安全性，遠優於人工審查。
重點整理
重點- 1
形式驗證解決Web3的特有風險。Web3漏洞利用涉及金錢盜竊，修復需要複雜升級流程。代碼開源意味著更多攻擊者審視，形式驗證提供嚴格的數學證明確保安全性，遠優於人工審查。
- 2
形式驗證不能替代其他安全手段。最佳實踐是分層防禦：早期用靜態分析和模糊測試發現淺層bug，對存儲資金、資金路由等安全關鍵組件進行形式驗證，部署後繼續監控。每層都有盲點，綜合使用才能達到完整安全覆蓋。
- 3
開發者和審計員角色不同。開發者應在開發週期早期使用屬性測試和模糊測試，這些工具易學易用（Foundry框架已整合）；審計員需深入專業驗證，使用形式驗證工具和規範檢查發現開發者遺漏的漏洞，並整合驗證到持續整合流程中。
- 4
規範驗證比代碼驗證更重要。規範本身也可能有bug（Maker曾遇到規範與代碼同時出現相同bug的情況），因此應多人審查規範、運行變異測試、修改Solidity代碼驗證規範完整性。審計員應審核規範而非代碼，並確認部署到鏈上的字節碼與規範一致。
實用技巧與重點
乾貨- Web3形式驗證的優勢
- 代碼量小、成本高、開源透明
- 支援驗證智能合約、零知識證明電路、區塊鏈實現
- 比Web2（瀏覽器、操作系統）容易應用
- 現有工具與框架
- Foundry：整合屬性測試、模糊測試、符號執行
- Certora Prover：智能合約形式驗證
- Lean、Coq：零知識電路驗證的證明助手
- SMT求解器：形式驗證基礎設施
- 驗證方法分層
- 開發階段：屬性測試、模糊測試
- 輕量級驗證：靜態分析、基於屬性的測試
- 深度驗證：形式化驗證（交互式定理證明或符號執行）
- 專案應用方式
- 自行編寫規範（需專業團隊）
- 雇用專業公司編寫規範並維護
- 混合方式：公司編寫規範，內部團隊維護
- 規範驗證品質保證
- 多人審查規範
- 對規範進行變異測試
- 修改Solidity代碼驗證規範捕獲能力
- 設置內部基準測試集
- 驗證部署到區塊鏈的實際字節碼
- 縮放策略
- 組件分離驗證（分而治之）
- 抽象建模（如Zero Risk ZK電路驗證數十萬約束）
- 持續集成流程重複驗證（代碼更新時重新運行驗證）
- 經濟模型驗證
- 運行時驗證而非代碼驗證
- 形式化業務邏輯與共識協議
- 證明協議不會分叉等經濟屬性
- 建立抽象高層模型供其他協議參考
結論
結論“形式驗證是提升Web3安全性的必要手段，但應配合屬性測試、模糊測試、審計等多層防禦，重點在於驗證規範正確性而非代碼，並持續集成到開發生命週期中。”
完整解析
詳細Web3生態系統成為形式驗證最佳實驗場景，源於其特有的風險特徵。相比傳統軟體，智能合約漏洞代價極高——漏洞利用直接導致資金盜竊，且修復路徑複雜（涉及合約升級、多簽授權等治理流程）。同時Web3代碼開源，意味著全球攻擊者都在審視尋找漏洞。正是這些特點決定了形式驗證在此領域的核心價值：通過數學證明而非人工檢查，嚴格確保代碼邏輯符合預期條件。
然而，形式驗證並非銀彈。專家共識強調分層防禦。開發者在早期應使用屬性測試和模糊測試發現淺層邏輯錯誤——Foundry等現代框架已將符號執行集成其中，使開發者無需深入形式驗證理論即可受益。關鍵洞察是：屬性測試並非表達力弱，反而極強且易用，能表達任何三元組（前置條件、後置條件、假設和斷言），而黑客本質上就是通過屬性來思考攻擊，因此開發者也應這樣思考防禦。
審計員職責不同。他們應在開發完成後部署形式驗證工具深化審計，並檢查開發者是否遺漏的極端情況。持續整合流程至關重要——每次代碼變更都重新運行驗證，成本遠低於完整重審。但形式驗證涉及編寫規範，而規範本身也有bug風險（Maker經歷過規範與代碼同時出現相同漏洞）。防護方式包括：多人審查規範、運行變異測試觀察規範是否捕捉異常、甚至修改Solidity代碼驗證規範的完整性。審計員應專注於審核規範而非代碼，並驗證部署到區塊鏈的實際字節碼與規範一致。
縮放性挑戰並非不可逾越。隨著智能合約和零知識電路規模增長，業界採用組件分離驗證和抽象建模。硬體驗證領域已驗證整個晶片；零知識電路驗證已處理數十萬約束的系統。關鍵是將大系統分解為組件，各自獨立驗證，上層只需驗證組件間交互邏輯。這種方式還帶來額外收益：抽象規範可供其他協議參考，避免盲目複製合約導致的潛在bug。經濟模型驗證亦然——形式化業務邏輯和共識協議屬性（如"協議不會分叉"），無需查看任何代碼行。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
