Off-Chain But Not Off Radar - DeFi Security Summit 2025
三句話摘要
Runtime Verification CEO 分享加密基礎設施審計（編譯器、節點、VM、共識協議）的實戰技術與最佳實踐。 --- 基礎設施審計的核心是「分層擴展」：用短週期人工審計聚焦關鍵代碼，用 AI 補足覆蓋盲區，用差分模糊測試捕捉實作分歧，再選擇性地以形式化驗證提供最高安全保證——而一份清晰的規格說明，是貫穿所有環節的最重要加速器。 基礎設施審計與智能合約審計的核心差異是規模。智能合約幾千行即為完整專案，但 Ethereum/Solana 客戶端動輒數十萬行，加上語言差異（Rust/Go/C++）和不同的威胁模型（鏈分裂、DoS、記憶體耗盡），需要完全不同的審計策略。
重點整理
重點- 1
基礎設施審計與智能合約審計的核心差異是規模。智能合約幾千行即為完整專案，但 Ethereum/Solana 客戶端動輒數十萬行，加上語言差異（Rust/Go/C++）和不同的威胁模型（鏈分裂、DoS、記憶體耗盡），需要完全不同的審計策略。
- 2
採用「短週期輪迴審計」比一次性長期審計更有效。6-8 週一輪的集中審計可避免審計員疲勞，同時給開發團隊時間修復上一輪問題，再進入下一輪，形成正向循環。
- 3
差分模糊測試是發現客戶端實作分歧的高效手段。同時運行同一條鏈的不同客戶端實作，比對所有輸入下的行為是否一致，能識別出若任一節點拒絕有效交易就可能導致鏈分裂的高危漏洞。
- 4
提供具體規格說明能大幅提升 AI 輔助審計的效果。若只讓 AI 自行尋找漏洞，效果有限；但若同時要求 AI 比對代碼與規格之間的差異，則能發現人工審計容易遺漏的隱性假設錯誤。
- 5
--
實用技巧與重點
乾貨- 規模數字：
- Reth（Ethereum Rust 客戶端）：97,000 行 Rust
- Lighthouse（共識客戶端）：150,000 行 Rust（不含測試）
- FireDancer（Solana 客戶端）：340,000 行 C/C++
- Ethereum 2.0 存款合約現存約 2,000 億美元，2019 年由 RV 進行形式化驗證
- 工具名稱：
- `cargo audit`：掃描 Rust 專案依賴項（供應鏈攻擊防護）
- `Almanax`：用於智能合約與基礎設施的 AI 安全審計工具
- `Deep Wiki`：專案初期快速理解代碼庫架構
- `arbitrary`（Rust crate）：生成結構化模糊測試輸入
- `KVM`（K language）：EVM 的形式化模型
- `Certora Prover`、`Halmos`：生產級形式化驗證工具
- `cloc`：程式碼行數統計工具
- 方法與流程：
- 設計評審（數天至一週）→ 理解系統、定義規格與不變式
- 集中人工審查高優先級代碼（新代碼、`unsafe` 區塊、關鍵交互點）
- AI 輔助審查（帶規格說明）覆蓋人工無法觸及區域
- Panic-focused 模糊測試 → 基於屬性的模糊測試 → 差分模糊測試
- 選擇性形式化驗證（小型關鍵組件、橋接合約、數據結構）
- 真實案例：
- Cloudflare 事故原因：Rust 中 `unwrap()` 因錯誤輸入引發 panic，導致半數互聯網癱瘓
- 發現 Solana 部分節點實作拒絕空交易而其他節點不拒絕的分歧漏洞
- 形式化驗證 Nethermind EVM Yul 與 KVM 的操作碼等價性，發現若干實作差異
- 在 Viper 編譯器中因形式化驗證以太坊 2.0 存款合約而發現編譯器漏洞
- --
結論
結論“基礎設施審計的核心是「分層擴展」：用短週期人工審計聚焦關鍵代碼，用 AI 補足覆蓋盲區，用差分模糊測試捕捉實作分歧，再選擇性地以形式化驗證提供最高安全保證——而一份清晰的規格說明，是貫穿所有環節的最重要加速器。”
完整解析
詳細加密基礎設施是指智能合約與用戶之間整個執行堆疊——從編譯器、JSON-RPC 節點、記憶體池，到虛拟機指令執行，再到共識協議。Runtime Verification CEO 寶琳娜在演講中指出，業界過去幾年的安全焦點集中在智能合約，但近來基礎設施審計的需求正快速增加，成為新的行業趨勢。她坦言，這類審計在方法論上面臨根本性挑戰：程式碼規模大到難以想像——Ethereum Rust 客戶端 Reth 約 97,000 行，共識客戶端 Lighthouse 超過 150,000 行，而 Solana 的 FireDancer 更達 340,000 行 C/C++ 代碼。傳統的逐行人工審計在這種規模下根本不可行，加之威胁模型也截然不同，需要面對鏈分裂、DoS、記憶體耗盡、領導人選舉操控等智能合約審計幾乎不涉及的問題。
針對規模問題，寶琳娜分享了 RV 採用的核心策略：以 6-8 週為單位進行輪迴式短週期審計，每輪聚焦於高優先級代碼——包括較新的代碼、Rust `unsafe` 關鍵字出現的所有位置、EVM 兼容鏈與參考實作之間的差異點（例如 gas 定價差異可能引發 DoS），以及組件之間的交互邊界。每輪審計前先進行設計評審，用數天時間理解系統架構、定義規格與不變式，這份規格不僅指導人工審查的方向，也成為 AI 工具的輸入依據。她特別強調，使用 Almanax 進行 AI 輔助審計時，若僅要求它自行發現漏洞，效果有限；但若同時要求它找出代碼與規格之間的偏差，則能發現人工容易忽略的隱性假設錯誤——例如某個函數假設上層調用者會進行某項驗證，但實際上並沒有。
在工具擴展覆蓋範圍方面，模糊測試是另一支柱。RV 採用三層次的模糊測試：首先是 Panic-focused 測試，輸入偽隨機數據讓程式崩潰（Cloudflare 那次導致半數互聯網癱瘓的事故，正是 Rust `unwrap()` 因錯誤輸入 panic 所致，這類問題模糊測試能有效捕捉）；其次是基於屬性的模糊測試，不只檢查是否崩潰，還斷言函數的實際行為，例如類型轉換往返一致性、序列化反序列化的幂等性；最進階的是差分模糊測試，同時運行同一系統的不同實作（如 Rust 客戶端與 Geth），比對所有輸入下的行為，藉此發現客戶端分歧——RV 即以此發現 Solana 部分節點實作拒絕空交易而其他節點不拒絕的高危問題。Rust 項目的結構化輸入生成使用 `arbitrary` crate，不同語言有各自對應的工具生態。
最後在形式化驗證方面，寶琳娜建議選擇性應用：聚焦於小型關鍵組件（橋接合約的事件發送、數據結構操作）、EVM 不同實作的操作碼等價性驗證，以及存款合約等高價值目標。RV 在 2019 年形式化驗證以太坊 2.0 存款合約（現存約 2,000 億美元資產）時，正是因此發現了 Viper 編譯器漏洞——這類編譯器級漏洞幾乎只有形式化驗證才能識別。她建議最好在開發早期就引入形式化驗證，而非在系統成熟後才補做。
---
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
