Formally Verified Cryptographic Web Applications in WebAssembly
| Autor: | Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan |
|---|---|
| Přispěvatelé: | Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Microsoft Research - Inria Joint Centre (MSR - INRIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Microsoft Research Laboratory Cambridge-Microsoft Corporation [Redmond, Wash.], Programming securely with cryptography (PROSECCO ) |
| Rok vydání: | 2019 |
| Předmět: |
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
business.industry Computer science Programming language 020207 software engineering Cryptography 02 engineering and technology Cryptographic protocol JavaScript computer.software_genre Internet security Toolchain Instruction set [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Server 0202 electrical engineering electronic engineering information engineering Web application Compiler business computer Formal verification Protocol (object-oriented programming) computer.programming_language |
| Zdroj: | IEEE Symposium on Security and Privacy SP 2019-40th IEEE Symposium on Security and Privacy SP 2019-40th IEEE Symposium on Security and Privacy, May 2019, San Francisco, United States. pp.1256-1274, ⟨10.1109/SP.2019.00064⟩ 2019 IEEE Symposium on Security and Privacy (SP) |
| DOI: | 10.1109/sp.2019.00064 |
| Popis: | International audience; 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 WebAssembly, 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|