[CNMO科技消息]谷歌DeepMind的研究团队完成了对Signal消息安全性的形式化验证，并称这是首次由AI协助构造出证明，把协议层面的安全保证与一款被广泛使用的密码学实现对应起来。

AI示意图

这项工作依托AlphaProofCode完成，这是一个用于软件形式化规约与验证的多智能体框架。流程上，先由人工引导的智能体编写Lean规约、评估机器码语义，再由智能体生成证明，交由Lean内核对照规约逐项检查。被验证的对象是Signal的后量子PQXDH握手和TripleRatchet，由此确认了libsignal在前向保密、身份认证、密钥泄露后的恢复能力以及握手保密性方面的设计。

这距离有益人工智能基金会今年4月提出的构想近了一步：该基金会希望用Lean形式化验证Signal协议与应用。具体做法是先与多个模型协作，把Signal的安全目标转成经人工审阅的数学规约，再让GeminiCarbon智能体据此生成Lean代码，证明libsignal实现的正确性。智能体累计生成650万行代码，团队随后做了一轮审计，标出需要人工复核的部分。

“这是一套从根本上为人与AI协作而构建的系统，”谷歌DeepMind研究科学家、得克萨斯大学奥斯汀分校教授SwaratChaudhuri说。他表示，传统做法是数学家把定义清晰的问题交给AI去证明，而这次首先要弄清楚该证明什么。