Today, we’re announcing a preview release of EverCrypt, a verified cryptographic provider that offers a comprehensive collection of cryptographic algorithms. EverCrypt automatically selects the best available implementation for your platform (C or assembly); offers unified APIs for families of algorithms (e.g. hashes); and its performance is on-par with what you’d find in, say, OpenSSL. In short, EverCrypt aims to offer a verified cryptographic library that offers the same convenience as existing, industrial-grade libraries, but with added verification guarantees.

A verified cryptographic library is of crucial importance: cryptographic libraries are found in any modern software stack, and they’re incredibly hard to get right. Bugs range from memory corruption, incorrect math, to side-channel leaks and even illegal instruction errors. All of these can have incredibly painful consequences. With Evercrypt, we hope to demonstrate that one can rule out these errors with mathematical certainty, without compromising on the feature set or performance.

The technical details, including a precise description of what we verify, are available in the README. The high-level overview, with a human-readable explanation of what we hope to achieve, is on the MSR blog. For a more general perspective on software verification, Quanta Magazine just released a very accessible article that talks about our work.

What we’re hoping for with this alpha release

First, an obligatory disclaimer: this is an alpha release, and important features are missing, such as tests for non-X64 platforms; a C fallback implementation of the AES algorithms; and many others I’m sure. We also have a few admitted proofs here and there throughout our code which couldn’t be wrapped up in time for the release. These will be addressed by the end of this release cycle.

Nevertheless, the reason we’re doing an “informal” release is to gather feedback about the code, even in its current state. Things we’d love to hear about include:

  • ease-of-use of our library from C
  • whether the APIs are “idiomatic” or they could use some improvements
  • integration or build difficulties
  • things that could be improved to make this even more useful to C clients
  • most-wanted algorithms / optimized implementations (do you crave an AVX2 SHA256 or an AVX Chacha20?).

In terms of APIs, the most polished one is the hash API (EverCrypt_Hash.h); let us know if there are improvements to be enacted for this style.

Some of the improvements on the radar are: a unified error code in EverCrypt.Error; abstract C structs for all APIs, including Hash and AEAD; and many more.

Please get in touch via a GitHub issue! If sharing an experience report publicly is not possible, private emails also work.

A look behind the scenes

We call EverCrypt a “provider” because it unifies under a single interface two strands of work from Project Everest: HACL*, a cryptographic library written in Low* which generates pure C algorithms, and Vale-Crypto, a collection of assembly algorithms written in Vale.

EverCrypt is, perhaps, the first project to come out of Everest whose ownership is truly spread across all institutions currently working on Everest: Microsoft Research, INRIA, Carnegie Mellon University. It means it’s also the first instance in which we had to reconcile two independently-developed projects.

There were plenty of technical challenges which we will cover in an upcoming paper submission: verifying both the Vale and HACL implementations against the same specifications; crafting suitable interfaces to abstract away the implementation details; doing multiplexing in a style that is friendly to the C preprocessor; and many more.

But the challenge, perhaps, wasn’t so much in the verification itself, but in materializing the union of the two projects; and for that, a lot of work took place behind the scenes. We have, for the whole hacl-star repository, 110,000 lines of hand-written Low* and 25,000 lines of hand-written Vale; the latter translate to 70,000 lines of (generated) F*. Getting those in a single repository, efficiently verifying and building, was in itself a challenge. Several contributor-weeks were devoted to a unified build system; performance improvements at every level in F*; bringing back diverging abstractions into shared library modules that could guarantee safe interoperability; and many more mundane tasks that we’d all rather forget.

The work is still very much in progress and we have a long road towards a 1.0 release, but everyone has been admirably patient in the face of engineering and performance challenges. My hope is that as the technology stabilizes, we’ll be able to allocate more time to documentation and learning materials, and bring onboard more contributors who will help us grow our body of verified code.