以太坊共同創辦人 Vitalik Buterin 並不認為 改善人工智慧最終會讓網路安全變得基本上無法取勝。
Buterin 確信相反的情況最終可能發生：AI 或許能為防禦者提供所需的工具，從一開始就打造出更難被利用的軟體。
「AI 駭客意味著網路安全注定失敗，這種說法越來越常見。我不同意，」Buterin 週三在 X 社群網路上發表了一篇冗長且一如往常內容紮實的社群媒體貼文，如此寫道。
根據這位以太坊共同創辦人的說法，一旦開發者開始充分利用形式驗證，網路安全自然會對防禦者有利。
Buterin 也將這個信念直接與他自己對加密貨幣的曝險連結起來，並透露他約 90% 的淨資產仍留在加密貨幣中。
他主張，任何繼續持有大量加密貨幣的人，實際上都是在押注：儘管攻擊者日益精密，仍能打造出足夠安全的數位系統。
「如果 AI 能證明 Navier-Stokes 和 FLT，那麼 AI 就能把『這個程式是安全的』這個陳述證明為一個數學定理，」Buterin 寫道，指的是 Navier-Stokes 問題和費馬最後定理。
他的論點基於形式驗證，這是一種以數學方式證明軟體滿足特定屬性的方法。
Buterin 在他五月的文章中廣泛探討了同樣的想法，他在文中將 AI 輔助的形式驗證描述為對安全關鍵軟體極具變革性的工具。然而，要證明這類軟體是安全的，可能會相當具有挑戰性。
定義問題
Buterin 以加密通訊應用程式 Signal 為例，說明這為何可能很困難。
攻擊者可能會試圖偽造訊息、阻止訊息送達、重播舊訊息、入侵伺服器、操縱用來發現另一位使用者公鑰的流程，或利用作業系統中的漏洞。
其他問題可能來自損壞的資料庫、惡意函式庫、編譯器，甚至硬體層級的資訊外洩。
即使對話內容保持加密，攻擊者仍可能得知誰在通訊。因此，「安全」究竟是什麼的數學定義本身，可能就會變得極其複雜。
「所以……即使是定義也可能超過一千行程式碼，而且需要深入仔細思考才能釐清，」Buterin 寫道。
攻擊者與防禦者
毫無疑問，能力更強的 AI 系統可以讓尋找漏洞變得更容易。
然而，機器推理的同樣進步，也可能大幅降低以形式方式證明軟體依照精心建構的安全規格運作的成本。
雙方都會擁有 AI。
