Google DeepMind 用 AlphaProof Code 形式化验证 Signal 协议关键密码学保证
Google DeepMind 研究人员用名为 AlphaProof Code 的智能体 AI 框架,在四周内对 Signal 协议的关键密码学保证做了数学层面的形式化验证。验证未发现新漏洞,但在含已知漏洞的旧版 Signal 上能正确识别问题并证明无法通过形式化验证;研究未覆盖整个 Signal 移动应用,研究人员称这是更大进程中的一个里程碑,并将公开规格与证明以支持后续形式化验证工作。
推荐理由:报告给出 DeepMind 用 AI 形式化验证 Signal 密码学协议的范围、耗时与局限,还透露会在旧版本上复现已知漏洞。