Google DeepMind用AI形式化验证Signal协议核心加密保障
来源标题：Google DeepMind just mathematically verified key parts of Signal
Google DeepMind研究人员利用智能体AI，对Signal协议的多项关键加密保障完成了数学证明（形式化验证）。该项目仅耗时四周，使用名为AlphaProof Code的新AI框架，既为Signal、Google Messages和WhatsApp等平台依赖的加密提供了独立验证，也展示了AI辅助形式化验证的可行性。
以下正文由 AI 翻译自 Ars Technica（原文版权归原站所有），可能存在偏差，重要内容请以原文为准。
Google DeepMind 的研究人员利用智能体 AI 对 Signal 协议的多项核心密码学保证进行了数学证明，也就是“形式化验证”——这对这一被广泛使用的密码学方案以及 AI 本身而言，都是一项里程碑式的进展。
这项工作以某种概念验证项目的形式开展，仅用四周就完成了，其重要意义体现在两个方面。其一，它是对保护着 Signal 应用、Google Messages 和 WhatsApp 等平台上海量全球通信的密码学方案的又一次独立验证。其二，它展示了 Google DeepMind 借助名为 AlphaProof Code 的新 AI 框架所具备的形式化验证能力。
更广泛地说，AI 辅助的形式化验证眼下正备受关注，但它能否真正投入大规模实际使用、又能在多大程度上保障大量代码的安全，目前尚不清楚。形式化验证的拥护者长期以来将其视为软件安全领域的某种“圣杯”，因为它用数学来检查和验证软件是否按预期运行——换句话说，就是确认软件不存在严重漏洞。
阅读全文 评论
正文由 探How 从来源站点 RSS 同步，内容未经改写；遇到排版缺失或需要图片、视频时请以原文为准。