发表机构
CISPA Helmholtz Center for Information Security（CISPA 亥姆霍兹信息安全中心）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究利用 SpecMon 运行时监控器，通过插桩 WhatsApp Web 和 Signal Desktop 并构建 Tamarin 兼容模型，弥合协议规范与实现间的差距，验证核心安全属性并发现库间差异。
AI 中文摘要
Signal 协议是一种著名的消息传递协议，为数十亿用户保障通信安全。它为全球使用最广泛的消息应用 WhatsApp 以及深受注重隐私用户欢迎的 Signal 应用提供支持。在计算模型和 Dolev-Yao 模型下的大量研究为该协议本身提供了强有力的形式化安全保证。然而，协议规范的保证与实现运行时实际行为之间仍存在差距。在本工作中，我们通过应用 SpecMon（一种近期提出的运行时监控器）来弥合这一差距，检查观察到的执行是否符合形式化协议模型。为此，我们对两个应用（WhatsApp Web 和 Signal Desktop）进行插桩，以捕获它们与网络和密码组件的交互。利用该插桩，我们开发了两个与 Tamarin 兼容的多重集重写模型，从而实现验证。我们推导出 WhatsApp Web 对 Signal 协议实现的第一个模型，以及迄今为止对 Signal 原始协议最详细的模型。监控确认观察到的执行符合这些模型，相对于可信事件提取和符号抽象而言。对于 Signal 协议的核心组件，我们验证了认证和保密属性。最后，监控揭示了原始 libsignal 库与 WhatsApp 分支之间先前未记录的差异。我们评估了我们的方法并展示了其可复现性。开发 WhatsApp Web 模型、对应用进行插桩、添加模糊测试以及运行实验共花费了三个人周。我们还展示了在实测环境中低开销下对真实世界应用的高效监控以及检测故意注入的安全故障。
英文摘要
The Signal protocol is a prominent messaging protocol that secures communication for billions of users. It powers WhatsApp, the most widely used messaging application worldwide, and the Signal app, popular among privacy-conscious users. Extensive research in the computational and Dolev-Yao settings provides strong formal security guarantees for the protocol itself. However, a gap remains between the guarantees of the protocol specification and the implementation's actual behavior at runtime. In this work, we bridge this gap by applying SpecMon, a recently proposed runtime monitor, to check whether observed executions conform to formal protocol models. To this end, we instrument two applications (WhatsApp Web and Signal Desktop) to capture their interactions with the network and the cryptographic components. Using this instrumentation, we develop two multiset-rewrite models that are compatible with Tamarin, thus enabling verification. We derive the first model of WhatsApp Web's implementation of the Signal protocol and the most detailed model to date of Signal's original protocol. Monitoring establishes that observed executions conform to these models, relative to the trusted event extraction and the symbolic abstraction. For the core components of the Signal protocol, we verify authentication and secrecy properties. Finally, monitoring reveals previously undocumented differences between the original libsignal library and WhatsApp's fork. We evaluate our methodology and demonstrate its reproducibility. Developing the WhatsApp Web model, instrumenting the app, adding fuzzing, and running the experiments took three person-weeks. We also demonstrate efficient monitoring of real-world applications and detection of deliberately injected security faults, with low overhead in our measured setting.
Comments16 pages, 3 figures, 4 tables. Full version of the corresponding ACM CCS '26 paper
