DeepMind用AI验证Signal加密代码

Google DeepMind表示，该公司使用AlphaProof Code，对Signal消息协议参考实现libsignal中的关键安全属性进行了数学验证。这项工作耗时四周。DeepMind称，过去类似的验证工作通常需要专家团队花费数年。

这套系统由研究人员与AI代理协同完成。研究人员和AI将Signal的安全目标转化为数学规范，并由人类审核。随后，由Gemini Carbon驱动的代理生成了约650万行Lean证明代码。Lean是一种编程语言，其检查器能够验证数学证明是否符合规则。代理还标出了代码库中约1%的内容，供人工审核。

证明涵盖了哪些内容？

研究人员检查了libsignal中后量子PQXDH握手协议和Triple Ratchet的编译后机器码。他们证明了前向保密、身份验证以及设备遭入侵后的保护等特定属性。研究论文称，代码由未修改的Rust代码通过标准编译器编译而成，随后以AArch64机器码进行检查。

这项工作不再局限于证明抽象设计安全，而是将明确规定的安全保证与编译后的代码联系起来。DeepMind称，这是首次以如此深入的程度，对一种广泛部署的加密协议实现进行形式化验证。团队还将两个此前已修复的漏洞重新引入隔离版本的代码；系统生成的证明显示，存在漏洞的版本不符合所述安全属性。

这项证明有其局限

这并不意味着Signal的所有部分，或所有使用该协议的应用，都获得了不存在安全问题的数学保证。证明涵盖的是libsignal的部分选定属性，而非整个应用。它也依赖经过批准的规范、Lean检查器，以及针对底层加密例程的契约。The Register指出，这项成果并未证明实际消息字节在计算意义上的保密性；DeepMind的论文则称，证明同时采用了符号模型和计算模型，并依赖关于底层加密原语的假设。

DeepMind表示，将向其他人开放验证材料供其使用。该公司希望把这一方法应用于医疗设备固件、电网软件等领域，但也表示，要扩大这种方法的适用范围，还需要更多研究。这项工作只是朝着验证更多现实世界代码迈出的一步，并不代表那些其他系统已经通过验证。