From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
Researchers use the SpecMon runtime monitor to verify WhatsApp Web and Signal Desktop against formal Signal protocol models, finding undocumented libsignal fork differences.
The paper applies SpecMon, a runtime monitoring tool, to check whether executions of WhatsApp Web and Signal Desktop conform to formal models of the Signal protocol. The authors instrument both applications and build Tamarin-compatible multiset-rewrite models, including the first model of WhatsApp Web's implementation and the most detailed model to date of Signal's original protocol. They verify authentication and secrecy properties for core Signal protocol components, show monitoring detects deliberately injected faults with low overhead, and identify previously undocumented behavioral differences between the original libsignal library and WhatsApp's fork.
- First Tamarin-compatible model of WhatsApp Web's Signal protocol implementation
- Verified authentication and secrecy for core Signal protocol components
- Monitoring exposed undocumented differences between libsignal and WhatsApp's fork
- Injected security faults detected at runtime with low measured overhead
- Development and experiments required three person-weeks of effort
Full article250 words · extracted from arxiv.org · click to collapse
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.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.11882