导航菜单
首页
排名 涨幅榜 跌幅榜 24h成交额 新币榜
快讯 机构 观点 人物 专题

Vitalik Buterin驳‘AI黑客致网络安全无解’:形式化验证或让防御方获结构性优势

以太坊联合创始人Vitalik Buterin 9月17日在X平台发文,反驳“AI黑客将让网络安全注定失败”的流行观点。他认为,具备足够能力的验证工具可能让防御方获得结构性优势;而他约90%的净资产仍持有加密货币,意味着他也在押注安全数字系统能够承受更强的自动化攻击。

形式化验证被视为防御方优势

Buterin的核心论点是形式化验证。该技术使用数学规范和证明来判断软件是否符合预设属性。他将其比作高级数学定理证明,并称足够强大的AI可以帮助证明“这个程序是安全的”,即使软件本身很复杂。

以太坊形式化验证文档也指出边界:形式化验证可以数学证明智能合约符合正式规范,在规范涵盖的属性上提供强于普通测试的保证;但证明软件满足规范,并不自动证明开发者定义了所有安全属性。规范选择不当或不完整,可能使部分行为不受证明约束。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日的协议优先级更新中,基金会表示形式化验证将作为跨领域工具,服务于其剩余多年研究领域。文件涵盖隐私、状态、zkEVM开发、后量子安全及其他协议组件,时间范围到2029年。路线图称,L1 zkEVM开发预计将推进形式化验证工具、工作流和已验证密码组件。以太坊研究人员正朝着验证者最终验证简洁执行证明、而不是独立重新执行每个区块的方向努力。

以太坊基金会8月启动的better.codes项目已在结合AI代理与机器检查证明。该项目让研究人员将AI系统指向Lean中形式化的密码学可靠性问题,而Lean内核检查提交证明是否满足固定定理陈述。基金会第二季度资助报告还列出更多结合大语言模型与形式化方法的工作,包括检查以太坊客户端实现是否符合规范的ETHeorem、用于自动化协议合规的SPECA和LeanAgent,以及涉及RISC-V zkVM基础设施的形式化验证。

以太坊更新后的技术路线图赋予形式化验证与隐私、零知识证明和后量子保护并列的角色。因此,Buterin在9月17日的评论延续了既有研究方向,而不是宣布新升级或计划中的分叉。他的帖子没有提到新的EIP、部署日期,也没有要求每个以太坊程序必须接受形式化验证的强制规则。

AI攻击能力也在上升

近期网络安全研究支持了AI正让攻击者更具能力的担忧,尽管防御性用途也在扩大。Anthropic在9月威胁情报报告中表示,已观察到恶意行为者利用AI自动化漏洞研究、利用开发和多目标行动。该公司称,一些运营者维持可连续进行漏洞研究的自动化工作流。Anthropic此前的协调披露仪表板称,截至8月26日,该公司已在392个开源项目中披露2300个AI发现的漏洞,其中421个已在上游修补。

Anthropic也把同一技术描述为防御工具。其Project Glasswing计划报告称,正与安全公司和软件厂商使用前沿模型,在恶意行为者利用前定位高危和关键严重漏洞。但攻击侧仍可衡量。Anthropic 6月研究审查了2025年3月至2026年3月期间与恶意网络活动相关的832个账户,发现威胁行为者在网络行动多个阶段使用AI。

Buterin此前还反驳了另一论点,即AI驱动的安全风险可能严重损害比特币信心。他表示,网络层问题通常可通过软件和挖矿基础设施升级解决,而比特币哈希或工作量证明机制被实际破解的可能性极低。Anthropic 9月报告称,调查人员识别出运营者使用AI构建的利用管道,针对安全设备和政府目标,一些行动产生了此前未知的漏洞,攻击者已在自有测试环境中验证。