谷歌DeepMind研究人员利用智能体AI对Signal协议的多项关键加密保证进行了数学证明，即“形式化验证”——这对这一广泛使用的加密技术以及AI本身而言都是一项里程碑式的进展。
这项工作作为概念验证项目仅用四周时间完成，其意义体现在两个方面。一方面，它为保护Signal、谷歌信息以及WhatsApp等平台上海量全球通信的加密技术提供了进一步的独立验证。另一方面，它展示了谷歌DeepMind利用一套名为AlphaProof Code的全新AI框架所具备的形式化验证能力。
更广泛地说，AI辅助的形式化验证正迎来一个发展契机，但它能否被广泛实际应用、能否有效保护大量代码，目前仍不明朗。形式化验证的支持者长期以来将其称为软件安全领域的“圣杯”，因为它利用数学方法来检验和确认软件是否按预期运行——换言之，确认软件不存在严重漏洞。
在AI时代之前，人们需要耗费大量时间来描述想要证明的软件特性，将这些描述转化为公式，然后再进行证明开发。而智能体AI能够大幅缩短后一阶段的工作时间，从而使得类似DeepMind此次对Signal的评估成为可能。但即便如此，这次分析的范围仍然有限——例如，它并未对整个Signal移动应用进行形式化验证——DeepMind的研究人员也强调，他们的发现只是这一更宏大进程中的一个里程碑。
“我们对这一结果感到非常振奋，但要将这种方法扩展到全世界所有软件，还有很长的路要走，而这正是我们想要实现的目标，”DeepMind研究科学家斯瓦拉特·乔杜里（Swarat Chaudhuri）向《连线》杂志表示。
DeepMind此次分析在所检视的Signal协议部分中并未发现新的漏洞，但当研究人员将AlphaProof Code应用于那些已知存在且早已修复漏洞的旧版本Signal时，该工具正确识别出了这些漏洞，并证明了该协议当时无法通过形式化验证。研究人员将公开他们为此次Signal协议分析所开发的规范文档和证明，以帮助推动其他形式化验证工作的开展。
尽管此次项目的速度令人瞩目，DeepMind的研究人员也指出，他们之所以能够在一定程度上抢占先机，部分得益于Signal基金会此前已经开展的一些形式化验证工作。
“此前的形式化验证只针对代码库中较小的部分，而谷歌DeepMind的方法则实现了显著的扩展，”Signal首席技术官埃伦·克雷特（Ehren Kret）在声明中表示。“随着AI驱动的安全威胁日益增长，对Signal协议实现进行严格验证，使我们对自身代码的隐私保障更加放心。”
对于那些在高风险场景中使用的关键服务而言，如果能够对每一个代码库和整个软件供应链进行形式化验证，那将是梦寐以求的事情。“如果现在你能够验证这些实现的正确性，那你就可以放心了，”谷歌云首席科学家、DeepMind研究副总裁普什米特·科利（Pushmeet Kohli）说。“你可以想象一下，银行，以及那些依赖安全保障、担心漏洞问题的其他公司，现在都可以说，‘我能证明这些特性。’”
不过，整个科技行业都存在一个悬而未决的问题：AI自动化的形式化验证能否真正实现规模化扩展——以及能否以可行的成本实现这一目标。DeepMind此次对Signal的分析是作为研究项目免费进行的，谷歌并未透露这次分析的成本。该公司也拒绝透露是否计划推出商业化的形式化验证产品或服务。
研究人员表示，他们一些关键的进展在于开发出了一种乔杜里所称的“人机协作流程”，这种流程允许智能体在几乎每个阶段都能做出贡献并进行自我修正，同时仍在关键节点寻求人类的意见和审核。“我们不希望出现这样一种‘凭感觉’的局面，即AI生成目标、AI生成证明，基本上是在做自己出的题，”乔杜里说。“中间应该有一个平衡点。”
本文最初发表于wired.com。
