Vitalik Buterin 反駁 AI 網路安全末日論

Buterin 在 9 月 17 日於 X 的貼文中寫道，他不同意日益普遍的觀點，即「AI 駭客攻擊意味著網路安全注定失敗」。他表示，繼續持有加密貨幣的人其實是在隱性押注安全的數位系統能夠抵禦更強的自動化攻擊，並補充說他個人淨資產中約 90% 仍為加密貨幣。

他的論點核心是形式化驗證，這是一種利用數學規格與證明來判斷軟體行為是否符合預定義屬性的技術。Buterin 以高等數學定理證明作為類比，表示能力足夠的 AI 可以協助證明「此程式是安全的」，即使軟體本身相當複雜。

Buterin 認為形式化驗證有利於防守方

Buterin 的論點並未將 AI 安全視為一場防守研究人員僅需比攻擊者更早找出漏洞的競賽。他的貼文反而描述了一種模型：開發者定義系統必須滿足的屬性，然後使用自動化證明工具來確立實作符合這些屬性。

以太坊自身的形式化驗證文件以較狹隘的用語描述此技術。文件指出，形式化驗證能以數學方式證明智慧合約符合形式化規格，針對規格中包含的屬性提供比一般測試更強的保證。

同一份以太坊文件點出了 Buterin 評論背後的一項重要限制。證明確立了軟體滿足受檢驗的規格；它並不會自動證明開發者正確地定義了每一項安全屬性。選擇不當或不完整的規格可能使行為落在證明範圍之外。

Buterin 在貼文中也做出相同區分。他主張，將「安全」定義得太狹隘可能遺漏涉及協定、伺服器、資料庫、網路層、快取或其他支援元件的攻擊路徑。因此，他提出的方向是驗證更完整的系統，而非僅將一小群模組標記為安全關鍵。

Buterin 先前已將 AI 輔助的形式化驗證描述為軟體開發可能的「最終型態」。他先前的評論將此方法應用於以太坊共識、零知識系統與抗量子密碼學等領域。

以太坊已在測試 AI 輔助安全

以太坊研究人員已在安全工作中使用 AI，儘管目前系統距離全系統安全的自動證明仍相當遙遠。

以太坊基金會協定安全團隊在 7 月報告，協同運作的 AI 代理已在以太坊使用的系統中發現真實缺陷。其中一項已確認的發現涉及 Rust libp2p 的 Gossipsub 網路實作中可遠端觸發的崩潰。

該缺陷成為 CVE-2026-34219。美國國家漏洞資料庫的紀錄顯示，0.49.4 之前的版本可透過特製的 PRUNE 訊息遠端觸發崩潰，該訊息在 Gossipsub 退避處理期間引發算術溢位。0.49.4 版已修復此問題。

基金會安全團隊表示，漏洞發現並非 AI 工作流程中最困難的部分。研究人員發現，AI 代理經常產生令人信服的報告，但涉及不可達的執行路徑、僅在除錯模式出現的失敗，或是形式上通過但實際上證明了較預期更弱屬性的證明。

在團隊接受一項發現之前，獨立重現仍是必要條件。基金會表示，需要自動化檢查與人工審查，因為代理可能產生看似有效的證明，卻未能約束研究人員真正想測試的軟體行為。

基金會的經驗被描述為一種分流問題：AI 可以產生大量候選漏洞，但研究人員仍須判斷每個問題在生產環境中是否可達且具有意義。

形式化驗證正進入以太坊協定路線圖

以太坊基金會已另行將形式化驗證納入其目前的協定研究計畫。在 9 月 7 日的協定優先事項更新中，基金會表示形式化驗證將作為跨領域工具，涵蓋其餘多年的研究領域。該文件涵蓋隱私、狀態、zkEVM 開發、後量子安全及其他協定元件，直至 2029 年。

同一份路線圖指出，L1 zkEVM 的開發預期將推進形式化驗證工具、工作流程與經過驗證的密碼學元件。以太坊研究人員正朝向一個系統努力，在該系統中驗證者最終將驗證簡潔的執行證明，而非獨立重新執行每個區塊。

另一個於 8 月啟動的以太坊基金會專案已將 AI 代理與機器檢查證明結合。better.codes 專案讓研究人員引導 AI 系統處理以 Lean 形式化的密碼學健全性問題，而 Lean 核心則檢查提交的證明是否滿足固定的定理陳述。

基金會的第二季資助報告列出更多結合大型語言模型與形式化方法的工作。專案包括用於對照規格檢查以太坊用戶端實作的 ETHeorem、用於自動化協定合規工作的 SPECA 與 LeanAgent，以及涉及 RISC-V zkVM 基礎設施的形式化驗證。

以太坊更新的技術路線圖賦予形式化驗證與隱私、零知識證明及後量子保護並列的角色。因此，Buterin 在 9 月 17 日的評論延續了既有的研究方向，而非宣布新的升級或排定的分叉。他的貼文並未提及新的 EIP、部署日期，或要求每個以太坊程式都必須接受形式化驗證的強制性規則。

當前 AI 證據亦顯示更強的攻擊能力

近期的網路安全研究支持一項擔憂：即使防禦性應用不斷擴大，AI 仍使攻擊者能力更強。Anthropic 在 9 月的威脅情報報告中表示，已觀察到惡意行為者利用 AI 自動化漏洞研究、漏洞利用開發與多目標攻擊活動。該公司表示，部分操作者維持可持續進行漏洞研究的自動化工作流程。

Anthropic 先前的更大規模研究也發現類似證據。其協調揭露儀表板顯示，截至 8 月 26 日，該公司已揭露 392 個開源專案中由 AI 發現的 2,300 個漏洞，其中 421 個已在當時於上游修補。

Anthropic 將相同技術描述為對防禦有用。其 Project Glasswing 計畫報告與資安公司及軟體供應商合作，使用前沿模型在惡意行為者利用之前找出高嚴重性與重大嚴重性缺陷。

攻擊面仍可量化。Anthropic 在 6 月的研究檢視了 2025 年 3 月至 2026 年 3 月間與惡意網路活動相關的 832 個帳戶，發現威脅行為者在網路作戰的多個階段使用 AI。Buterin 先前已駁斥另一項主張，即 AI 驅動的安全風險可能嚴重打擊對比特幣的信心。他表示，網路層問題通常可透過軟體與挖礦基礎設施升級來解決，同時將比特幣雜湊或工作量證明機制實際被破解描述為極不可能。

Anthropic 的 9 月報告指出，其調查人員已識別出使用 AI 建構的漏洞利用管線針對安全設備與政府目標的攻擊者，部分攻擊活動產生了攻擊者在其自有測試環境中驗證過的未知漏洞。