【CNMO科技消息】谷歌DeepMind这个研究团队, 把对Signal这个消息的安全性, 给做成了形式化验证这种工作, 并且声称这是第一次由人工智能协助去构造出证明这个东西, 然后把协议这层面所持有的安全保证, 和那一件被广泛使用着的密码学研究实现, 对应了起来。
AI示意图
这一工作的进行, 是紧紧依靠那个名为AlphaProof Code的系统来作为基础的, 而这个系统啊, 它是一个专门被设计出来应对软件形式化规约以及验证任务的, 并且它还运用了多智能体框架来进行运作。
在具体的流程安排上面, 首先会由人工去引导那个智能体来编写Lean这种语言写出来的规约内容, 同时评估机器码所代表的语义情况, 完成这一步之后，再让智能体生成相应的证明工作, 最后把这些证明交给Lean内核这个部分来进行处理, 让它能够对照着前面确定的规约内容进行一项一项的全面检查。
本次所检验的项目, 主要是涉及到Signal协议里面的PQXDH这种前量子密码的握手流程, 还有那个Triple Ratchet三重棘轮机制。
通过这样的检验工作, 我们确认了libsignal这一部分代码或者库, 它在前向保密这个方面是怎么设计的, 在身份认证这一块是怎么做的, 还有当密钥泄漏之后它是如何恢复能力的, 以及握手过程中的保密性方面也是经过验证的。
这离有益人工智能基金会在今年4月那个构想实现又走近了一步。这个基金会是想要用Lean那种形式化验证的技术, 去验证Signal协议还有其应用方面的东西。具体的操作办法是先跟好几个模型进行合作, 把Signal的安全目标转换成已经经过人工仔细审查的数学规约内容。
然后再让Gemini Carbon智能体, 根据这些规约来生成Lean语言的代码, 最终目的是为了证明libsignal这个库实现的正确性所在。
智能体这块, 累计生成的那种代码量, 都已经有650万行了, 然后团队就在那后面紧跟着做了一轮那个审计出来, 把那些需要人工再去复核的具体部分, 都给标出来了。
谷歌DeepMind的研究科学家, 同时也是得克萨斯大学奥斯汀分校的教授Swarat Chaudhuri表示, 这是一套系统, 这套系统在根本上是为了让人和AI进行协作而构建起来的。他说, 传统的方式是把定义非常清楚的问题交给AI去证明, 但是这一次首先要做的事情是弄清楚到底该证明什么内容。
