DeepMind用AI形式化验证Signal协议部分内容

Google DeepMind的研究人员展示了一种AI系统如何以数学方式证明Signal消息协议的重要安全属性。团队使用名为AlphaProof Code的新框架，对多项密码学安全保障进行了形式化验证。这项工作耗时约四周，属于研究项目，并非商业产品。在研究人员检查的部分中，没有发现新的漏洞；将AI用于该协议的旧版本时，它则正确标出了早已修复的缺陷。

形式化验证是用数学方法检查软件是否严格按预期运行，确保没有隐藏漏洞。过去，这一过程需要专家编写详细规范、将其转换为公式，再构造证明——工作量很大，可能耗时数月。DeepMind让具备自主设定并推进子目标能力的智能体AI承担大部分繁重工作，将耗时缩短至数周。研究人员表示，AI在关键步骤仍需要人工监督，但也能自行提出证明并修正错误。

Signal首席技术官Ehren Kret指出，过去的验证工作只覆盖了少量代码片段。他表示，DeepMind的方法可以“显著扩大”可验证的范围。团队将他们编写的规范和证明公开，供其他团队在此基础上开展工作。尽管成果令人鼓舞，DeepMind也提醒，要将这种方法扩展到整个应用或完整的软件供应链仍面临挑战；AI驱动验证的成本也尚未披露。

为何重要

如果AI能够可靠地证明密码协议的安全性，Signal、Google Messages、WhatsApp等应用的日常用户就能更有信心地相信自己的消息受到隐私保护。对于依赖加密通信的企业——包括银行、医疗机构和记者——这项技术未来或能提供可依法验证的保证，证明其软件不存在重大缺陷。