Signal协议长期以来一直被视为端到端加密消息传递的黄金标准，爱德华·斯诺登是其著名支持者。如今，谷歌DeepMind的一项分析已“正式验证”了该协议的安全性。
除了在Signal应用中使用外，同一协议也被WhatsApp和Google Messages采用，这项工作被描述为“一项里程碑式的发展”……
“形式化验证”是指通过数学方法证明或证伪加密算法或协议在所有条件下都满足其安全声明的术语。它保证不存在协议会失败的情况。这远高于传统测试方法，后者旨在寻找漏洞，但无法保证不存在其他漏洞。
使用智能体AI进行形式化验证对密码学和AI来说都是巨大突破。然而，这在计算上极为耗时，因此谷歌告诉Wired，目前尚不清楚将其更广泛使用有多么实用。
DeepMind研究人员强调，他们的发现只是更大过程中的一个里程碑。“我们对这一结果非常兴奋，但在能够将此扩展到世界上所有软件之前还有很长的路要走，而我们希望做到这一点，”DeepMind研究科学家Swarat Chaudhuri告诉WIRED。
需要注意的是，验证是针对协议本身，而非整个Signal应用。然而，令人鼓舞的是，当针对包含已知漏洞的旧版Signal进行测试时，它识别出了这些漏洞并将其标记为未通过形式化验证。
