Formally Verified Cryptographic Web Applications in WebAssembly

Explore a 19-minute IEEE conference talk on formally verified cryptographic web applications in WebAssembly. Delve into the development of a new toolchain that compiles Low*, a subset of the F* programming language, into WebAssembly. Learn about two case studies: WHACL*, a WebAssembly version of the verified HACL* cryptographic library, and LibSignal*, a new verified implementation of the Signal protocol in WebAssembly. Discover how these advancements can be applied to modern web applications like WhatsApp, enhancing security in cryptographic components. Gain insights into the benefits of targeting WebAssembly over JavaScript for cryptographic code, and understand the focus on compactness and auditability in the compilation pipeline. Examine the verification process, implementation details, and performance implications of this approach to building high-assurance cryptographic libraries and protocol implementations.

Introduction
Contributions
Key Points
Verification
Implementation
Why WebAssembly
Summary
Verification Results
API Replacement
Performance