The original README for Signal is README.LIBSIGNAL.md; this README describes the Signal* fork.
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:
- memory safety;
- secret independence (absence of some timing attacks);
- functional correctness, compared to a concise functional specification.
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.
We forked the official implementation of Signal in Javascript. The main modifications to the implementation concern the files src/SessionBuilder.js and src/SessionCipher.js. We carved out from those files a core module of cryptographic constructions, called src/SessionCore.js in our implementation.
src/SessionCore.js then calls the WebAssembly functions generated from F*. These functions are accessible through a wrapper called src/SignalCoreWasm.js. src/SignalCore.js is a alternative Javascript implementation of what is inside the F*-generated WebAssembly code.
We also modified crypto.js to divert calls to Curve25519 and other cryptographic primitives to use our F*-generated WebAssembly code.
We include in this repo a pre-generated snapshot of the WebAssembly files, in the folder fstar/signal-wasm. You can test it by firing up a web server from the repo's root directory and then accessing the test/ directory.
To switch between the all-Javascript implementation of Signal and the implementation using WebAssembly compiled from F*, use:
make vanilla
and
make fstar
In order to use make fstar above and re-generate the WebAssembly artifacts, you need to setup the F* toolchain. See the README.md in the fstar folder.
To update the demo website with the sources from the src and fstar directory,
use make update-demo.