Title: Project Everest: Verified Secure Compenents in WebAssembly
Speaker: Jonathan Protzenko
Summary: Project Everest is a multi-institutional effort that aims to build a stack of formally verified components for secure internet communications, notably: HACL*, the verified cryptographic library (now used by Firefox, Linux, and many others); EverQuic, a verified implementation of QUIC packet encryption and decryption; and EverParse, a library of secure parsers and serializers for binary network formats.
In this talk, I will give an overview of Everest and will present the compilation toolchain that we use to go from our source code, written in F*, to WebAssembly. I will cover its implementation via the KReMLin compiler, the challenges we encountered while compiling to WebAssembly, and future prospects related to a fully verified compilation toolchain that leverages the latest advances in WebAssembly (e.g. SIMD).