Google AI首度证明Signal实际程序代码安全，四周完成
2026-11-12分类：人工智能 阅读（）
Google DeepMind 11 月10 日在官方部落格发表AlphaProof Code，用一组AI 代理以数学方式证明，Signal 加密协定在装置上实际执行的程序代码，符合专家设定的主要安全性质。 Signal 协定除了Signal 本身，也用在Google Messages 等通讯软体，保护数十亿则私人对话。
DeepMind 说，这是AI 第一次在这个深度，形式验证一套广泛使用的加密协定；不论用不用AI，这类协定的「实作」被完整形式验证，也是第一次。整个验证花了四周，DeepMind 说传统上要专家团队花好几年。
过去只验设计图，这次验到编译后的程式码
形式验证是用数学证明程式照规格运作，没有漏洞，被视为最高等级的资安保证，但非常耗人力。 DeepMind 说，大多数协定验证只做到设计层，证明「设计」是安全的；真实世界的漏洞，却常藏在设计和实作之间的落差。
这次AI 代理一路证明到编译后的程式码，例如装置暂时被入侵前后，讯息仍受保护这类性质，都验证到装置上实际执行的那一层，证明难度也因此大幅提高。
600 万行Lean 证明，人只需看其中1%
AlphaProof Code 把工作拆成研究团队的分工：人类专家和AI 一起决定「要证明什么」，再交给一群AI 代理去证明。
第一步，研究人员和多个模型合作，把Signal 的安全目标翻成形式化的数学规格，每一条都由人类专家审过。接着由Gemini 4 Carbon驱动的代理动手证明，写出超过600 万行Lean。 Lean 是一种用来写数学证明的程式语言，电脑会自动检查每一步。
最后，代理自己稽核证明，标出需要人类再看一次的地方，只占整份程式码的1%；其余部分由Lean 自动检查，专家只需把时间花在真正需要判断的地方。
把两个已修好的旧漏洞放回去，系统都抓得出来
为了确认AlphaProof Code 分得出正确和有问题的程式码，研究人员在隔离环境中的Signal 程式码里，重新放回两个过去真实存在、已经修掉的漏洞。两次系统都产出经机器检查的证明，指出有漏洞的版本不安全。
Signal 技术长Ehren Kret 在部落格中说，过去的形式验证只能涵盖较小范围，要确认正式上线的程式码严格符合加密设计，需要大量人工；用AI 代理把线上程式码自动翻成有效的Lean 定理是「很大的突破」。他说，AI 驱动的资安威胁越来越多，核心协定经过严格验证，让Signal 对自家程式码的隐私保证「更有信心」。
证明档已开源，下一步瞄准医疗设备与电网
DeepMind 已把这次的形式验证成果开源，并附上技术论文。 DeepMind 说，同一套方法可以用在医疗设备韧体、电网软体等关键系统，但要扩大规模还需要更多研究。
用AI 做形式验证，近期不只DeepMind 在做。 Anthropic 10 月与Theorem 合作，用Claude形式验证123 个开源函式库，过程中找出数百个错误。以太坊共同创办人Vitalik Buterin 在Devcon 8 开幕演讲中，也主张以开源、可验证取代单纯信任，点名晶片、通讯、AI 等领域都需要可以被验证。
Tags：
