以太坊联合创始人 Vitalik Buterin 表示,AI 驱动的黑客攻击的兴起并不会让网络安全变成一场无法取胜的较量,他转而指向形式化验证,将其作为证明软件安全的一种途径。他认为,开发者无需依赖漏洞的发现,而是可以用数学方法证明程序满足既定的安全需求。

在 5 月 18 日发布于 X 的博客文章中,Buterin 提出,AI 可以让这种验证在规模化场景下变得切实可行。他表示,这一方法对关键系统最为重要,包括密码学、消息协议和区块链软件。

安全覆盖须先被定义,才能被证明

Buterin 表示,要证明一个程序是安全的,首先需要定义安全究竟意味着什么。他以加密即时通讯应用 Signal 为例,指出仅靠加密并不能覆盖所有安全问题。一个完整的定义可能需要考虑消息伪造、投递失败、消息重放、设备被入侵以及密钥泄露等因素。

硬件则带来更多复杂性。物理信号可能泄露信息,而消息大小、发送者身份和时序等细节本身也可能暴露信息。综合来看,这些考量因素可能使安全定义超过 1,000 行代码。尽管如此,Buterin 认为,与底层实现相比,定义仍是验证时更小的目标范围。

形式化验证面向整个程序

形式化验证并非新概念:它早已应用于航空和医疗软件等安全攸关领域,在这些领域失败代价高昂,但所需的投入使其在通用开发中一直较为罕见。从历史上看,开发者通常只验证由他们自己认定的安全关键代码段,这主要是因为验证需要大量工作。Buterin 认为,AI 可以改变这一局面,使全程序验证更加切实可行,并将覆盖范围扩展到数据库、网络、缓存层以及其他组件。

他将这一目标与防守方抢在攻击者之前发现漏洞的传统模式区分开来。在他的方案下,软件通过证明其满足安全需求而变得更有韧性。他表示,当不同团体确立各自的需求时,定义也可以进行组合;如果两个定义无法共存,开发者可以隔离底层的设计冲突。不过他也承认,某些用户界面仍然更难处理。

以太坊软件面临复杂的验证需求

Buterin 指出,消息传递协议、沙盒、SNARKs——即证明某项计算被正确执行的紧凑密码学证明——以及全同态加密(允许直接在加密数据上进行计算)等,都是定义与实现之间的区分可能产生重要影响的领域。他将这一方法直接与以太坊的发展方向联系起来,表示区块链需要更强的软件安全性,尤其是在追求可扩展性和隐私的系统之中。

这一背景凸显了利害关系:区块链软件是开源的,其支撑的网络直接托管资产,同一份代码对攻击者和防守者同样可见——在这种条件下,不依赖于谁先发现漏洞的保障便具有特殊分量。

他的论证核心在于数学验证,而非仅仅依赖漏洞发现。他表示,验证必须超越被选定的代码段:定义需要细致的工作,而实现则仍需接受形式化检验。在他看来,AI 可以承担这一过程的规模压力,数据库、网络、缓存及其他组件。值得观察的问题是,AI 辅助工具能否将全程序验证带入生产规模下的常规实践,包括他所指出的最难处理的用户界面。