Streamlining Security Audits with AuditHub - DeFi Security Summit 2025
三句話摘要
Veridise 發布 Audit Hub 安全審計平台，整合靜態分析與模糊測試工具，協助 DeFi 與 ZK 電路漏洞發現與審計流程管理。 Audit Hub 最值得記住的價值在於：將靜態分析（DeFi/ZK Vanguard）與模糊測試（Orca）整合進單一審計協作平台，讓形式化方法從學術概念變成可點擊執行、結果即時可追蹤的工程工具，同時透明化的協作流程也讓客戶與審計員雙方都受益。 審計流程碎片化是根本痛點：傳統審計需跨多個通訊管道（Slack、Email、PDF 報告）同時協調審計員、客戶與工具，認知負擔極高。Audit Hub 將所有行為收斂在單一平台，客戶得以即時追蹤審計進度而非等待期末 PDF。
重點整理
重點- 1
審計流程碎片化是根本痛點：傳統審計需跨多個通訊管道（Slack、Email、PDF 報告）同時協調審計員、客戶與工具，認知負擔極高。Audit Hub 將所有行為收斂在單一平台，客戶得以即時追蹤審計進度而非等待期末 PDF。
- 2
跨過程除法先乘問題是 Slither 盲區：Resupply Finance 的 1000 萬美元漏洞根因是「除法結果存入 storage 後再被乘法使用」，Slither 雖有除法先乘偵測器，但無法跨函數追蹤中間有 storage 操作的情況；DeFi Vanguard 支援自訂偵測器，可明確描述跨過程 storage 讀寫路徑來補上這個盲區。
- 3
靜態分析 + 模糊測試組合驗證可行性：靜態分析器可能回傳誤報，Orca 模糊測試器透過宣告式規範（如「三個函數結束後用戶必須有償付能力」）自動生成反例，驗證靜態分析警告是否真的可被利用，兩者互補。
- 4
形式化方法工具具備確定性保證：若靜態分析器回報某錯誤模式不存在，即代表程式庫確實沒有該錯誤；若 Pyus 驗證器確認電路受到適當約束，即視為形式化認可，不同於傳統審計的主觀判斷。
實用技巧與重點
乾貨- Resupply Finance 損失：約 1000 萬美元（oracle 操縱 + 精度損失複合攻擊）
- 漏洞模式：除法結果截斷為 0 → 存入 storage 變數 → 傳遞至破產函數 → LTV 恆為 0 → 所有用戶永遠有償付能力
- 工具一：ZK Vanguard — ZK 電路靜態分析器，偵測約束不完整問題
- 工具二：DeFi Vanguard — Solidity 靜態分析器，支援自訂偵測器（custom detectors）
- 工具三：Orca — 規範模糊測試器（guided specification fuzzer），接受部署腳本 + 宣告式規範
- Risk Zero 審計結果：Pyus 找到 9 個非確定性電路（non-deterministic circuits），多數為嚴重或高危
- 合作案例：Sustain（開發期間使用，非審計期間）
- 平台功能：程式碼行級對話、工具結果儀表板、誤報根因標記（系統自動傳播至後續掃描）、問題管理（含公開/私密對話分離）
- 文件資源：Audit Hub 文件網站、OpenAI 平台上的「audit hub GPT」自訂 ChatGPT
- 存取方式：Discord 伺服器、掃描 QR Code 填寫 Email/姓名即可試用
- 底層理論：形式化方法（Formal Methods）學術分支；中間表示（IR）統一降低多個 DSL/框架
結論
結論“Audit Hub 最值得記住的價值在於：將靜態分析（DeFi/ZK Vanguard）與模糊測試（Orca）整合進單一審計協作平台，讓形式化方法從學術概念變成可點擊執行、結果即時可追蹤的工程工具，同時透明化的協作流程也讓客戶與審計員雙方都受益。”
完整解析
詳細Veridise 是一家專注於 DeFi 與 ZK 安全的審計公司，多年來除了替客戶做人工審計，也在內部開發了一系列自動化工具。隨著業務量增加，他們發現傳統審計流程存在嚴重的協作斷層：審計員需同時透過多個通訊管道與客戶互動、在內部協調不同審計員的進度、並行跑外部靜態分析工具，還要記住哪個修復對應哪個問題。對客戶而言，審計過程幾乎是黑箱，只能在最後收到一份 PDF 報告。這些問題促使 Veridise 決定自行開發 Audit Hub 平台。
Audit Hub 的設計理念是讓「安全審計」成為一個透明且可追蹤的協作過程。平台以專案為單位組織內容，提供程式碼閱覽器讓審計員可以在任何程式碼片段上發起對話串，並整合工具執行入口（目前為 DeFi Vanguard、ZK Vanguard、Orca）。工具執行結果直接呈現在儀表板，審計員可以標記誤報根因，系統會自動將同樣根因的警告傳播消除，甚至在後續掃描中記住這些判斷。問題管理模組則支援公開頻道（客戶可見）與私密頻道（僅審計員可見）分離，讓溝通層次清晰。
在技術能力展示上，講者以 2024 年中的 Resupply Finance 1000 萬美元駭客事件為例，說明 Audit Hub 如何偵測此類漏洞。該漏洞的根因是一個跨函數的精度損失：oracle 回傳極高價格，除法結果被截斷為零後存入 storage，後續乘法引用此值，導致 LTV 恆為零，讓所有用戶在任何情況下都被判定為有償付能力。這種「先除後乘但中間有跨過程 storage 操作」的模式是 Slither 的盲區，但 DeFi Vanguard 支援使用者編寫自訂偵測器，可精確描述「寫入 storage 的除法 → 讀取同一 storage 的乘法」這條跨過程路徑。靜態分析找到候選警告後，再透過 Orca 模糊測試器提供宣告式規範（使用者只需聲明「哪些函數結束後用戶應有償付能力」），系統便自動生成能打破該規範的反例，確認漏洞可被真正利用。
ZK 電路方面，平台提供 ZK Vanguard 靜態分析器與 Pyus 驗證器，均以形式化方法為基礎。Pyus 的核心價值在於確定性：若它找不到反例，即代表電路已被正式驗證；若找到，則返回具體輸入使電路產生多個輸出，精確定位約束缺失位置。在 Risk Zero 審計中，Pyus 共找到 9 個非確定性電路，其中多數為嚴重或高危等級，是該次審計中表現最突出的「審計員」。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
