AlphaProof Code：AI证明Signal代码的安全属性
· BehindLines 编辑部
Google DeepMind的研究人员表示，他们借助人工智能代理，证明了Signal消息协议所依赖的真实代码的多项安全保证。据DeepMind的博文称，这将是首次由AI以如此细致的程度对广泛使用的密码协议进行形式化验证；The Register报道说，这是研究人员的说法。
团队式方法
该系统名为AlphaProof Code。据DeepMind介绍，人类专家和多个语言模型先把Signal的安全目标转化为数学规范，由人员逐条审阅。随后，代理用Lean编写证明，Lean是一种其检查器会自动验证推演的语言。据The Register报道，代理生成了650万行Lean代码；DeepMind则称超过600万行。之后它们对这些证明进行审计，标出约1%的代码交由人类再看一遍，DeepMind称这大大节省了时间。
证明了什么
DeepMind强调，这些证明针对的是编译后的代码，而不只是协议的理论框架。例如，它们涵盖设备被短暂入侵前后对消息的保护。The Register还提到前向保密、身份验证和初始密钥交换的保密性。为确认该方法能区分正确代码与有缺陷的代码，团队把两个已修复的真实漏洞放回Signal代码的隔离版本；每一次，系统都给出了经机器验证的证明，表明该版本不安全。
已承认的局限
The Register指出，结果仍属理论性质：它以假定完美的密码学为前提，并不保证字节的计算保密性。据该媒体引述的作者说法，这项工作由五个人花了四周，消耗了“相当多的token”。他们回顾说，验证seL4微内核耗费了20人年，CompCert编译器的开发用了六年。
Signal首席技术官Ehren Kret在DeepMind的博文中表示，这种方法明显扩大了形式化验证的范围。研究人员之一Swarat Chaudhuri对The Register说，下一个难题将是决定该规定什么，而不是生成证明。
为什么重要
DeepMind指出，现实中的漏洞常常藏在协议设计与实现之间的差距里，而这些证明正是要弥合这一差距。该公司认为这为保护医疗设备固件、电网软件等其他重要系统提供了基础，同时说明推广到更大规模仍需继续研究。