Inria MSR-Inria MSR Everest

Signal*, a verified cryptographic protocol

Signal is a secure messaging application that relies on a special cryptographic protocol for exchanging messages between participants. The Signal web application runs inside the browser using the Web Crypto API and Emscripten-generated Javascript code for encryption.

In order to make the Signal web application more secure, the Prosecco research team at Inria, in collaboration with Microsoft Research through Project Everest, developed a reimplementation of the core protocol, called Signal*, using WebAssembly. WebAssembly is a portable execution environment supported by all major browsers and Web application frameworks. It is designed to be an alternative to but interoperable with JavaScript. WebAssembly defines a compact, portable instruction set for a stack-based machine. These features make WebAssembly a better language in which to implement the cryptographic primitives that lack from the Web Crypto API, such as elliptic curve cryptography.

The WebAssembly used in this demo is generated from F* sources using the KreMLin compiler. The F* implementation, contains the cryptographic top-level functions of the Signal protocol like encrypt or respond. F* is a verification framework, that we use to prove three properties about this Signal protocol implementation:

This details of the verification of the Signal protocol is described in an article accepted at IEEE S&P 2019. The F* code is then compiled into WebAssembly using a custom, small and auditable toolchain that allows for higher assurance about the generated code, at the expense of some performance losses compared to Emscripten-generated WebAssembly. You can find the F* and Javascript sources for this modified version of the Signal protocol on GitHub.

What you can see below is Signal* running in your browser and passing some of the tests from the Signal protocol test suite. This proof of concept shows that Signal* can be made to interoperate with actual Signal-based web applications like Whatsapp or Signal.

Contact

If you have comments, questions or suggestions, you can contact the authors of the paper: Jonathan Protzenko (protz@microsoft.com), Benjamin Beurdouche (benjamin.beurdouche@inria.fr), Denis Merigoux (denis.merigoux@inria.fr) and Karthikeyan Bhargavan (karthikeyan.bhargavan@inria.fr).