This post has been republished via RSS; it originally appeared at: Microsoft Research.
Project Everest is a multiyear collaborative effort focused on building a verified, secure communications stack designed to improve the security of HTTPS, a key internet safeguard. This post, about the high-performance industrial-grade EverCrypt cryptographic provider, is the second in a series exploring the groundbreaking work, which is available on GitHub now.
If you’re reading this blog post right now, you’re likely using HTTPS, the most popular application of the Transport Layer Security (TLS) protocol. In fact, if you’ve logged in to a website, checked your email, ordered a product, or banked online today, you’ve used it. Just check out the URL in your address bar. An internet standard, TLS powers most secure communications over the internet, ensuring all clients and servers can interoperate with each other.
Delivering an implementation of TLS that guarantees with mathematical certainty your communications will be confidential and protected is a vast and ambitious effort. Like the building of a pyramid, it requires a strong foundation. Such an implementation needs successive verified software layers, beginning with the raw cryptographic algorithms, followed by a cryptographic provider. A crucially important component, the cryptographic provider orchestrates these standalone algorithms into a unified collection to meet the security needs of the protocol. Today, we’re happy to introduce the first fully verified cryptographic provider.
EverCrypt—developed and verified by the Project Everest team—offers the same features, convenience, and performance as popular existing cryptographic libraries without the bugs that leave protocols and applications vulnerable. Usable by verified and unverified clients alike, EverCrypt emphasizes both multiplatform support and high performance. We accomplish this by producing both platform-agnostic C code and optimized assembly code for specific hardware targets through the combination of two components of Project Everest: the HACL* cryptographic library developed jointly between Inria and Microsoft Research and the Vale-Crypto library of assembly primitives developed collectively between Microsoft Research and Carnegie Mellon University.
The case for verification
Historically, writing a high-quality, trustworthy cryptographic library has been a difficult task, and many of the bugs found in security applications like TLS turn out to be in this underlying layer. These bugs are often a result of extremely complex cryptographic implementations that have been designed to achieve maximum performance. For each algorithm, there are dozens of implementations, each hand-tuned to a specific platform so the implementation can leverage vector or crypto-specific instructions. This practice—known as implementation multiplexing—allows a library to provide high-performance implementations on popular hardware platforms while still providing a fallback implementation that’ll work on any platform. For instance, one may find several versions of the AES block cipher, some using SSE, AVX, or NEON, or even the dedicated AES-NI collection of instructions.
In light of this complexity, it’s no surprise existing crypto libraries have bugs. After all, who among us can truly scrutinize half a dozen slightly different assembly implementations and spot a bug—for example, a forgotten carry-bit propagation—that testing has an infinitesimally small chance of finding?
The research community has recognized this as an urgent issue and over the past few years has produced several verified implementations of individual algorithms. While these developments have advanced our understanding of the research area, they do not provide the kind of industrial-grade features developers have come to expect from popular established libraries such as Microsoft Windows Cryptography API: Next Generation, OpenSSL’s libcrypto, or libsodium.
A high-performance industrial-grade provider—minus the bugs
To meet the needs and expectations of programmers today, a cryptographic library should possess three features:
- Comprehensiveness: Application developers want a single library that covers all of the functionality they’ll need—asymmetric and symmetric encryption and signing, hashing, and key derivation, at the very least.
- Agility: A modern cryptographic library should provide multiple algorithms for the same functionality and all of the algorithms should employ a single unified API to make it simple to change algorithms if one is broken.
- Multiplexing capabilities: The library should support multiplexing but make these choices automatically rather than force the developer to do so.
With EverCrypt, we deliver this and more. EverCrypt comprises a comprehensive suite of algorithms that includes block ciphers, elliptic curves, and hash functions. To build cryptographically agile applications, developers can use the EverCrypt interface to easily switch from the algorithm SHA2-256 to SHA3-512, for instance. As far as multiplexing, we’ve designed EverCrypt to choose the best implementations based on the features of the processor it’s running on. And we’ve verified the entire provider, which distinguishes it from other libraries available today.
Performance and safety
By using the F* programming language for all our verification results, we’ve enabled EverCrypt to perform verified implementation multiplexing and algorithmic agility. No matter which implementation or algorithm is called, the same cryptographic guarantees apply. For verified clients of EverCrypt, the details of multiplexing and agility are intentionally hidden, providing a clean interface that serves as a robust foundation for the subsequent layer of the pyramid. Our TLS implementation sits right above EverCrypt, and the careful design of EverCrypt directly benefits and supports the verification efforts taking place in the TLS layer.
Under the EverCrypt hood, we bring together HACL* and Vale-Crypto, both of which are written using domain-specific languages based on F*. HACL* is written in Low* for verified low-level C implementations, while Vale-Crypto is written in Vale for verified assembly implementations. Both are verified for memory safety, correctness, and side-channel resistance. Crucially, Vale and Low* algorithms are shown to implement the same specifications, meaning that the two can be brought together under the EverCrypt provider interface. The two languages can interoperate—mundane, noncritical parts of an algorithm are written once in Low*, leaving more time to write and verify performance-critical code in Vale.
Thanks to the mixture of C and assembly code, the verification effort doesn’t compromise performance. EverCrypt operates on par with, or better than, many existing offerings.
EverCrypt—TLS and beyond
We built EverCrypt for our TLS implementation, but we designed the provider to be useful for a wide range of software beyond TLS, from disk encryption to instant messaging. As of this writing, several other clients use EverCrypt for their cryptographic needs.
As part of the work we’re doing with Project Everest, we have one verified client written in F*: a Merkle tree library usable for blockchains. Outside of Project Everest, clients include the WireGuard VPN; the upcoming Zinc crypto library for the Linux kernel; the MirageOS unikernel; and the Tezos blockchain. Parts of EverCrypt have been used for over a year within Microsoft in support of implementing the QUIC protocol. These clients are usually written in C and are not themselves verified; however, because they use a verified cryptographic provider, they’re reducing their attack surface and improving their security and reliability.
As tools improve and the scope of verification expands, we hope that EverCrypt will not only show that large-scale verified libraries are attainable but also that there now exist viable alternatives to legacy libraries. With EverCrypt, developers no longer have to compromise performance for security, and it is our aspiration that many more software projects start using EverCrypt for greater assurance.
The post EverCrypt cryptographic provider offers developers greater security assurances appeared first on Microsoft Research.