AlphaProof Code形式化验证Signal协议实现

近日，谷歌旗下深度思维研究人员发布名为阿尔法证明代码的新框架，首次利用人工智能智能体对信号加密协议的实际实现代码完成深度形式验证。信号加密协议为数十亿私密通信提供底层安全保护，其代码级验证长期被视为难题。该框架将形式验证按科研团队模式分工，人类专家与多模型人工智能协作将安全目标转化为数学规范，并由基于谷歌大模型的智能体自动生成超过六百万行利恩证明代码。系统随后自动审计，仅将约百分之一需要人类判断的代码标记复核，大幅降低人工成本。 研究人员验证的是编译后运行在设备上的代码满足关键安全属性，包括设备临时被攻破前后仍能保护消息安全，因此桥接了设计规格与实际实现之间常被忽视的风险缺口。整个流程在四周内完成，而传统类似验证往往耗时数年。为检验框架能否区分正确代码与缺陷代码，团队在隔离版本中重新引入两个曾修复的真实漏洞，系统均生成机器可检查的证明，表明对应版本不安全。谷歌旗下深度思维称，这是首次通过人工智能对广泛部署加密协议实现进行如此深度的形式验证，也是首次以任意方式完成该级别协议实现验证，显示人工智能可显著提升软件安全审计与形式化保障效率。