PaperlayerView exact revision on arXiv

Source-linked AI summary

From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp

Moustafa Said, Aurora Naska, Kevin Morio, Robert Künnemann

arXiv:2609.11882v1cs.CR

TL;DR

Formal security results for the Signal protocol do not by themselves establish that deployed messaging applications behave according to the verified models. The paper instruments Signal Desktop and WhatsApp Web, builds Tamarin-compatible SpecMon models, and finds conforming executions, verified core properties, implementation differences, and low-overhead fault detection within stated trust and abstraction boundaries.

  • Problem

    Formal guarantees for the protocol may not transfer to actual implementations, which can deviate from models; this matters particularly for closed-source messaging applications.

  • Method

    The paper instruments Signal Desktop and WhatsApp Web to extract network and cryptographic events, then builds monitorable multiset-rewrite models compatible with Tamarin.

  • Results

    Monitoring validates protocol conformance across major Signal operations, while Tamarin verifies authentication and initial-root-key secrecy and fault injection detects several security-relevant deviations.

  • Takeaways & Limitations

    The methodology provides a practical way to connect runtime monitoring with formal verification for open- and closed-source Signal-based applications.

  • Takeaways & Limitations

    SpecMon cannot detect secrets encoded as ordinary application payloads, and monitorable-to-verification transformations remain unmechanized.

Abstract

from arXiv · show

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.

1 Introduction

The paper addresses the gap between formal Signal-protocol guarantees and the runtime behavior of messaging applications. It applies SpecMon to Signal Desktop and WhatsApp Web, developing monitorable models that support verification and practical validation.

  • Formal guarantees may not transfer to implementations that omit security-relevant steps, use different primitives, or contain bugs, especially when applications are closed-source.
  • SpecMon provides dynamic, black-box compliance checking during protocol execution, complementing static techniques that require substantial proof effort or cover limited implementations.
  • The Signal Desktop case study extends prior models with PQXDH, Sealed Sender, and omitted cryptographic details, producing the most detailed Signal model to date.
  • The WhatsApp Web case study derives the first formal model of WhatsApp’s Signal-protocol implementation from application-generated traces without a previous model.
  • The methodology supports efficient monitoring and continuous validation, with WhatsApp model development, instrumentation, fuzzing, and experiments completed in three person-weeks.
  • Tamarin verifies authentication and initial-root-key secrecy for both models, while the work also identifies undocumented differences between Signal’s original library and WhatsApp’s fork.

2 Background

The Signal protocol combines authenticated key agreement with continuous message encryption, while SpecMon and Tamarin use related multiset-rewrite models for monitoring and verification. Monitorable rules add concrete implementation structure, event handling, and message formats to symbolic protocol models.

  • 2.1 The Signal Protocol: Signal combines X3DH or PQXDH authenticated key agreement with Double Ratchet message encryption, while Sesame manages sessions and Sealed Sender can provide sender anonymity.
  • 2.2 Formal Models and Monitoring: Tamarin verifies symbolic trace properties, whereas SpecMon checks whether concrete implementation events can be explained by the same multiset-rewrite rules.
  • 2.2 Formal Models and Monitoring: SpecMon separates event extraction from checking, allowing deployment-specific aggregators to forward implementation events to the monitor.
  • 2.3 Monitorable Rules: Monitorable models interpret symbolic function applications as implementation calls and use triggers, trace rewriting, and format strings to align observed events with protocol rules.
  • 2.3 Monitorable Rules: Format strings recover concrete bitstring structure for monitoring, while verification can retain symbolic tuple abstractions in the same unified model.

3 Monitoring Methodology

The methodology instruments applications, transforms concrete runtime events into monitorable traces, and checks them against extended formal models. Its assurance is trace-relative, while current deployment targets development, testing, and auditing.

  • 3 Monitoring Methodology: The monitor’s assurance is limited to trusted event extraction, symbolic cryptographic abstraction, and exercised behaviors; it misses side channels, storage behavior, and unexercised paths.Omitted events can hide invalid behavior, so complete event streams are important.
  • 3 Monitoring Methodology: The approach supports development, testing, and auditing, while production monitoring remains a future extension requiring automated instrumentation.The WhatsApp Web model, instrumentation, fuzzing, and experiments took three person-weeks, while monitor-engine improvements preserve semantics and improve scalability.
  • 3 Monitoring Methodology: SpecMon separates event extraction from model checking, using annotated libraries or dynamic browser instrumentation to log networking and cryptographic events.Signal Desktop uses annotated libraries, while WhatsApp Web uses browser instrumentation.
  • 3 Monitoring Methodology: Monitoring can begin from pre-traces that recover evolving session state from application storage and initialize the monitor.This handles sessions whose keys persist across application restarts.
  • 3 Monitoring Methodology: Trace rewriting maps implementation-specific calls and multistep operations to the model’s symbolic actions before monitoring.For example, aes_encrypt is rewritten to senc and multistep operations can be combined.
  • 3 Monitoring Methodology: Models must be extended for concrete formats, protocol features, and cryptographic details that verification-oriented abstractions may omit.The Signal adaptation adds cipher-key derivation and other implementation-observed behavior.

