谷歌DeepMind用AI形式化验证Signal加密
据外媒报道，谷歌DeepMind（Google DeepMind）研究人员利用智能体AI对Signal协议若干关键加密保证进行形式化验证，并在四周内完成概念验证。该工作为Signal应用、Google Messages和WhatsApp等平台的通信加密提供独立校验，也展示AlphaProof Code在软件安全验证中的应用潜力。
驱动中国11月12日消息，据 Ars Technica 报道，谷歌DeepMind（Google DeepMind）研究人员近日使用智能体AI（agentic AI）对Signal协议中的若干关键加密保证进行数学证明，也就是“形式化验证”。这一进展被视为广泛使用的加密技术与AI领域的一次标志性事件。
报道指出，该工作以概念验证形式开展，耗时约四周。其意义首先体现在对Signal加密算法的独立校验：Signal应用、Google Messages和WhatsApp等大量全球通信平台依赖相关协议保护消息安全，形式化验证为这些基础密码学保证提供了新的技术确认。
其次，该案例展示了谷歌DeepMind在形式化验证方向上的能力。研究团队使用了名为AlphaProof Code的新AI框架，将AI用于数学证明和协议正确性检查，而不是仅停留在自然语言问答或代码生成层面。
形式化验证在软件安全领域长期被视为“圣杯”式目标。其核心思路是用数学方法检查软件或协议是否按预期运行，从而在理论上排除关键漏洞。相比传统测试只能覆盖有限场景，形式化验证试图对特定安全属性给出可证明的结论。
不过，报道也强调，AI辅助形式化验证目前仍处在快速发展阶段。它是否能够在更大规模代码库、更复杂工程环境中广泛落地，以及能否有效保障海量代码安全，仍有待观察。此次针对Signal协议关键加密保证的验证，更多体现的是阶段性突破和方法论价值。
从行业角度看，AI与形式化验证结合正在成为软件安全、密码协议审计和可信计算的新兴方向。Signal协议因端到端加密和公开协议规范而受到关注，若AI工具能够持续降低证明门槛，未来可能推动更多关键通信基础设施接受类似数学校验。