Capture the Spec (Competition) | Tomer Ganor (Certora) - DSS 101 2024
三句話摘要
DSS期間舉辦的Solidity多重簽名合約開發競賽，參賽者需基於預定CVL規範編寫智能合約。 通過提供完整CVL規範反向設計合約，這場競賽實踐展示了形式驗證如何在安全需求高的場景中大幅提升開發效率——事前規範設計好的代碼驗證速度遠快於事後測試。 反向開發流程：通常工作是根據客戶代碼編寫CVL規範，本次比賽反向進行——講者提供完整CVL規範，參賽者需編寫符合規範的Solidity合約，降低參賽門檻。
重點整理
重點- 1
反向開發流程：通常工作是根據客戶代碼編寫CVL規範，本次比賽反向進行——講者提供完整CVL規範，參賽者需編寫符合規範的Solidity合約，降低參賽門檻。
- 2
多層規範保證：提供三類規範文件——規則規範（描述系統合約流程）、不變性規範（驗證器數組唯一性等）、健全性規範（確保實現真實功能，防止空實現通過）。
- 3
實現自由度與約束平衡：參賽者可自由編寫Solidity代碼和優化實現，但不能修改CVL文件，且建議添加來自CVL的屬性列表和系統描述。
- 4
形式驗證的實用價值展示：透過完整規範設計，展現事前編寫好規範能大幅加快開發速度——無需傳統測試，代碼通過CVL驗證即可確保安全性。
實用技巧與重點
乾貨- 獎金設置
- 前3個通過驗證且獨一無二規範的提交：各1000美元
- 最高效代碼實現額外獎勵：500美元
- 最快解決特定屬性的方案：500美元
- 規範文件
- 規則規範（.spec CVL文件）：描述系統合約流程
- 不變性規範（CVL文件）：多項系統不變性（如驗證器數組唯一性）
- 健全性規範：驗證實現功能真實性
- 多重簽名空合約（Sol文件）：包含需實現的外部函數
- 技術要求
- 代碼必須編譯
- 包含清晰註釋
- 無bug
- 驗證時間不超過15分鐘
- 不修改CVL規範文件
- 支持渠道
- 仓库README：包含所有問題答案
- Telegram支持頻道：規範缺失內容補充
- 截止時間
- 提交截止：9號晚上
結論
結論“通過提供完整CVL規範反向設計合約，這場競賽實踐展示了形式驗證如何在安全需求高的場景中大幅提升開發效率——事前規範設計好的代碼驗證速度遠快於事後測試。”
完整解析
詳細本次比賽創新性地反轉了智能合約形式驗證的通常流程。在正常工作中，工程師根據客戶提供的Solidity代碼和設計需求編寫CVL（Certora Verification Language）規範，這個過程學習難度大、門檻高。而此次競賽正好相反——講者團隊已經編寫完整的CVL規範和不變性定義，參賽者只需用熟悉的Solidity代碼實現功能即可。
規範體系包含三層。規則規範文件描述多重簽名合約應有的流程邏輯；不變性規範則定義了系統必須始終滿足的性質，例如驗證器數組中任意兩個點的所有驗證器都必須不同；健全性規範則是一道「防作弊關卡」，它檢驗參賽者是否真正實現了功能，而非提交空實現或無意義的代碼——若只是回滾操作什麼都不做，健全性規範會因為沒有任何行為發生而失敗。
參賽者獲得包含外部函數接口定義的空合約框架，可自由編寫任何Solidity代碼，但嚴禁修改CVL文件（因為最終評測會用講者的官方規範版本進行驗證）。講者建議參賽者基於CVL派生出屬性列表、撰寫系統描述文檔，這些對理解需求、加速開發很有幫助。這個過程模擬真實開發場景：在短時間內（約兩天）設計和實現一個安全系統，但與傳統開發不同的是，無需進行繁瑣的測試流程——只要代碼通過CVL驗證，就等同於形式上證明了其正確性。
獎勵機制鼓勵多個維度的優化。前三個成功提交獨一無二規範的團隊各獲1000美元；另有兩個500美元的加分獎項，分別獎勵最高效的代碼實現和最快解決特定屬性的方案。不過所有獎項都有前提：必須通過所有規則驗證。提交截止日期為9號晚上，所有支持資料（倉庫、README、Telegram頻道）都已準備就緒。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