4 Signal Desktop

The Signal Desktop model combines and extends prior X3DH, Double Ratchet, and Sesame models to match the implementation. It includes PQXDH, Sealed Sender, concrete formats, and detailed key derivations.

  • 4 Signal Desktop: Signal Desktop monitoring covers PQXDH, Double Ratchet, Sealed Sender, session initialization, and annotated libsignal network and cryptographic functions.The open-source implementation enables the annotated-library instrumentation approach.
  • 4 Signal Desktop: The implementation uses libsignal exposed to JavaScript, with network events extracted from WebSocket handlers and session state stored in an encrypted database.Pre-traces recover session keys for monitor initialization.
  • 4 Signal Desktop: The model tracks ratchet keys and derives message and cipher keys from chain keys for encryption and decryption.It explicitly models post-quantum ML-KEM keys and the initial DH ratchet step.
  • 4 Signal Desktop: The final Signal Desktop model is the most detailed model to date, extending prior models with PQXDH, Sealed Sender, and implementation-specific protocol behavior.It covers session initialization, Double Ratchet operation, sender identity hiding, and concrete message structure.
  • 4 Signal Desktop: Signal Desktop message formats are modeled using Protocol Buffers definitions observed in the implementation traces.Format strings extend the model to cover actual message structure.

5 WhatsApp Web

The authors derive and monitor the first formal model of WhatsApp Web’s Signal implementation using browser instrumentation. Monitoring exposes engineering and feature-adoption differences from Signal Desktop, with qualified security implications.

  • 5 WhatsApp Web: Chrome DevTools intercepts WebSocket and modified-libsignal functions, selectively forwarding relevant events and cryptographic traces to SpecMon.Stack traces distinguish Signal-protocol traffic from unrelated browser traffic.
  • 5 WhatsApp Web: WhatsApp Web’s model covers Double Ratchet and X3DH and is derived directly from recorded traces without a prior formal model.This yields the first formal model of WhatsApp Web’s Signal implementation.
  • 5 WhatsApp Web: WhatsApp Web bundles separately encrypted SignalMessage objects into WebSocketMessage transmissions, with an event aggregator decoding and emitting individual messages.This avoids requiring format strings for every possible bundle size.
  • 5.5 Findings: Differences from Signal Desktop: WhatsApp Web sends read receipts outside Double Ratchet, unlike Signal Desktop, so receiving a read receipt does not trigger a DH ratchet.The observed difference means WhatsApp Web performs DH ratchets less frequently for comparable interactions.
  • 5.5 Findings: Differences from Signal Desktop: The authors do not conclude that the read-receipt difference weakens WhatsApp’s security, because healing also depends on key-material persistence they do not observe.They show no concrete attack and leave finer-grained healing analysis for future work.
  • 5.5 Findings: Differences from Signal Desktop: The studied WhatsApp Web version lacks PQXDH during session initialization and lacks Sealed Sender, unlike Signal Desktop.The paper documents these known feature-adoption differences and their behavioral consequences at the model level.

6 Evaluation

The evaluation tests SpecMon on Signal Desktop and WhatsApp Web using realistic, randomized, adversarial, and performance workloads. The models handled generated traces, detected protocol-level faults, and imposed low measured overhead.

  • 6.1 Functionality and Fuzzing: SpecMon handled about 900 Signal messages and 400 WhatsApp messages without failure, including traces totaling 25 MB and 6.5 MB.The experiments also succeeded with 50,001 consecutive messages and repeated Diffie-Hellman ratcheting.
  • 6.2 Security Faults: SpecMon detected all injected protocol-level faults, while payload-encoded secret leakage remained outside the model’s reach.Leaks in extra protocol messages and new protocol fields were detected; secrets encoded as ordinary chat content were not distinguishable from legitimate payloads.
  • 6.2 Security Faults: SpecMon detected incorrect DH-ratchet key reuse, bypassed key generation, and skipped signature checks in modified implementations.The experiments targeted both Signal Desktop and WhatsApp Web, including acceptance of arbitrary server prekey bundles.
  • 6.3 Performance Overhead: 0.082–0.336 ms per event and 22.00–53.54 MiB peak RSS were measured across Signal, WhatsApp, and WhatsApp out-of-order workloads.Signal measured 0.277–0.336 ms per event and 31.29–53.54 MiB RSS; WhatsApp measured 0.082–0.257 ms and 22.00–37.44 MiB; WhatsApp OOO measured 0.099–0.271 ms and 26.22–43.30 MiB.
  • 6.3 Performance Overhead: 0.30 ms of instrumentation overhead was measured at 50 messages, compared with a 2.76 ms uninstrumented average latency.The latency difference fell within average-latency fluctuations and decreased as the number of messages increased.

