Microsoft has released a new cryptographic provider – an independent software module that performs cryptography algorithms for authentication, encoding, and encryption – and cryptographic library that it describes as capable of guaranteeing with “mathematical certainty” that communications will be secure.
EverCrypt, developed and verified by the “Project Everest” team (a joint Microsoft-academia collaboration) includes a comprehensive suite of algorithms spans block ciphers, elliptic curves, and hash functions based on new language F*.
It was developed to deliver a more robust implementation of TLS, the protocol that underpins secure HTTPS communications across the internet, but has been designed to be useful for a wide range of software, from disk encryption to instant messaging.
EverCrypt is already in use by Mozilla Firefox and the WireGuard VPN; and will be used in the upcoming Zinc crypto library for the Linux kernel; the MirageOS unikernel; and the Tezos blockchain, Microsoft Research’s Jonathan Protzenko, and Bryan Parno, an Associate Professor, Carnegie Mellon University said in a joint post this week
F* Allows it to be Mathematically Verifiable as Secure
It offers the “same features, convenience, and performance as popular existing cryptographic libraries “without the bugs that leave protocols and applications vulnerable” the two said this week, unveiling the project.
EverCrypt is mathematically proven to be free of coding errors, like buffer overruns, that can enable hacking attacks; gets the cryptographic math right every time and is invulnerable to so-called side channel attacks, in which an adversary infers the contents of an encrypted message just by observing how a programme operates (e.g running faster when it adds “0” to a value and slower when it adds “1” to a value).
As Inria’s Karthik Bhargavan told Quanta Magazine’s Kevin Hartnett, the main challenge when creating EverCrypt was developing a single programming platform that had the capacity of a traditional software language like C++ “and the logical syntax and structure of proof-assistant programs like Isabelle and Coq, which mathematicians have been using for years”. The language the Project Everest team developed, F*, aims to deliver this; putting software and mathematical proofs on the same footing.
Content from our partners
As Bhargavan told Hartnett: “We unified these things into a single coherent framework so that the distinction between writing programs and doing proofs is really reduced… You can write software as if you were a software developer, but at same time you can write a proof as if you were a theoretician.”
EverCrypt: A Combination of Projects
Project Everest brings together EverCrypt itself – a multi-platform, self-configuring cryptographic API, as formally unveiled this week – with Project Everest projects HACL*: a verified library of cryptographic primitives written in F*, and Vale: a domain-specific language for verified cryptographic primitives in assembly
The company developed the platform alongside Carnegie Mellon University, INRIA, and the Microsoft Research-INRIA joint center, with its initial primary aim being to develop a fully verified implementation of HTTPS, the software that secures web communication, with TLS as its underlying cryptographic protocol.
The team said in a blog this week: “Delivering an implementation of TLS that guarantees with mathematical certainty your communications will be confidential and protected is a vast and ambitious effort…”
“Such an implementation needs successive verified software layers, beginning with the raw cryptographic algorithms, followed by a cryptographic provider.”
They added: “A crucially important component, the cryptographic provider orchestrates these standalone algorithms into a unified collection to meet the security needs of the protocol… 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?”
To resolve these challenges, a cryptographic library like that which EverCrypt includes, should possess three features, the team said.
- 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” the Project Everest team claimed.
What Project Everest Comprises
Project Everest is the combination of the following projects.
- F*, a verification language for effectful programs
- miTLS, reference implementation of the TLS protocol in F*
- KreMLin, a compiler from a subset of F* to C
- HACL*, a verified library of cryptographic primitives written in F*
- 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.
Combined, in short, these projects generate a mixture of C and assembly code that implements TLS 1.3, with proofs of safety, correctness, security and various forms of side-channel resistance. Ultimately, the team hopes to deliver a stack of software (vulnerabilities in adjacent/overlapping programmes could still undermine the library, so mathematically demonstrable secure interoperability is the focus) that is demonstrated to be mathematically watertight, with the end result; a safer internet.
