谷歌 DeepMind 的新人工智能工具证明信号协议是安全的

谷歌 DeepMind 研究人员使用代理人工智能从数学上证明或“正式验证”信号协议的一些关键加密保证——这对于广泛使用的加密技术和人工智能本身来说是一个里程碑式的发展。作为一种概念验证项目，这项工作在短短四个星期内就完成了，其意义有两个方面。它可以作为对密码学的进一步独立验证，保护 Signal 应用程序、Google Messages 和 WhatsApp 等平台上的大量全球通信。它使用名为 AlphaProof Code 的新人工智能框架展示了 Google DeepMind 的形式验证功能。更广泛地说，人工智能辅助形式验证正在流行，但尚不清楚它的广泛使用有多实用，以及它在保护大量代码方面的有效性如何。形式验证的支持者长期以来一直将其称为软件安全领域的一种圣杯，因为它使用数学来检查和验证软件是否按预期运行，换句话说，它不存在严重漏洞。在人工智能时代之前，人们描述他们想要证明的软件的特征，将这些总结转化为公式，然后开发证明是非常耗时的。 Agentic AI 可以显着缩短后一个项目的时间，从而实现像 DeepMind 的信号评估这样的分析。但即使是这种分析的范围也有限——例如​​，它没有正式验证整个 Signal 移动应用程序——DeepMind 研究人员强调，他们的发现只是更大过程中的一个里程碑。 DeepMind 研究科学家 Swarat Chaudhuri 告诉《连线》杂志：“我们对这个结果感到非常兴奋，但在我们能够将其扩展到世界上所有软件之前，还有很长的路要走，我们希望做到这一点。” DeepMind 分析没有在它所研究的 Signal 协议部分中发现任何新的漏洞，但是当研究人员在包含已知和长期修复的漏洞的旧版本 Signal 上使用 AlphaProof 代码时，它正确地识别了这些漏洞，并表明该协议无法得到正式验证。研究人员正在发布他们为信号协议分析开发的规范和证明，以帮助其他形式验证工作。虽然该项目的速度令人瞩目，但 DeepMind 研究人员指出，由于 Signal 基金会过去进行的一些正式验证工作，他们能够在一定程度上取得领先。 Signal 首席技术官 Ehren Kret 在一份声明中表示：“虽然之前的形式验证主要集中在代码的较小部分，但 Google DeepMind 的方法可以实现显着扩展。” “随着人工智能驱动的安全威胁的增长，严格验证 Signal 协议的实现使我们对代码的隐私保证更有信心。”对于高风险环境中使用的关键服务，能够正式验证每个代码库和整个软件供应链将是一个梦想。 “如果你现在可以验证这些实现的正确性，那么你就可以高枕无忧了，”Google Cloud 首席科学家兼 DeepMind 研究副总裁 Pushmeet Kohli 说道。 “你可以想象银行，想象所有其他依赖保证并担心错误的公司，他们现在可以说，‘我可以证明这些属性’。”不过，整个科技行业的悬而未决的问题是人工智能自动化形式验证是否可以真正扩展，以及是否可以以可行的成本实现这一点。 DeepMind 作为一个研究项目免费进行了信号分析，而谷歌拒绝分担分析费用。该公司还拒绝就是否计划发布商业形式验证产品或服务发表评论。研究人员表示，他们的一些关键进展在于开发了一种“人类与人工智能协作流程”，正如 Chaudhuri 所说，该流程允许智能体在流程的几乎每个阶段做出贡献和自我纠正，同时仍在关键时刻寻求人类的输入和审查。 “我们不想要这种由人工智能生成目标、人工智能生成证明并基本上进行自写测试的氛围世界，”Chaudhuri 说。 “有一个中间立场。”