Paper 2019/542

Formally Verified Cryptographic Web Applications in WebAssembly

Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, and Karthikeyan Bhargavan

Abstract

After suffering decades of high-profile attacks, the need for formal verification of security-critical software has never been clearer. Verification-oriented programming languages like F* are now being used to build high-assurance cryptographic libraries and implementations of standard protocols like TLS. In this paper, we seek to apply these verification techniques to modern Web applications, like WhatsApp, that embed sophisticated custom cryptographic components. The problem is that these components are often implemented in JavaScript, a language that is both hostile to cryptographic code and hard to reason about. So we instead target WebAssebmy, a new instruction set that is supported by all major JavaScript runtimes. We present a new toolchain that compiles Low*, a low-level subset of the F* programming language, into WebAssembly. Unlike other WebAssembly compilers like Emscripten, our compilation pipeline is focused on compactness and auditability: we formalize the full translation rules in the paper and implement it in a few thousand lines of OCaml. Using this toolchain, we present two case studies. First, we build WHACL*, a WebAssembly version of the existing, verified HACL* cryptographic library. Then, we present LibSignal*, a brand new, verified implementation of the Signal protocol in WebAssembly, that can be readily used by messaging applications like WhatsApp, Skype, and Signal.

Note: Typo in the email of an author on the pdf paper (berudouche -> beurdouche)

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Published elsewhere. Minor revision. IEEE Security & Privacy 2019
DOI
10.1109/SP.2019.00064
Keywords
protocolsapplicationsverification
Contact author(s)
protz @ microsoft com
benjamin beurdouche @ inria fr
denis merigoux @ inria fr
karthikeyan bhargavan @ inria fr
History
2019-05-22: revised
2019-05-22: received
See all versions
Short URL
https://ia.cr/2019/542
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2019/542,
      author = {Jonathan Protzenko and Benjamin Beurdouche and Denis Merigoux and Karthikeyan Bhargavan},
      title = {Formally Verified Cryptographic Web Applications in WebAssembly},
      howpublished = {Cryptology ePrint Archive, Paper 2019/542},
      year = {2019},
      doi = {10.1109/SP.2019.00064},
      note = {\url{https://eprint.iacr.org/2019/542}},
      url = {https://eprint.iacr.org/2019/542}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.