Google DeepMind借助AI代理，首次将对Signal核心加密库libsignal的形式化验证推进到机器码层面。与以往主要停留在源代码或协议设计层面的研究不同，这次验证覆盖了程序编译后的实际产物，因此受到业界关注。
据台湾地区媒体IT Home于11月12日报道，DeepMind已开源其AI形式化验证框架AlphaProof Code，并宣布完成对Signal加密协议核心库libsignal的验证工作。
所谓形式化验证，是指先以数学方式定义程序必须满足的安全条件，再通过严格证明确认代码是否符合这些要求。过去相关研究多聚焦于协议本身，或针对经过改写的代码展开验证；而此次验证对象则是未经修改的真实实现代码。
在具体方法上，研究团队将基于Rust开发的libsignal封装进命令行测试程序，并将其编译为AArch64 Linux机器码，随后对机器码的执行行为进行数学分析，逐项核验其是否满足预设的安全条件。
整个项目由5名研究人员与AI代理协同完成，耗时4周，累计生成约650万行Lean证明代码。流程上，研究人员先审定安全属性，再由基于Gemini Carbon的AI代理生成证明，最后交由Lean验证器检查其数学有效性。
此次验证覆盖了用于协商初始加密密钥的PQXDH，以及在消息传输过程中持续更新密钥的Triple Ratchet机制。
研究团队重点验证了前向保密性、消息认证，以及在部分加密密钥泄露后系统恢复安全性的能力等关键条件。
除验证安全属性外，团队还测试了系统的漏洞发现能力。他们将此前已修复的两处漏洞重新引入测试程序后，系统在两种情况下都能从数学上证明其不满足既定安全条件。
不过，这并不意味着整个Signal应用已经获得完整的安全证明。此次验证仅适用于使用特定版本libsignal的测试程序，尚未覆盖群聊、多设备环境，也无法囊括所有量子计算攻击场景。
此外，部分加密运算的安全性仍建立在若干前提假设之上。DeepMind目前已公开相关证明与代码，并表示未来有望将这项技术用于医疗设备、电力系统等关键系统的安全验证。
Jae-won Choi
ittt_0801@d-today.co.kr