Formal Analysis from Design to Deployment

How Signal uses verification tools to secure their code

Karthik Bhargavan, Franziskus Kiefer

The advent of powerful AI agents has given attackers the ability to easily find and exploit security vulnerabilities, which means that traditional testing and auditing methods are no longer sufficient to protect security-critical systems. Companies like Amazon and Apple have turned to formal verification to provide strong guarantees for their core security mechanisms, but adopting a verification-oriented workflow has traditionally been considered too disruptive, time-consuming, and expensive to be practical for mainstream open-source software. This is no longer the case.

Signal is an end-to-end encrypted messenger that is used by millions of users worldwide. In the past few years, the engineers behind Signal have worked with multiple research groups to formally verify the security of their protocol designs and implementations. The most recent effort in this direction is the Signal Shot challenge, where a group of academic and industrial researchers are working to prove different aspects of the Signal ecosystem.

Let’s look a bit closer at a case study on how Cryspen and CE Labs work with Signal to improve assurance in the Signal’s new post-quantum protocol codebase.

Post-Quantum Transition for Signal Messenger

As quantum computers come closer to reality, all cryptographic systems, including Signal, are transitioning their cryptography from classical to post-quantum cryptography. The first stage of this transition at Signal was the deployment of the PQXDH Key Agreement Protocol. Cryspen and Signal collaborated on the formal security analysis of PQXDH, leading to several improvements in the protocol. The second stage of the transition was the deployment of Sparse Post-Quantum Ratchets (SPQR). This time, Signal developers decided to use formal verification throughout their workflow, from early protocol design through to the final deployed implementation.

Analyzing the SPQR Protocol Design

SPQR implements a cryptographic construction called Sparse Continuous Key Agreement (SCKA). Several SCKAs have been proposed in prior research, so the Signal engineers experimented with multiple candidate protocols before settling on the SPQR design. Each candidate was modeled and formally analyzed using the ProVerif protocol analyzer, allowing the engineers to exhaustively verify the protocol against fine-grained adversarial models and evaluate its security under different compromise scenarios. The final protocol was chosen for its balance of performance and security. In this process, formal analysis worked as an integral tool for protocol design, not just a post-hoc check on the final protocol. Only when the protocol design settled did the project transition to concrete software development.

Verifying the SPQR Protocol Implementation

Once the design space was narrowed to a few candidates, they were all implemented in Rust for testing and benchmarking. Eventually the final protocol design was refined until it was ready to be deployed in the Signal app. To ensure that this concrete implementation did not diverge from the security properties of the verified protocol design, Signal used the hax toolchain to translate the Rust code into ProVerif models. These extracted models were then verified for the same security properties as the hand-written models for the high-level protocol design. However, unlike the hand-written models, the models extracted from Rust are faithful to the implementation, capturing its serialization functions, state machines, and error handling. The analysis ensures that the protocol’s expected security guarantees hold at the level of the running code. Furthermore, incorporating hax and ProVerif in the software development process enables ongoing verification of the implementation while the code is being maintained and improved over the lifetime of the project.

An End-To-End Workflow for Improved Security Guarantees 

Analyzing the new post-quantum protocol code is only one part of the puzzle, since the Signal codebase consists of many other crucial elements. Formal verification is used in two other ways to provide higher assurance. Deploying SPQR requires an implementation of the ML-KEM post-quantum key encapsulation mechanism and Signal uses libcrux, a library that uses formal verification to provide high-assurance cryptographic implementations in Rust. Furthermore, the protocol code for SPQR is itself analyzed for runtime safety using hax and F*, ensuring that a protocol endpoint will not crash at runtime, even if an attacker were to send it carefully crafted messages.

The SPQR project provides a blueprint for using formal methods from the design process through the deployment of the implementation. Using a combination of formal verification techniques, it shows how even small open-source projects can iterate on critical security protocols with confidence without sacrificing speed or performance. We believe such processes are paramount to tackle challenges like the post-quantum transition.