Vitalik Buterin：人工智慧和形式化驗證可以讓關鍵程式碼無法被破解

以太坊共同創辦人維塔利克‧布特林（Vitalik Buterin）向來不吝於提出宏大的構想。但他最新的文章將目光投向了區塊鏈之外，探討了一個可能重塑軟體安全基礎的領域：形式化驗證。形式化驗證是一種透過編寫數學上可驗證的證明來證明電腦程式碼的行為完全符合預期的實踐。面對日益強大的人工智慧能夠大規模地發現和利用軟體漏洞，布特林認為，這種沿用數百年的數學證明方法不僅有用，而且可能是通往可信賴的數位未來的唯一可靠途徑。

這論點可謂恰逢其時。人工智慧輔助的漏洞發現正在迅速將局勢向攻擊者傾斜。過去需要人工審核團隊花費數週時間才能審查的程式碼，現在只需幾分鐘即可掃描漏洞。安全領域的一些人士對此表示無奈，認為確定性軟體保障已基本終結，或認為唯一可行的應對之策是退回到閉源的壁壘之後。 Buterin 堅決駁斥了這兩種觀點。

他的樂觀並非源自於一廂情願，而是基於特定的技術組合：人工智慧與形式化驗證的結合。人工智慧可以產生海量程式碼，包括高度優化的底層彙編程式碼，而這些程式碼如果由人類編寫則需要耗費大量精力。形式化驗證隨後能夠以機器可驗證的數學確定性證明這些程式碼具備所需的屬性。布特林認為，結果是回歸編寫最高效程式碼的模式——就像程式設計師五十年前用原始彙編語言編寫的程式碼那樣——但這一次，程式碼附帶了嚴格的正確性證明。研究員平井洋一稱之為「軟體開發的最終形態」。布特林對此表示贊同。

形式化驗證的實際作用──以及它所不具備的作用

要理解 Buterin 的案例，首先需要明確形式化驗證的概念。本質上，它指的是編寫關於軟體的數學定理，然後自動驗證這些定理。與其測試程式碼在樣本輸入上是否有效，不如證明在給定特定條件的情況下，程式碼在所有可能的輸入上都能正常運作。 defi無需任何假設。 Lean程式語言是這裡的主要工具，它在純數學和軟體工程領域都得到了越來越廣泛的應用。目前正在進行的項目包括對加密協議進行形式化驗證的實現，例如Signal的X3DH密鑰交換、ZK-STARK證明系統，甚至還有一個完全用RISC-V彙編語言構建的以太坊虛擬機（EVM），並附有正確性證明。

這確實非常強大。最棘手的軟體漏洞往往是互動漏洞——位於兩個子系統邊界處的缺陷，而這兩個子系統單獨來看都是安全的。人類審計人員根本無法同時考慮整個複雜的系統。而自動化的證明檢查系統可以做到。形式化驗證也特別適用於以太坊最需要確保安全的系統類型：抗量子簽名、零知識證明系統和共識演算法——所有這些領域的安全屬性在概念上都很容易描述，即使實現起來極其複雜。

但布特林謹慎地避免過度誇大其詞。 「可證明的正確性」並非大多數人所理解的那樣。證明僅僅表明代碼滿足形式化定義的規範。如果規範不完整，證明也就不完整。如果證明中嵌入的關鍵假設在實踐中不成立——例如，硬體側通道以威脅模型從未考慮過的方式洩露資訊——證明仍然有效，但係統仍然不安全。歷史提供了令人警醒的例子：經過形式化驗證的C編譯器也存在漏洞；經過形式化驗證的加密協定後來在設計者未預料到的攻擊者模型下被破解。布特林強調，形式化驗證並非萬靈藥。它只是眾多強大技術之一，如果應用不當、不完整，或使用的規格與用戶實際需求不符，它就會失效。

前路漫漫：漏洞百出的世界中的安全核心

Buterin 的願景既細緻入微又充滿希望。在他看來，軟體安全的未來並非一個所有程式碼都經過完美驗證的世界——這既不現實也不必要。它是由一個日益精簡的「安全核心」和一個較為寬鬆的沙盒式外圍組成。外圍程式碼——應用程式、外掛程式、人工智慧生成的腳本——可能仍然混亂且容易出錯。只要它們以最低權限運行且不會危及核心安全，這都是可以接受的。相較之下，安全核心——作業系統核心、以太坊本身、加密基礎設施、物聯網基礎架構——必須遵循完全不同的標準，而形式化驗證是實現這一標準的關鍵。

在這種架構中，人工智慧改變的不是預設提高程式碼安全性，而是首次使嚴格驗證變得可行。手工編寫證明極其困難，幾十年來一直使形式化方法成為一門小眾學科。但如果人工智慧能夠同時編寫優化的實現和相應的證明，而人類的監督則僅限於檢查所陳述的定理是否真正抓住了關鍵所在，那麼整個體系的運作方式就發生了轉變。繁重的驗證工作變得可以自動化；人類的角色從逐行檢查程式碼轉變為規範和判斷。

在布特林看來，事關重大，遠不止於以太幣或加密貨幣本身。密碼朋克傳統——即認為在數位網路中，防禦者擁有結構性優勢，因為建立加密保護比破解它更容易——正受到人工智慧攻擊者的真正威脅。形式化驗證與人工智慧結合，是目前為數不多的能夠恢復這種優勢的工具之一。其目的並非消除所有漏洞，而是使最關鍵的系統真正能夠抵禦形式化攻擊，從而實現可證明的安全。 defi一類威脅。在一個人工智慧日益自主、能力日益強大的世界裡，這或許正是我們需要的硬性保障。