SOIL Seminar: Project Everest: Verified Secure Compenents in WebAssembly
From Ross Tate February 01, 2021
10 plays
10
Related Media
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).
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).
- Tags
- Appears In
Link to Media Page
Loading
Loading…