谷歌AI四周数学证明Signal协议安全
报价宝综合消息谷歌AI四周数学证明Signal协议安全
谷歌DeepMind的研究人员用一个名为AlphaProof Code的新型AI智能体框架，在四周内完成了对Signal加密协议多项关键安全性质的数学证明，即形式化验证。这是AI首次在如此深度上对一款大规模部署的加密协议完成验证，被业内称为里程碑式进展。
Signal协议是当今应用最广的端到端加密方案之一，Signal应用、WhatsApp和谷歌Messages都在使用。形式化验证是指用数学方法证明协议在所有条件下都满足其安全声明，不存在任何失效场景。过去这类工作几乎全靠人工，极其耗时，因此长期被视为软件安全的圣杯。
研究人员让由Gemini驱动的智能体生成了超过600万行Lean证明代码，仅把约1％的代码库标记为需要人工复核。团队强调这是一套人机协作流程：AI在几乎每个环节贡献并自我纠错，关键节点仍由人类把关。DeepMind研究员乔杜里直言，不希望出现AI自己出题、自己打分的局面。
验证结果显示，受检部分未发现新漏洞；而用该框架检测含有已知旧漏洞的历史版本Signal时，它准确找出了问题，并证明旧协议无法通过验证。Signal基金会此前的人工验证工作为本次提速打下基础，Signal首席技术官克雷特表示，DeepMind的方案让验证范围得以显著扩大。
DeepMind将公开本次验证的规范和证明，供其他研究者使用。不过成本与规模仍是未知数：谷歌拒绝透露项目花费，也未说明是否推出商用验证服务。研究人员坦言，距离验证全世界所有软件的目标还很遥远，但银行等高安全要求行业或许能率先受益。
编译自 Wired，原标题："A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure"