7 Verification

The authors build monitorable Tamarin models for the setup, key-agreement, and message-exchange components of Signal and WhatsApp. Verification establishes authentication and initial-root-key secrecy under stated threats, while conversation PCS is falsified as expected.

  • 7 Verification: The monitorable Signal model includes Sealed Sender for implementation fidelity, but sender privacy is not verified.That property requires observational-equivalence analysis outside the current Tamarin workflow.
  • 7.3 Properties: A responder completing PQXDH has a matching initiator session with the same parameters unless specified keys are compromised or DH is already broken.The guarantee does not cover a DH break before the responder completes the handshake.
  • 7.3 Properties: Initial-root-key secrecy holds except under specified identity-key, prekey, DH, or comprehensive key-compromise conditions.Equivalent initiator- and responder-secrecy properties were specified and proved; these are not new proofs of Double Ratchet message-key forward secrecy.
  • 7.3 Properties: Conversation PCS is falsified because multi-session clients permit parallel attacker-started sessions after long-term identity-key compromise.Modeling a single-session client would avoid one issue, but is outside the deployed-client scope.
  • 7.3 Properties: Authentication and initiator- and responder-secrecy lemmas were verified for both models, while the expected conversation-PCS counterexample was reproduced.The models also proved 12 sanity traces that safeguard executability.

8 Related Work

Prior analyses often abstract away handshake, ratchet, session, or implementation details to retain tractability. This work instead emphasizes deployed-client monitoring and broader, implementation-aligned model coverage, while making narrower security claims in some areas.

  • 8.1 Formal Analyses of Signal: The model covers X3DH, PQXDH, the Double Ratchet, and Sealed Sender, trading re-proving session/device-level DR forward secrecy for broader monitorability.Table 2 compares covered features approximately because prior models target narrower protocol fragments.
  • 8 Related Work: Computational analyses provide stronger cryptographic guarantees but idealize the specification, making direct comparison with deployed implementations difficult.This work addresses implementation alignment through monitoring rather than relying solely on specification-level analyses.
  • 8.1 Formal Analyses of Signal: Earlier Tamarin work with Sesame abstracts away X3DH and simplifies the Double Ratchet, whereas these models include key agreement and ratchet computations needed for monitoring.Verification models still merge rules and simplify implementation details to keep proof search tractable.
  • 8.1 Formal Analyses of Signal: Prior work analyzes PQXDH without the Double Ratchet, or proves message secrecy without out-of-order delivery; this work proves secrecy only for the initial secret.The comparison reflects different coverage and property targets rather than a uniform security ordering.
  • 8 Related Work: Model inference and fuzzing approaches can find implementation differences, but finite-state reconstructions may omit ratchet state and attack-finding tools are not verification methods.Static conformance analyses avoid runtime overhead on small examples but require substantial expertise and become costly as implementations grow.

9 Limitations and Future Work

The paper identifies limitations in application trust, test coverage, instrumentation portability, model reconciliation, and composed-system verification. It presents these constraints as directions for future work rather than fully solved problems.

  • Trust and Malicious Applications: SpecMon cannot detect secrets encoded as application payload because the MSR model treats payload content as an indistinguishable atom.This means payload independence from protocol secrets is an assumption about applications that are not fully trusted.
  • Functionality and Coverage: The monitor may reject untested desired behaviors, potentially causing unexpected termination in a distributed closed-source deployment.Both UI actions and network input can trigger such rejections.
  • Functionality and Coverage: The randomized fuzzer explores selected action combinations but provides no coverage guarantee.The authors propose expanding the action set and guiding exploration with coverage feedback.
  • Instrumentation: Instrumentation is application-specific, so vendor-provided standardized interfaces are needed for broadly deployable monitoring.Signal uses annotated libraries, whereas WhatsApp Web uses DevTools-based runtime wrappers.
  • Model Reconciliation: The toolchain exposes but does not automate reconciliation between verification and monitoring models, whose abstraction gap remains only informally justified.The authors argue that a model-to-model gap is preferable because it can be reasoned about, but automated reconciliation remains open.
  • Composed Systems: Holistic verification of nested TLS and application layers is prohibitively expensive, although monitoring handled tested intermediate layers effectively.The existing TLS model alone requires about a week of continuous computation.

