网络攻击愈发猖獗，防御方能否用AI扳回一城？

截图来自Anthropic官网

AI正在颠覆软件行业的方方面面，但在安全领域，表现却一直不尽如人意。尤其在AI生成代码带来更多隐患，而黑客又得以利用AI大规模、低成本地寻找并攻击安全漏洞时，防御一方往往疲于奔命，甚至难以招架。

仅10月中旬以来，重大网络安全事件就频频发生，先是编程智能体OpenCode被攻击泄露用户第三方模型密钥，随后全球近七成网站使用的PHP开源编程语言又被爆出发现重大漏洞，不少网站因此关停。Axios最新报道还爆料称，AI Agent正在对美国银行系统发起“总攻”，其速度超过了金融机构的反应能力，带来重大安全风险，摩根士丹利、美国银行等主流机构都在加急处理。

在攻击一方愈发猖獗之际，人们尤其关注网安领域如何更好利用AI，拿出更好的应对方案。

10月23日，Anthropic与Theorem Labs团队发布了一份名为《大模型正让形式化软件验证在更大规模上变得可行》（LLMs are making formal software verification feasible at a much larger scale）的报告。虽然题目看似有些垂直、学术，但正是在网安问题愈发急迫之际，这份报告在开发者社区引发了广泛关注。

发现漏洞证明安全

根据报告，Anthropic的Claude模型针对123个开源软件库中的239个程序入口，生成了约1.8亿行Rocq证明代码，并在此过程中发现并修复了数百个Bug。其中包括一些曾历经数万亿次测试，但仍在多年的运行中一直未被发现的漏洞。

除了更快、更精准地找出漏洞外，这项研究的核心突破在于，研究团队将验证推进到了汇编指令层面，以RISC-V指令集为基础进行证明。

有开发者在讨论中解读称，相关研究试验的最重要意义在于，在安全领域，AI以往更多用来“查虫”，但这只是对传统软件测试模式的一种提速、提效而已，本质来说，无论测试多少次，都很难穷尽所有可能情况，也避免不了留下漏洞，让黑客有可乘之机。而形式化验证则是通过数学证明，确认程序在给定条件下满足特定安全性质。

过去，这项工作高度依赖专业人员，成本高、耗时长，很难大规模应用于普通软件。但研究显示，随着大模型智力的不断提升，Agent调用、主动执行任务能力的加强，这项工作终于得以规模化。

Anthropic方面也指出，大多数软件都存在漏洞，而AI现在可以轻松发现并利用这些漏洞。如今，主流的网络防御手段已无法满足要求，更需要的是证明代码无漏洞的可靠方法。而此次公布的相关研究，是首次大规模利用AI在汇编代码层面将形式化验证应用于生产软件，让以往显得“不切实际”的需求终于成为了现实。

能否扭转攻防局势？

通过不断进化的AI能力和能在现实中跑通的大规模形式化验证，网络安全领域的防御方能够发现传统测试难以触及的缺陷。也有利于将安全检查前移到开发阶段，在代码上线之前发现问题，而不是等到漏洞被攻击者利用后再紧急补救。

但目前来看，想要真正扭转攻防局势，还不那么容易。

首先，根据报告和相关解读，形式化验证并不意味着能够证明整个软件“绝对安全”。它只能证明程序在特定假设、约束和验证范围内满足预设性质。如果规范本身存在缺陷，或者验证范围之外还存在漏洞，攻击者依然可能找到突破口。对于复杂的软件系统而言，如何确定验证目标、处理第三方依赖，以及将修复方案安全地部署到生产环境，仍然需要大量工作。

更现实的挑战在于，攻击者和防御者使用AI的成本并不对等。攻击者只需要找到一个可利用的漏洞，就可能获得入侵机会；防御者却必须保护整个系统，不仅要发现漏洞，还要判断风险、验证修复，并避免修复过程引入新的问题。即使AI能够将漏洞发现和代码验证的成本大幅压低，也不意味着防御方可以立即完成所有这些工作。

此外，还有开发者提到，形式化验证可能会拖慢开发速度，在AI驱动下软件开发已经开启不断提速的模式，能否为了安全慢下来可能会演变成现实中的两难问题。还有开发者担心，AI生成的证明策略可能“绕过关卡”，产生人类难以审查的冗长证明，最终脱离人类能够监测、管控的能力范围，形成更严重的问题。

虽然相关研究还无法马上扭转攻防局势，但开发者社区内的多数讨论还是对新的进展抱持乐观态度，认为变化已经发生，或许不久就将迎来转机。

不少开发者发帖称，随着相关研究在现实场景的普及，可能会成为塑造未来软件开发模式，改变整个安全体系的工作方式的重要一环，知名AI与Web技术博主Pratham也表示，这可能是“目前AI所取得的成就中明显被低估的一个”，称随着网络安全问题变得更加棘手，“我们尤其需要在这一领域取得更多进展”。（本文首发于钛媒体APP，文｜飞向Tai空）