


We include in this repo a pre-generated snapshot of the WebAssembly files, in the folder fstar/signal-wasm. We also modified crypto.js to divert calls to Curve25519 and other cryptographic primitives to use our F*-generated WebAssembly code. src/SignalCore.js is a alternative Javascript implementation of what is inside the F*-generated WebAssembly code. These functions are accessible through a wrapper called src/SignalCoreWasm.js. Src/SessionCore.js then calls the WebAssembly functions generated from F*. But cannot help and wonder whether Signal has plans of closing the source. Is there any specific reason why this is so I can see an few recent updates on the GitHub. We carved out from those files a core module of cryptographic constructions, called src/SessionCore.js in our implementation. (It conveniently only mentiones Signal protocol being open source ) There isn't one mention of it being open source on the Google play store. The main modifications to the implementation concern the files src/SessionBuilder.js and src/SessionCipher.js. We forked the official implementation of Signal in Javascript.
#SIGNAL WEB BASED CODE#
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.
#SIGNAL WEB BASED VERIFICATION#
This details of the verification of the Signal protocol is described in an article accepted at IEEE S&P 2019.

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.
#SIGNAL WEB BASED PORTABLE#
WebAssembly defines a compact, portable instruction set for a stack-based machine. It is designed to be an alternative to but interoperable with JavaScript. WebAssembly is a portable execution environment supported by all major browsers and Web application frameworks. 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. The Signal web application runs inside the browser using the Web Crypto API and Emscripten-generated Javascript code for encryption. Signal is a secure messaging application that relies on a special cryptographic protocol for exchanging messages between participants. The original README for Signal is this README describes the Signal* fork.
