维塔利克·布特林称人工智能可强化加密安全性

币安Binance

币安交易所是全球加密货币交易所龙头，在手机上即可买卖比特币等数字货币！

官网注册  APP下载

以太坊联合创始人谈AI如何增强加密系统安全性

针对日益增长的担忧——基于AI的漏洞挖掘将使开发者不堪重负，并在区块链上制造无休止的攻击机会——以太坊联合创始人Vitalik Buterin近日作出回应。他认为，在不久的将来，这项技术的应用实际上可能使加密系统更加安全。他指出，AI辅助的形式化验证或许会成为对抗加密及互联网基础设施安全漏洞的最强防御手段之一。

AI可能成为安全加固者而非破坏者

形式化验证是指编写计算机可自动验证的软件数学证明，以替代人工审查。这一概念已存在数十年，但始终未普及，因为手动生成此类证明对开发者而言相当繁琐，导致许多人望而却步。Buterin指出，AI正在改变这一局面：开发者无需自行撰写证明，而是可以要求AI同时生成代码及配套证明，开发者只需验证最终被证明的陈述是否符合预期目标。

Buterin设想了一种场景：当AI模型足够强大，能自动发现现有代码中的漏洞时，对于那些单一漏洞就可能导致用户损失全部资产的系统意味着什么？他的答案是：通过端到端的形式化验证，人们可以从数学上证明一段代码完全按预期运行。这样，即使面对能力强大的AI漏洞搜寻工具，其所检查的也已是经过验证的无漏洞代码。

他还列举了以太坊生态中已在尝试此方法的项目，例如致力于实现完全形式化验证STARK方案的Arklib，以及正在构建基于RISC-V汇编的低层级EVM、并对照可读参考实现验证其正确性的evm-asm项目。

关于哪些AI模型适用于此项工作，Buterin表示Claude与Deepseek 4 Pro均能胜任Lean证明的编写。同时，他特别提及专为Lean优化的开源轻量模型Leanstral，该模型可在本地运行，并在形式化验证基准测试中优于许多大型通用模型。

技术仍存在局限性

尽管对形式化验证充满热情，Buterin也花费相当篇幅解释了该技术在实践中的失败案例。例如已验证编译器中的漏洞、仅部分代码被证明而未被证明部分反而出问题的库，以及技术上已获证明却未能真正反映开发者意图的规范缺陷。

但他强调，形式化验证并非要取代所有安全实践，而是在“每行代码缺陷更少”这一长期趋势中的有力工具。这一观点在当前背景下尤为相关：Buterin发表论述当日，加密行业刚在四天内遭遇第三起重大攻击——跨链桥协议Echo遭黑客盗取价值超7600万美元加密资产。此前，THORChain也被曝损失超1000万美元，随后Verus-Ethereum桥接项目又因缺乏验证检查而被盗1158万美元。此类具体而局部的缺陷，恰恰是形式化证明检查可能及时发现的问题。