Original title: From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
Moustafa Said, Aurora Naska, Kevin Morio, Robert Künnemann · September 2026
Apps like Signal and WhatsApp use the Signal protocol to protect private messages. Researchers have proven on paper that the protocol is secure. However, actual apps might behave differently from the blueprint when they run. To solve this problem, researchers used a tool called SpecMon, which monitors software while it runs to check whether it follows the official security design. The researchers added tracking code into WhatsApp Web and Signal Desktop. This code records how the apps interact with the network and their digital security systems. The tool checked these live actions against formal mathematical models of the protocol. They confirmed that the live apps followed the models and kept key security features intact, specifically secrecy and authentication, which confirms who is sending the message. The testing also showed previously undocumented differences between the original Signal code library and the version WhatsApp modified.
Imagine you are following a recipe to bake a cake. You have a list of ingredients and steps. But suppose the actual ingredients in your pantry are slightly different from what the recipe assumes, and you only notice when the cake tastes off. In this paper, the recipe is the Signal protocol design, the pantry is the actual code in WhatsApp and Signal apps, and the runtime monitor is like a taste-tester that checks each step as you bake, revealing that the two pantries have different ingredients that were not listed in the recipe.
Billions of people rely on WhatsApp and Signal for private messaging. This work shows that even when a protocol is proven secure, the actual code can behave differently. By monitoring real app executions, the researchers found undocumented differences between WhatsApp's and Signal's implementations, which could hide security risks. Their method makes it possible to continuously check that apps follow the intended protocol.
The monitoring relies on the assumption that event extraction is correct and that the symbolic abstraction captures all relevant behavior. The models are built for specific versions of WhatsApp Web and Signal Desktop, and may not generalize to mobile apps or future updates. The verification of authentication and secrecy is only for core components, not the entire application. The detection of differences is based on the models, so other differences might exist.
Ask anything about this paper. Answers come from its abstract, and say so when the abstract doesn't cover your question.
From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp — Moustafa Said, Aurora Naska, Kevin Morio et al.
Abstract licence: CC0
Explanation generated by Synthesis from the abstract — it is not the original paper. This is a preprint, so it hasn't necessarily been peer reviewed.