Google DeepMind正式验证了Signal协议的部分内容——Ars Technica

Google DeepMind借助智能体人工智能，从数学上确认了Signal协议的一系列关键加密保障。一项持续四周的研究项目具有演示性质，并使用了新的人工智能框架AlphaProof Code，Ars Technica报道。

加密属性验证

形式化验证是对软件是否符合既定属性、是否不存在关键漏洞进行的数学检查。在人工智能出现之前，这一过程耗时很长：专家需要描述程序的属性，将其转换为公式，并构建数学证明。

据该媒体报道，智能体人工智能能够显著缩短创建此类证明所需的时间。同时，DeepMind的研究规模有限：它并未涵盖整个Signal移动应用程序，而是涉及协议的个别部分。

在分析过程中，研究人员未在经过验证的Signal协议部分发现新的漏洞。当AlphaProof Code被应用于存在已知且早已修复问题的旧版Signal时，系统正确识别出这些漏洞，并表明在这些漏洞存在的情况下，该协议无法通过形式化验证。

更多最新消息请关注 UA.News Telegram 频道 Telegram.

研究的局限性

DeepMind强调，该结果只是更广泛工作中的一个阶段。将人工智能辅助的形式化验证扩展至大量程序代码和所有软件系统，仍需要进一步发展。

研究人员还指出，Signal Foundation此前对代码个别部分进行形式化验证的工作，有助于更快地完成分析。DeepMind正在发布为分析Signal而创建的规范和证明，以便它们可用于其他形式化验证研究。

该公司作为研究项目免费开展了这一项目，但未披露其成本。Google也没有说明是否计划推出用于形式化验证的商业产品或服务。

DeepMind将这一方法描述为人与人工智能的协作：智能体可以在不同阶段提供帮助并修正自身工作，但在关键阶段仍设有人类参与和审查。