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

V神驳斥AI网络安全末日论:形式化验证可助防御者占据上风

9月17日,以太坊联合创始人维塔利克·布特林(Vitalik Buterin)在X平台发文,驳斥了“日益强大的AI黑客将使网络安全变得无法防御”这一日益流行的观点。他表示,先进验证工具最终可能给防御者带来结构性优势。

布特林透露,根据他本人9月17日的声明,其净资产的90%仍投资于加密货币。他强调,继续持有加密货币的人实质上是在押注安全的数字系统能够抵御更强大的自动化攻击。

形式化验证有望助防御者占据上风

布特林论证的核心在于形式化验证(formal verification),即使用数学规范和证明来确定软件是否符合预定义属性。他类比高级数学定理证明,认为足够强大的AI可帮助证明“该程序是安全的”,即使软件本身复杂。

他指出,安全定义过窄可能忽略协议、服务器、数据库等其他组件的攻击路径,因此提议验证更完整的系统,而非仅标记少数模块为安全关键。布特林曾将AI辅助形式化验证描述为软件开发的“终极形态”,并应用于以太坊共识、零知识系统和抗量子密码学等领域。

以太坊已测试AI辅助安全

以太坊基金会协议安全团队7月报告称,协调的AI代理已在以太坊使用的系统中发现真实缺陷。其中一个确认为Rust libp2p的Gossipsub网络实现中存在远程可达崩溃漏洞,编号为CVE-2026-34219。该漏洞可通过特制PRUNE消息触发算术溢出,已在0.49.4版本修复。

团队表示,AI生成的大量候选漏洞仍需人工复现和审查,因为代理可能给出看似有效但约束不足的证明。目前形式化验证已成为以太坊协议研究计划的一部分。9月7日的协议优先级更新中,基金会将其作为跨领域工具,涵盖隐私、状态、zkEVM、后量子安全等至2029年的工作。

AI攻防两端均展现能力

另一方面,Anthropic公司在9月威胁情报报告中指出,恶意行为者正利用AI自动化漏洞研究与利用开发。其协调披露仪表板显示,截至8月26日已披露2300个AI发现的漏洞。但Anthropic也称前沿模型可用于防御,如Project Glasswing initiative与供应商合作定位高危漏洞。

布特林此前还驳斥了AI驱动安全风险会严重损害比特币信心的论点,称网络层问题可通过软件升级解决。总体而言,布特林的9月17日评论延续了以太坊现有研究方向,并未宣布新升级或强制规范。