Provably Secure Communication Software
Focusing on the HTTPS ecosystem, including components such as the TLS protocol and its underlying cryptographic algorithms, Project Everest began in 2016 aiming to build and deploy formally verified implementations of several of these components in the F* proof assistant.
While we have yet to complete a fully verified implementation of HTTPS, we have branched out to tackle a broader range of problems, including verified implementations of newer security protocols like QUIC, Signal and DICE, as well as securing networking infrastructure used in commerical cloud platforms.
Everest software is deployed in systems ranging from the Linux kernel and the Windows kernel to Microsoft Azure and Mozilla Firefox, improving the security and reliability of software used by billions of people every day.
Everest Artifacts with Formal Proofs
The following is a partial list of software components with formal proofs of correctness and security developed using Project Everest’s toolchain.
The TLS-1.3 record Layer
The TLS record layer is the main bridge between applications and TLS’ internal sub-protocols. Its core functionality is an elaborate authenticated encryption: streams of messages for each sub-protocol (hand- shake, alert, and application data) are fragmented, multiplexed, and encrypted with optional padding to hide their lengths
We have built and verified a reference implementation of the TLS record layer and its cryptographic algorithms in F*, reducing the high-level security of the record layer to cryptographic assumptions on its ciphers.
Our implementation has been plugged in to miTLS, a TLS library partially verified in F*, and interoperates with Chrome and Firefox, confirming that our code is compatible with other, mainstream (unverified) implementations.
HACL*, ValeCrypt, and EverCrypt: Cryptographic libraries
HACL* is a formally verified library of modern cryptographic algorithms, where each primitive is verified for memory safety, functional correctness, and secret independence. HACL* provides efficient, readable, standalone C code for each algorithm that can be easily integrated into any C project.
ValeCrypt provides formally verified high-performance cryptographic code for selected primitives in assembly language. It relies on the Vale tool to produce code and proofs in F*. Vale supports multiple platforms and proves that its implementations are memory safe, functionally correct, and that timing and memory accesses are secret independent.
EverCrypt is a high-performance, cross-platform, formally verified modern cryptographic provider that packages implementations from HACL* and ValeCrypt, and automatically picks the fastest one available, depending on processor support and the target execution environment (multiplexing). Furthermore, EverCrypt offers an (agile) API that makes it simple to switch between algorithms (e.g., from SHA2 to SHA3), and verified cryptographic data structures like Merkle trees.
Code from HACL*, ValeCrypt and EverCrypt is deployed in several production systems, including Mozilla Firefox, the Linux kernel, mbedTLS, the Tezos blockchain, the ElectionGuard electronic voting SDK, and the Wireguard VPN.
The QUIC record Layer
QUIC is a new, high-performance secure transport protocol. We model packet and header encryption, which uses a custom construction for privacy and formalize and verify its security in F* and integrate it with a provably-safe implementation of the rest of the QUIC protocol in Dafny. Our record layer achieves nearly 2 GB/s throughput, and our QUIC implementation’s performance is within 21% of an unverified baseline. For more details, see this paper.
Signal*: A verified secure messaging protocol
DICE*: A verified implementation of DICE measured boot
Measured boot is an important class of boot protocols which ensure that each layer of firmware and software in a device’s chain of trust is measured, and the measurements are reliably recorded for subsequent verification.
DICE* is a formal specification as well as a formally verified implementation in F* of DICE, an industry standard measured boot protocol. DICE* has been integrated into the boot firmware of an STM32H753ZI micro-controller, replacing an unverified DICE implementation with negligible effect on the code size and boot time. For more details, see this paper.
Tools for Program Proofs
In conjunction with our verified software artifacts, we develop a variety tools for program proofs.
F*: A programming language and proof assistant
F* is a general-purpose functional programming language with effects, based on dependent type theory and aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to OCaml, F#, C, Wasm, or ASM code. F* is the core programming and proving platform on which Project Everest is built.
Vale: A tool for verifying cryptographic primitives in assembly
Vale is a tool for constructing formally verified high-performance assembly language code, with an emphasis on cryptographic code. It uses existing verification frameworks, including both Dafny and F*, for formal verification. It supports multiple architectures, such as x86, x64, and ARM, and multiple platforms, such as Windows, Mac, and Linux. Additional architectures and platforms can be supported with no changes to the Vale tool.
Low* and KaRaMeL: A proof-oriented subset of C embedded in F*
Low* is a subset of F* and a set of F* libraries that models a fragment of the C programming language, including its memory model, stack- and heap-allocated arrays, machine integers, C string literals, and a few system-level functions from the C standard library, enabling formal proofs of low-level, sequential, imperative programs in F*. Low* programs are compilable to C by KaRaMeL. This paper provides more details.
EverParse: A parser generator for binary data formats
EverParse is a framework for generating formally proven secure parsers and formatters from domain-specific format specification languages. It produces optimized C code through the Low* toolchain which has been integrated in several projects, including our verified implementations of QUIC, DICE, and in the Microsoft Azure networking stack.
Steel: A concurrent separation logic embedded in F*
Getting started with Project Everest
Project Everest is the combination of the following GitHub projects.
- F*, a verification language for effectful programs
- miTLS, reference implementation of the TLS protocol in F*
- KaRaMeL, a compiler from a subset of F* to C
- HACL*, a verified library of cryptographic primitives written in F*, including the EverCrypt cryptographic provider.
- Vale, a domain-specific language for verified cryptographic primitives in assembly
- EverCrypt, a verified crypto provider that combines HACL* and Vale via an agile, multi-platform, self-configuring cryptographic API.
- EverParse, a library and tool to automatically generate verified parsers and serializers for binary data formats
To make things easier for prospective users, the everest script performs high-level project management and revision tracking.
Prerequisite (Windows only). Open up a Cygwin64 terminal with a Cygwin git client. Our library is a native Windows DLL but we rely on Cygwin to provide the Unix tools that many of our projects rely on.
The first step checks out the high-level
git clone https://github.com/project-everest/everest cd everest
This will ensure that your environment is sane. On Windows, this will fetch & install a proper version of OCaml and all packages for you.
If you just want to read the sources, then the step below is sufficient; it will fetch blessed versions of all the projects, which are known to work together.
At this stage, you can build HACL*, ValeCrypt and EverCrypt since the generated C/ASM is under version control. If that’s what you’re looking for, head over to the relevant documentation.
If you’d rather build the tools and verify all of Project Everest, read on.
Building all the projects together should work at any time, and be achieved by running
Testing the generated binaries can be achieved by running:
Finally, if you want to revert to a clean state, you can run:
For the lazy: Docker
Every night, we automatically build the
Linux Docker image with everything already built and verified, for you
to directly pull from the Docker
Hub, where you can find the
list of the latest images, each of which is tagged with their commit
hash on the Everest repository and is accompanied with its relevant
docker pull command to download and run it on your machine.
Then, for some image with tag
foobar, you can create and run a fresh
container with a Bash interactive command-line prompt using the
docker run -i -t projecteverest/everest-linux:foobar /bin/bash --login
(Windows Docker images are no longer working, due to this issue.)
Please file bugs if something doesn’t work!