From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
[Kryptografia i bezpieczeństwo] Autorzy: Moustafa Said, Aurora Naska, Kevin Morio i 1 więcej
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 comp…
- Kategoria arxiv
- cs.CR
- Kategoria
- Kryptografia i bezpieczeństwo