V for Verification, Kostas Ferles - DeFi Security Summit 2022
三句話摘要
Veridis 公司使用形式方法工具為區塊鏈應用提供代碼驗證與安全保證服務。 形式方法正從學術研究轉變為生產工具，Veridis 展示了如何將數學嚴格性與實用易用性結合，為區塊鏈安全提供可擴展的解決方案。 區塊鏈安全需求的急迫性：智能合約、共識協議、零知識證明等各層都曾發生高成本的漏洞，這種經濟損失的風險使得形式方法從學術領域走入生產環境成為必要。
重點整理
重點- 1
區塊鏈安全需求的急迫性：智能合約、共識協議、零知識證明等各層都曾發生高成本的漏洞，這種經濟損失的風險使得形式方法從學術領域走入生產環境成為必要。
- 2
形式方法的技術光譜：測試與靜態分析位於光譜一端，擅長快速發現 bug 且對用戶輸入要求最少；形式驗證位於另一端，能提供完整的正確性證明但需要更多人工投入。
- 3
VAS 平台的設計策略：通過統一的 V 規範語言和語言無關的工具核心實現易用性和可擴展性，使平台能輕鬆支持新區塊鏈和編程語言。
- 4
V 語言的表達能力：支持時態邏輯（LTL 變體）、系統不變量、複雜行為規範，能在任何執行路徑（含交易回滾等邊界情況）上驗證規範。
實用技巧與重點
乾貨- 公司名稱：Veridis
- 講者身份：Costas，首席科學家
- 公司目標：用形式方法硬化區塊鏈安全
- 形式方法類型：系統測試、靜態分析、形式驗證
- 主要產品：驗證即服務（VAS, Verification as a Service）
- 規範語言：V 語言，支持 LTL 變體
- 已有成就：內部審計發現閃電貸漏洞、零知識證明健全性 bug
- 近期發布計劃：
- 改進版 VAS 服務（今年）
- Pus（電路通用漏洞檢測器）
- Circum（電路功能正確性驗證工具）
- Devcon 十月舉辦相關講座
結論
結論“形式方法正從學術研究轉變為生產工具，Veridis 展示了如何將數學嚴格性與實用易用性結合，為區塊鏈安全提供可擴展的解決方案。”
完整解析
詳細區塊鏈生態面臨的根本性安全挑戰是：每一個漏洞都可能造成巨額經濟損失。Costas 指出，這些漏洞不限於智能合約，而是可能出現在堆棧的任何層級——從共識協議到零知識證明系統。正是因為這種高風險、高成本的特性，形式方法這套數學上嚴格的技術從學術象牙塔走入實用，成為區塊鏈安全的重要工具。
形式方法並非單一技術，而是一個完整光譜。光譜的一端是系統測試和靜態分析，這些方法擅長快速發現 bug，對用戶的輸入要求最少。光譜的另一端是形式驗證，它能對代碼的正確性提供數學證明，但代價是需要更多人工投入——用戶必須用專門的規範語言明確描述所需行為。
Veridis 的核心產品「驗證即服務」（VAS）建立在這個理解上。工作流程如下：用戶提交代碼，並用 Veridis 設計的 V 語言編寫正式規範，描述代碼應該做什麼。平台隨後運行所有適用的工具，檢查規範是否得到滿足，並為任何違規規範提供具體的反例。設計核心是易用性和可擴展性——通過統一的 V 語言界面和語言無關的工具核心，Veridis 能輕鬆添加對新區塊鏈和編程語言的支持。
V 語言本身具有相當表達能力。除了基礎規範（如「存款方法成功調用後，餘額應增加指定金額」），V 語言還支持時態邏輯變體，允許用戶指定任何可能執行路徑上的行為，包括交易回滾等邊界情況。用戶還可描述系統不變量和複雜行為規範。迄今，Veridis 已用這套工具進行多次內部審計，發現了從去中心化應用的閃電貸漏洞到零知識證明的健全性 bug 等多種問題。
未來規劃展示公司視野超越傳統智能合約。今年將發布改進版 VAS 服務，並推出針對零知識系統的新工具，包括 Pus（電路通用漏洞檢測器）和 Circum（電路功能正確性驗證工具）。這表明公司正在擴展到整個區塊鏈安全生態。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
