资金费率
资金费率热力图
多空比
大户多空比
币安/欧易/火币大户多空比
Bitfinex杠杆多空比
账号安全
资讯收藏
自选币种
谷歌DeepMind利用AI代理对Signal加密协议进行数学验证
谷歌DeepMind利用AI代理，对Signal加密协议中一对一聊天代码的核心安全性质进行了数学验证。该分析历时四周，结果并未涵盖群组对话或整个Signal应用程序的验证。
10日，谷歌DeepMind在官方博客、技术论文及证明资料中公开了利用“AlphaProof Code”的研究成果。AlphaProof Code是一种形式化验证框架，它基于人类设定的安全条件，由AI代理编写实际代码的证明。
形式化验证不同于通过输入部分数据来查找错误的测试方法。它将代码必须遵守的条件以数学方式表达，并证明执行结果是否满足这些条件。
研究中，研究人员负责确定需要证明的安全性质并编写规范文档供审查。AI代理生成的证明必须通过Lean检查器的验证才能获得认可，结论并非仅凭代理的判断得出。
验证对象是由libsignal 0.105.4和SPQR 1.6.0构建的一对一聊天可执行文件。研究人员将未修改的库封装为命令行工具，并编译为AArch64机器码进行分析。
验证的功能包括用于协商加密密钥的PQXDH（初始握手）以及用于每条消息更新密钥的Triple Ratchet（三重棘轮）。Signal协议系列不仅应用于Signal应用，还广泛用于Google Messages、WhatsApp和Meta Messenger等。
论文将前向保密性（确保过去的消息不会因后续密钥泄露而暴露）、入侵后安全性（密钥泄露后恢复保护能力）、对方认证及初始连接的秘密性列为验证目标。消息机密性和真实性验证也包含在内。
研究分别在符号模型和计算模型中展示了结果。符号模型将密码运算视为理想对象，而计算模型则假设攻击者的计算能力受限，以此分析安全性质。
两种模型的保障范围并不相同。符号模型涵盖了即使面对量子攻击者破坏Diffie-Hellman密钥交换时，仍能保证初始连接秘密性的情况；而计算模型未针对量子攻击者，且未将SPQR应对量子攻击的恢复性质纳入证明范围。
此次研究不仅限于协议设计文档，还将编译后的可执行文件行为与规范进行了对照。不过，验证对象是研究人员创建的命令行可执行文件，而非Signal应用程序本身。
结果基于一定的前提假设。研究假设密码运算及部分库功能按约定条件运行，并将Lean检查器和AArch64语义模型的可信度纳入考量。
验证范围仅限于两个用户之间的对话。群组消息、多设备状态以及Signal应用本身未被包含，研究者在论文中明确指出了这一局限性。
为了确认验证方法能否发现缺陷，研究人员将已发现并修复的两个Bug重新植入隔离的代码中进行测试。在这两种情况下，机器验证均得出了安全命题不成立的结果，但这并非旨在发现新的漏洞。
研究团队五名成员并行工作四周，创建了约650万行的Lean证明代码。论文指出，证明所需的信任规范和AArch64语义模型约为2.6万行。
Signal首席技术官Ehren Kret表示：“现有的形式化验证通常专注于代码的微小部分，而谷歌DeepMind的方法极大地扩展了验证范围。”Kret对这种在更广泛范围内验证协议实现的做法给予了高度评价。
《WIRED》杂志指出，本次研究是否真正解决了AI辅助形式化验证的实际可扩展性和成本问题尚不明确。谷歌尚未公布分析成本或商用验证产品/服务的发布计划。
论文提出将群组消息、发件人隐私功能及服务器端协议作为后续验证的范围。谷歌DeepMind已公开了相关规范和证明资料。
