You can test it by firing up a web server from the repo's root directory and then accessing the test/ directory. 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*. We carved out from those files a core module of cryptographic constructions, called src/SessionCore.js in our implementation. 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. 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. This details of the verification of the Signal protocol is described in an article accepted at IEEE S&P 2019.
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |