README for Signal is
README describes the Signal* fork.
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
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.
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
We also modified
crypto.js to divert calls to
Curve25519 and other cryptographic primitives to use our F*-generated WebAssembly code.
Running the test suite
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
Switching Signal flavors
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
To update the
demo website with the sources from the