新聞 
幣種資訊 
關於我們 
EthSystems 已完成以太坊(ETH)隱私池的形式驗證，範圍從設計文件延伸至部署在 Sepolia 測試網上的程式碼。驗證過程共發現 6 項問題，其中 3 項來自驗證工具本身。
PANews 報導，EthSystems 於 27 日公布上述結果。隱私池旨在隱藏交易資訊，同時確認交易是否符合既定規則。此次驗證逐步檢查設計文件的內容是否落實於實際實作及部署程式碼。
形式驗證是將程式必須滿足的條件以數學方式表達，再透過工具確認條件是否成立。EthSystems 使用 Lean 驗證模型、電路與雜湊，並以 Halmos 和 Kontrol 驗證智慧合約；錢包則由 Aeneas 和 Verus 檢查。
在驗證器與部署階段，團隊重新建置程式碼，並逐位元組比對其與 Sepolia 測試網上執行的位元碼。位元碼是網路實際執行的程式碼。這項程序用來確認設計文件與可讀程式碼的審查結果，也反映在已部署的程式碼中。
主要驗證項目是防止雙重支付與確保價值守恆，也就是避免同一資產被使用兩次，或交易過程中在沒有依據的情況下增加價值。EthSystems 表示，這兩項條件已透過 Lean 定理證明器完成機器驗證。
驗證過程共發現 6 項問題，其中 3 項出自驗證工具。EthSystems 未在公告中披露各項問題的內容或是否已修正。
驗證結果仍有前提。PANews 報導，EthSystems 將不存在雜湊碰撞、拒絕偽造證明，以及智慧合約與驗證模型行為一致，列為驗證成立的前提。因此，驗證結果應在這些條件持續成立的範圍內解讀。
為處理以太坊公有帳本會公開交易資訊的問題，EthSystems 正在開發面向機構的隱私技術。此次公告說明了從設計文件到測試網執行程式碼的驗證範圍，也揭示了仍須成立的假設。
留言 0