- 以太坊聯合創始人 Vitalik Buterin 表示，AI 輔助的形式驗證可以從數學上證明代碼的安全性，並將其稱為軟件開發的「最終形態」。
- 此番言論發表於 Verus Protocol 橋接漏洞之後，該漏洞因偽造消息導致了 1160 萬美元的損失，凸顯了持續存在的 DeFi 安全風險。
- Buterin 認為，該方法對於保護以太坊的核心升級至關重要，包括 ZK-EVM、STARK 以及針對未來攻擊的抗量子密碼學。
返回
Vitalik Buterin 表示 AI 可協助削減 99% 以上的漏洞後果
(P1) 以太坊聯合創始人 Vitalik Buterin 表示，AI 輔助的形式驗證可以消除絕大部分代碼漏洞。這一言論發表之際，另一家 DeFi 協議由於以太坊橋接漏洞損失了 1160 萬美元。
(P2) 「如果你進行端到端的形式驗證，你不僅是在證明協議的某些描述在理論上是安全的，而且是在證明用戶運行的具體代碼在實踐中也是安全的，」Buterin 在週一發佈的博客文章中寫道。他認為這種方法可以減少因代碼破碎帶來的 99% 以上的負面後果。
(P3) Buterin 對代碼安全的評論因 Verus Protocol 以太坊橋接漏洞的報告而顯得尤為重要。鏈上安全公司 Blockaid 和 PeckShield 報告稱，攻擊者利用偽造的跨鏈轉移消息提取了資產，隨後將其轉換為 5402 枚以太幣，價值超過 1140 萬美元。
(P4) 這一事件突顯了加密生態系統中軟件漏洞帶來的財務風險。Buterin 認為，形式驗證對於保護下一代以太坊基礎設施至關重要，特別是對於像量子抗性簽名、STARK 和 ZK-EVM 等複雜且關鍵的組件。
根據 Blockaid 的說法，Verus 橋接事件是由於缺少源金額驗證引起的，這一缺陷本可以通過大約 10 行 Solidity 代碼來識別和修復。該安全公司指出，此次攻擊的結構類似於 2022 年 Nomad Bridge（1.9 億美元）和 Wormhole（3.25 億美元）的漏洞，在這兩個案例中，欺詐性指令誘騙橋接器從其儲備中發送資金。
在文章中，Buterin 描繪了一個未來：AI 工具幫助開發人員編寫高效代碼的同時，也編寫驗證其正確性的數學證明。他將這種結合稱為軟件開發的潛在「最終形態」。這種方法被視為一種強大的防禦手段，以應對未來高級 AI 可能被用於以前所未有的規模發現並執行網絡攻擊的情況。
儘管 Buterin 是該技術的堅定倡導者，但他提醒說，形式驗證「並非萬靈丹」，因為它無法消除所有安全風險，例如源於初始假設缺陷或硬件漏洞的風險。然而，他認為它非常適合支撐以太坊未來路線圖的複雜密碼系統，使接近無漏洞的代碼成為現實的期望。
本文僅供參考，不構成投資建議。