10 Discussion and Lessons Learned

The case studies combine verification-oriented and monitoring-oriented modeling, exposing tensions between tractable abstractions and implementation-level fidelity. Practical lessons concern rule scoping, nondeterminism, fact pruning, message modeling, and reusable instrumentation.

  • Modeling: A unified model provides a shared validation point but must balance verification tractability against monitoring details such as message formats, helper computations, and persistent state.Maintaining monitorable and verification variants is harder than performing either task alone.
  • Modeling: Rule boundaries should be scoped where the first observable computation directly uses an input or freshly sampled value.The authors found this criterion sufficient for their models and beneficial for both monitoring and verification.
  • Monitoring: Accidental nondeterminism can make monitoring costly, so differentiating parameters were added to facts to restrict exploration to intended cases.SpecMon’s flexible exploration of all applicable rules can otherwise expand unnecessarily.
  • Performance: Fact pruning by role identity and local protocol state improved monitoring and verification, while mean peak memory stayed below 54 MiB across all three workloads.Pruning earlier fact arguments was cheaper than pruning later ones.
  • Modeling: Models should distinguish adversary-facing Tamarin Out facts from implementation-emitted messages so monitors do not retain events the implementation never produces.The authors used the same macro mechanism to let the monitor skip storing such facts.
  • Instrumentation: WhatsApp Web’s low-level WebCrypto chokepoints covered broad protocol behavior, and the initial model and instrumentation required two person-weeks.Revising instrumentation, adding fuzzing and out-of-order support, and rerunning experiments took one additional person-week.

11 Conclusion

The paper demonstrates runtime monitoring of Signal protocol implementations in Signal Desktop and WhatsApp Web to bridge formal models and real applications. The models validate protocol conformance, detect several injected faults, and support a practical, reproducible monitoring methodology with low measured overhead.

  • Conclusion: Runtime monitoring of Signal Desktop and WhatsApp Web bridges the verification gap between formal Signal protocol models and production messaging implementations.The work reports the first runtime monitoring of the Signal protocol in production messaging applications.
  • Conclusion: The unified artifacts include a comprehensive Signal model, the first formal model of WhatsApp’s Signal variant, monitoring methods for open- and closed-source applications, and low-overhead deviation detection.The contribution set combines model construction, instrumentation, and empirical evaluation.
  • Conclusion: SpecMon validated session initialization, symmetric ratcheting, and asymmetric ratcheting, including out-of-order delivery in the reported Signal Desktop results.The models support out-of-order messages for both applications.
  • Conclusion: Fault injection detected unexpected network outputs, malformed messages, and incorrect cryptographic-library use, but not secrets encoded as ordinary message payloads.The latter limitation is explicitly outside the reported detection capability.
  • Conclusion: The methodology offers vendors a way to check proprietary implementations within a monitored scope while retaining source-code control, and offers researchers a viable and portable workflow.The paper frames formal models as executable documentation and runtime monitors as compliance checks.
  • Reproducibility: The artifact provides monitoring scripts, pre-collected traces, evaluation outputs, and a Docker reproduction environment for the reported experiments.The container reproduces monitoring over pre-collected traces, while live executions require case-study-specific setup.

B Ethical Considerations

The study used only client-side WhatsApp Web experiments with personal test accounts and reports no unauthorized access. It did not identify a concrete WhatsApp vulnerability, while separately reporting a Signal Desktop crash after 4,348 consecutive messages.

  • Ethical Considerations: The WhatsApp Web research used personal test accounts in the client-side environment, without unauthorized access to user data or Meta infrastructure.The work was conducted for academic purposes under Meta’s Bug Bounty Policy guidelines.
  • Ethical Considerations: The study did not identify a concrete bug, security vulnerability, or demonstrable misbehavior in WhatsApp.Its findings about protocol design and feature adoption are characterized as deliberate engineering choices.
  • Ethical Considerations: Signal Desktop was reported to crash after 4,348 consecutive messages.This finding was separately reported to the developers.

D Details: Evaluation

The evaluation instrumentation supports controlled message reordering while preserving Noise transport sequence numbers. Signal Desktop and WhatsApp Web use separate instrumentation approaches, with function-level interception documented in tables.

  • D.1 Instrumentation: Signal Desktop’s instrumentation functions and corresponding symbolic operations are listed in Table 3.The table documents the functions instrumented for the client.
  • D.1 Instrumentation: WhatsApp Web’s instrumentation functions and corresponding symbolic operations are listed in Table 4.The table documents the functions instrumented for the browser application.
  • D.1 Instrumentation: Held-back messages can be released after later messages, preserving Noise transport sequence numbers while Signal messages arrive out of order.The models and artifact support out-of-order delivery experiments.
Loading 2609.11882v1…