维塔利克·布特林：AI辅助形式化验证引领软件开发安全新纪元

币安Binance

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

官网注册  APP下载

形式化验证：新的编程范式

一种新的软件开发方法正在以太坊研究领域获得关注。开发者们开始使用低级语言或直接使用Lean（一种用于可验证数学证明的语言）编写代码。其目标是实现代码的正确性能够被自动且数学化地验证。

Buterin认为这种方法可能具有变革性，并引用了研究员Yoichi Hirai的观点，称其为“软件开发的最终形态”。该方法将效率与可读性完全分离：一个版本的代码追求运行速度，另一个版本则写得清晰易懂以供人类理解，并通过数学证明将两者关联起来。

这种方法对于ZK-EVM、抗量子签名和共识算法等高价值系统尤为重要。这些系统构建复杂，但其安全属性却能够相对直接地进行形式化表述。这种复杂性与清晰性之间的差距，恰恰是形式化验证最能发挥作用的领域。

像Arklib和evm-asm这样的项目已经将此方法应用于以太坊基础设施。evm-asm项目直接在RISC-V汇编中构建EVM实现，然后通过形式化证明其与一个可读的高级版本相匹配。

对网络安全悲观论的回应

业界一些声音认为，AI驱动的漏洞发现将使安全、无需信任的软件成为不可能。Buterin直接反驳了这一观点。他将当前阶段视为一个过渡性的挑战，而非攻击者将永久占据上风的根本性转变。他认为一旦格局稳定，防御方将比以往更强大。

他以Mozilla的研究作为佐证。Mozilla指出安全缺陷是有限的，并且防御者现在拥有一条现实的路径去发现所有缺陷。建立在“数字防御者拥有优势”这一理念上的密码朋克传统，不必被抛弃。

Buterin提出的模型将软件分为可信的安全核心和信任度较低的边缘组件。边缘组件在权限极少的沙盒环境中运行。而被刻意保持小巧的核心部分，则能充分受益于AI辅助的形式化验证。

形式化验证的局限

Buterin也谨慎地避免过分夸大形式化验证的作用。一些已记录的失败案例显示了其实际局限。

在某些约束条件根本未被指定的情况下，经过形式化验证的C语言编译器中依然出现过漏洞。2025年libcrux中的一个漏洞表明，未经验证的内部函数封装可能会在特定硬件平台上破坏输出。另一个漏洞则因已验证部分之外的代码中一个未处理的解密错误，导致了进程崩溃。

这些失败的案例模式是一致的：要么只有部分代码被验证，要么证明中从未包含某个关键属性。形式化验证并不能在人类语言的完整意义上证明软件的正确，它只能证明在特定假设下，指定的属性得以成立。

侧信道攻击构成了另一个边界。即使是一个被完美证明的加密方案，也可能通过电力波动泄露私钥。攻击者的数学模型并不总能捕捉到现实世界中所有的信息泄露类型。

Buterin的结论是审慎的：形式化验证并非一个完整的解决方案，但它是对一个已在进程中的安全趋势的强大助推剂——而AI正使这一趋势变得显著更易实现。