DeepMind用AI工具形式化验证Signal协议安全

Google DeepMind 研究人员使用名为 AlphaProof Code 的新 AI 框架，在四周内形式化验证了 Signal 协议按预期运行。该分析未在已检查的协议部分发现新漏洞，但在含已知旧漏洞的旧版 Signal 上正确识别出问题并显示协议无法通过形式化验证。 DeepMind 研究科学家 Swarat Chaudhuri 表示，这是将形式化验证扩展至全球所有软件目标中的一个里程碑，仍有很长的路要走。研究人员同时公开了为此次分析开发的规范与证明，以协助其他形式化验证工作。(WIRED)