以太坊Vitalik Buterin解釋AI如何能讓智能合約真正安全

本文《Ethereum 聯合創辦人 Vitalik Buterin 解釋 AI 如何讓智能合約真正安全》首發於 Coinpedia Fintech News

Ethereum 聯合創辦人 Vitalik Buterin 發表了一篇詳細論述，指出 AI 輔助形式驗證（Formal Verification）有望從根本上改變安全軟件的構建方式，並反駁網絡安全社群中日益蔓延的悲觀情緒——即無需信任的系統是否能夠在日益強大的 AI 驅動攻擊下存活。

「許多人聲稱，隨著 AI 輔助漏洞發現技術的出現，安全代碼將變得不可能，」Buterin 寫道。「我的看法要樂觀得多，而 AI 輔助形式驗證正是其中一個重要原因。」

形式驗證究竟是什麼

形式驗證是一種針對代碼編寫數學證明並由電腦自動檢查的實踐方法。開發者不再依賴測試軟件並期望漏洞不出現，而是編寫數學證明，從數學上保證一段代碼在所有條件下均按預期運行。

這項技術已存在數十年，但始終處於小眾領域，原因在於手動編寫這些證明極其困難且耗時。Buterin 的論點是，AI 大幅改變了這一局面。AI 可以同時編寫代碼和證明，而人類只需驗證所證明的陳述是否與他們實際希望軟件執行的內容相符。

他將這種組合描述為研究員 Yoichi Hirai 所稱的「軟件開發的最終形態」。

這對 Ethereum 的意義

Buterin 指出形式驗證已在 Ethereum 開發生態系統中的多個領域得到應用，包括抗量子簽名、STARK 證明系統、共識算法以及 ZK-EVM——這些領域的安全屬性定義簡單，但底層代碼極為複雜。

Arklib 等項目正致力於實現完全形式驗證的 STARK 實現。evm-asm 項目正在構建一個直接以 RISC-V 彙編語言編寫的完整 EVM，並通過數學方式對照人類可讀的參考實現進行驗證。拜占庭容錯共識協議也正在 Lean 中進行形式規範和驗證。

核心洞見在於，對於這些系統而言，代碼實際行為與預期行為之間的差距可以通過數學確定性而非概率測試來消除。

他所承認的局限性

Buterin 謹慎地避免誇大其詞。形式驗證存在真實的失敗模式。證明可能只針對系統的一部分編寫，而關鍵漏洞則隱藏在未經驗證的部分。開發者可能忘記規定重要屬性。形式規範本身也可能出錯。旁道攻擊等硬件漏洞甚至可以繞過數學上正確的軟件。

「可證明的正確性並不能以大多數人理解的方式證明軟件是正確的，」他寫道。形式驗證實際上能做到的，是讓開發者以多種不同的冗余方式表達其意圖，並自動檢查所有這些表達是否彼此相容。

更宏觀的願景

Buterin 描述了一個樂觀的未來：軟件分為兩層。不安全的邊緣層負責處理低風險功能，在沙盒中運行，並以最小權限運作。安全核心層負責處理所有關鍵事務，包括 Ethereum 本身、操作系統內核以及敏感的 IoT 基礎設施。

安全核心層被刻意保持精簡，並接受嚴格的形式驗證。AI 帶來了使大規模驗證切實可行的計算能力。最終結果並非零漏洞的軟件，而是最關鍵的組件可以憑藉數學確信而非僥幸心理加以信賴的軟件。

「防禦者終於有機會決定性地獲勝，」他總結道，並援引 Mozilla 自身在針對 AI 輔助攻擊工具強化代碼庫方面的經驗。