Vitalik Buterin 驳斥了能力日益增强的 AI 黑客将使网络安全实际上变得无法取胜的说法,他在 9 月 17 日辩称,先进的验证工具最终可能赋予防御方结构性优势。
摘要
- 根据 Buterin 本人 9 月 17 日的声明,他净资产的 90% 仍以加密货币形式持有。
- 根据 Buterin 的论点,AI 辅助的形式化验证有助于证明软件满足已定义的安全属性。
- 以太坊的安全团队已经在使用 AI 代理来检查协议代码并独立复现漏洞。
- 以太坊研究人员现在将形式化验证视为贯穿多个长期协议研究方向的交叉工具。
- Anthropic 表示,前沿 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 日的协议优先级更新中,基金会表示形式化验证将作为横跨其剩余多年研究领域的通用工具。该文件涵盖截至 2029 年在隐私、状态、zkEVM 开发、后量子安全及其他协议组件方面的工作。
同一路线图称,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 个开源项目中披露了 2,300 个由 AI 发现的漏洞,其中 421 个已在上游得到修补。
Anthropic 也将同一技术描述为对防御有用。其 Project Glasswing 计划报告称,与安全公司和软件供应商一起使用前沿模型,在恶意行为者利用之前定位高严重性和严重漏洞。
攻击方面仍然是可以衡量的。Anthropic 六月份的研究考察了 2025 年 3 月至 2026 年 3 月期间与恶意网络活动相关的 832 个账户,发现威胁行为者在网络行动的多个阶段使用了 AI。Buterin 此前已经驳斥了另一种论点,即 AI 驱动的安全风险可能严重损害人们对比特币的信心。他表示,网络层问题通常可以通过软件和挖矿基础设施升级来解决,同时称比特币哈希或工作量证明机制被真正攻破的可能性极低。
Anthropic 九月份的报告称,其调查人员已发现一些操作者利用 AI 构建的漏洞利用流水线攻击安全设备和政府目标,其中一些行动产生了此前未知的漏洞,攻击者还在自己的测试环境中对其进行了验证。






