Verifying Signal and WhatsApp apps to check messaging security
From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
Cryptography and Security
Summary
Messaging apps like Signal and WhatsApp use complex protocols to keep your conversations private, but it’s hard to know if the actual apps always follow these rules perfectly. The authors developed a way to watch the apps while they run and check if their behavior matches the formal protocol models. They created detailed models for both apps and verified important security properties like who can read messages. Their approach also found previously unknown differences between Signal's original software and WhatsApp’s version. Their work shows it is possible to monitor real messaging apps for security issues with little performance impact.
Signal protocolWhatsApp Webruntime monitoringmultiset-rewrite modelsTamarin proverauthenticationsecrecycryptographic protocolsinstrumentationsecurity verification
Authors
Moustafa Said, Aurora Naska, Kevin Morio, Robert Künnemann
Abstract
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.