技术摘要：从规范到应用：验证 Signal 与 WhatsApp 的模型

问题陈述

尽管 Signal 协议支撑着数十亿次的加密通信（包括 WhatsApp 和 Signal），但存在一个显著的“验证差距”，即形式化安全保证与实际运行时行为之间存在脱节。广泛的研究已通过使用 Tamarin 和 ProVerif 等工具，为协议规范提供了强大的形式化安全证明。然而，这些证明依赖于抽象模型，往往忽略了实现细节，例如特定的密码学原语、消息格式或状态管理逻辑。此外，虽然 Signal 协议是开源的，但主要的实现（如 WhatsApp）是闭源的，这使得验证部署的代码是否遵循理论模型变得十分困难。静态验证技术（如代码验证、定理证明）通常需要大量的证明工作，或者仅限于特定的实现。因此，需要一种动态方法，能够验证真实世界的应用程序在运行时的执行过程是否符合其形式化协议模型。

方法论

作者通过应用 SpecMon（一种运行时监控引擎）来检查观察到的执行是否符合形式化协议模型，从而弥补这一差距。该方法主要包含三个阶段：

1. 插桩与事件提取：

   • Signal Desktop（开源）： 作者对 libsignal 库（Rust/JavaScript）进行了注解，以记录加密和网络函数的输入、输出及返回值。
   • WhatsApp Web（闭源）： 作者利用 Chrome DevTools 动态地对浏览器环境进行了插桩。他们通过将运行时堆栈跟踪和函数名称与 Signal 白皮书进行匹配，拦截了 WebSocket 调用和加密函数，从而有效地构建了对闭源实现的“黑盒”视图。
   • 事件聚合器 (EA)： 该组件负责捕获这些事件，处理预追踪初始化（从加密数据库或浏览器内存中提取会话密钥），并将标准化的事件流转发给监控器。

2. 模型构建与适配：

   • 作者开发了与 Tamarin 兼容的 多重集重写 (Multiset-Rewrite, MSR) 模型。
   • Signal 模型： 他们扩展了现有的 Tamarin 模型（X3DH、Double Ratchet），加入了后量子密钥交换 (PQXDH)、Sealed Sender 以及在实现中观察到的特定密钥派生逻辑。这造就了迄今为止最详细的 Signal 模型。
   • WhatsApp 模型： 仅通过运行时追踪，他们从零开始推导出了 WhatsApp Web 的 Signal 协议变体的第一个形式化模型。
   • 统一语言： 他们使用了一种统一的规范语言，其中格式字符串用于解析具体的位串（bitstrings）以进行监控，而符号项（symbolic terms）则用于 Tamarin 验证。追踪重写规则将实现特定的函数调用（例如 aes_encrypt）归一化为模型符号（例如 senc）。

3. 运行时监控与验证：

   • SpecMon（在线）： 监控实时事件流是否符合扩展后的 MSR 模型。它检查是否符合协议逻辑，检测诸如顺序错误、格式不匹配或无效状态转换等偏差。
   • Tamarin（离线）： 用于在模型的符号版本上形式化验证安全属性（身份验证和机密性）。
   • 验证： 作者采用随机模糊测试工具生成多样化的通信模式（乱序消息、会话中断、重试），以压力测试模型和插桩。

核心贡献

• 生产级监控的可行性： 本文展示了首次成功将 SpecMon 应用于生产规模的消息应用（Signal Desktop 和 WhatsApp Web）并保持低度测量的开销。
• 详细的 Signal 模型： 作者创建了迄今为止最详细的 Signal 协议模型，统一并扩展了先前的 Tamarin 模型，以包含 PQXDH、Sealed Sender 以及在实现中观察到的特定密钥派生步骤。
• 首个 WhatsApp 形式化模型： 他们直接从运行时追踪中推导出了 WhatsApp Web 实现的 Signal 协议的第一个形式化模型，且无需预先存在的规范。
• 安全属性验证： 使用 Tamarin 验证了两个模型的身份验证和初始根密钥（initial-root-key）的机密性。他们还在其设定中实例化了一个关于后压缩安全性（Post-Compromise Security, PCS）的不可能性结果。
• 检测实现差异： 监控揭示了原始 libsignal 与 WhatsApp 分支之间未记录的差异，具体涉及：
  • 已读回执： WhatsApp Web 在 Double Ratchet 加密层之外传输已读回执（服务端处理），而 Signal Desktop 则将它们集成到 DR 协议中。
  • 特性采用： WhatsApp Web 缺乏 Signal Desktop 中存在的后量子机制 (PQXDH) 和 Sealed Sender。

结果

• 模型符合性： 监控证实，相对于受信任的事件提取和符号抽象，这两个应用程序的观察执行均符合各自的模型。
• 故障检测： 系统成功检测到了故意注入的安全故障，包括：
  • 关键机密泄露（通过意外事件或不匹配的格式字符串）。
  • 错误的加密库使用（例如，重复使用 DH 私钥、跳过签名检查）。
• 性能： 监控引入了极低的开销。
  • 处理时间： Signal 每个事件为 0.277–0.336 ms；WhatsApp 为 0.082–0.257 ms。
  • 内存占用： 根据工作负载，峰值 RSS 在 22 MiB 到 53 MiB 之间。
  • 延迟： 插桩为 Signal Desktop 的端到端消息加密增加了平均 0.30 ms 的开销（基准约为 2.76 ms）。
• 可复现性： 整个工作流程（模型开发、插桩、模糊测试和实验）针对 WhatsApp Web 大约耗时三个人周。

意义与主张

本文声称，这项工作提供了一种通过将形式化规范与运行时行为相联系，从而建立消息应用信任度的实用方法论。其意义在于：

1. 弥合差距： 它明确地将 Signal 协议的理论保证与开源及闭源实现的实际行为联系起来。
2. 共享验证点： 通过维护一个紧密相关的监控与验证变体（基于单一 MSR 模型），该方法创建了一个共享的验证点。被接受的追踪符合可监控的变体，而文档化的转换则将其连接到证明模型，使抽象差距变得显性化。
3. 持续验证： 作者提出，可监控模型可以集成到开发生命周期中进行持续验证，作为可执行文档和深度测试工具。
4. 用户与厂商的信任： 该方法为技术型终端用户提供了一种建立应用信任的方式，同时也为厂商提供了一种系统化的方法，以记录并维护协议的正确性。

作者保持了谦逊的态度，指出该方法依赖于受信任的事件提取，无法检测事件流之外的行为（例如侧信道、内存泄漏或未执行路径上的错误）。他们还指出，虽然观察到了 WhatsApp 与 Signal 之间 DH 轮转频率的差异，但并未基于此差异演示具体的攻击，这为更细粒度的愈合属性（healing property）分析留下了未来研究空间。