以太坊客戶端降低信任基礎的5條驗證路徑公開

以太坊客戶端降低可信計算基礎（TCB）的形式驗證設計與5條實作路徑已公開。

以太坊基金會成員喬治·卡迪亞納基斯（George Kadianakis）與凱夫·韋德伯恩（Kev Wedderburn）25日在以太坊研究論壇發布相關文章，說明如何透過形式驗證縮小以太坊客戶端的信任範圍。

TCB指的是使用時以信任為前提的元件、規格、工具與假設，而非已完成驗證的對象。文章指出，形式驗證無法完全消除TCB，但能縮小人員必須直接信任的範圍。

研究人員提出，應將抽象化客戶端拆分為多個模組，分別驗證各模組的功能與保證範圍，再透過介面連結模組級保證，以確認整體客戶端的安全屬性。

其中一項核心區分是「純模組」與「非純模組」。密碼學、SSZ與分叉選擇規則等副作用較少、數學結構明確的領域，適合歸類為形式驗證的純模組。網路模組則涉及大量輸入輸出與外部狀態，必須考慮訊息順序、連線中斷與延遲等因素，因此被視為非純模組。

研究人員建議，非純模組從設計之初就不應被直接信任。例如，不要直接信任網路模組傳遞的簽章，而是交由純簽章驗證模組重新處理，讓網路模組的錯誤能以與惡意外部輸入相同的方式被處理。

長期而言，驗證邊界也可進一步靠近網路。與其建模整個網路，不如優先驗證解析器、Gossip規則與同步邏輯，避免錯誤訊息導致系統中斷或消耗過多資源。

文章也將規格與實際執行檔之間的連結列為另一項課題。研究人員區分了使用Lean4撰寫形式規格並證明屬性，以及證明實際實作遵循該規格這兩個步驟。文章指出，使用者更重視自己電腦上執行程式的安全性，而非僅是Lean4中的定理，因此兩個階段都不可或缺。

實作路徑包括：△將以Rust等語言撰寫的程式碼自動轉換為Lean4 △將以Lean4撰寫的模組擷取為C程式碼 △直接以Lean4撰寫客戶端，僅將副作用較大的模組連接至其他語言 △以RISC-V組合語言直接撰寫核心模組 △使用經驗證的編譯器。

若將Rust程式碼轉換為Lean4，轉換器與建構最終二進位檔的Rust編譯器仍會留在TCB中。若將Lean4程式碼擷取為C，或以Lean4撰寫客戶端大部分內容，擷取器、C編譯器與外部函式介面則會被納入信任對象。

以RISC-V組合語言撰寫核心模組，可以將一般編譯器排除在TCB之外，但RISC-V指令集的形式模型，以及將組合語言轉換為其他處理器程式碼的工具，會成為新的信任對象。使用經驗證的編譯器，則能將擷取器與C編譯器排除在TCB之外。

研究人員認為，沒有必要對所有模組套用同一種方法。數學結構較強的模組可使用Lean4驗證，資料結構複雜或規模較大的模組則可採用轉換器或經驗證編譯器，混合使用不同方法。

這篇文章並非宣布整個以太坊客戶端已完成形式驗證，而是提出一套研究方向，探討如何拆分形式規格、實作與編譯流程的驗證單位，以及應將驗證範圍擴大至何種程度。