Project Everest, an ongoing collaboration started in 2016 with researchers from Microsoft, Inria, Carnegie Mellon University, and The University of Edinburgh, is working on a verified, secure communication stack designed to improve the security of HTTPS, and has already made available their work
on GitHub.

Project Everest is building software guarantees, for example, that a message you sent to your bank over the internet is safe from tampering and readable only by your financial institution. Project Everest is building software that provides such a guarantee as a theorem about the code that implements a secure communication protocol deployed in web browsers and servers everywhere.

“Proving theorems about programs has been a dream of computer science for the last 60 years or more, and we’re finally able to do this at the scale required for an important, widely deployed security-critical piece of software,” says Microsoft Senior Researcher Nik Swamy, a member of the Project Everest team.

The security of internet communications depends on a variety of cryptographic algorithms and protocols. The most widely used among these falls under the umbrella of the Transport Layer Security (TLS) protocol. TLS is used for secure web browsing via HTTPS, email, Voice over IP, instant messaging, and many other kinds of communication. Unfortunately, TLS and its many implementations have been attacked repeatedly over its 25-year history.

Growing out of several prior Microsoft Research projects, including Ironclad, miTLS, and F*, Project Everest aims to develop and deploy efficient, verified, open-source implementations of the entire TLS stack and related protocols, formally reducing the security of the code to the assumptions about the hardness of certain cryptographic problems.

Accoding to Jonathan Protzenko, a Microsoft researcher on the Everest team, “Everest makes for a tight interaction between industrial and academic research.”.

Project Everest is halfway through its projected five-year arc, and its verified components are beginning to replace the current infrastructure with proven, secure software. For instance, Everest’s HACL* library provides verified cryptographic primitives for Mozilla Firefox, for the WireGuard VPN, and for the Tezos blockchain. And within Microsoft, Everest’s miTLS protocol stack powers the primary implementation of the QUIC transport protocol. The Everest team expects to announce further deployments in the coming weeks. Meanwhile, Everest code is already open source and is developed publicly on GitHub.

Formal Verification of Software

Formal verification involves using software tools, including various kinds of theorem provers and proof assistants, to analyze all possible behaviors of a program and prove mathematically they comply with the code’s specification, a machine-readable description of the developer’s intentions. Once the code has been verified against its specification mechanically, based on trust in the software used to check proofs, a skeptical auditor need only study the specifications and the theorem statements proven without needing to consult the much larger programs and proofs.

“Most software built today gets tested before it is released—at least one hopes it does!” says Swamy. “But even the most rigorous testing can only find bugs; it cannot rule out the existence of errors. For certain kinds of software, say security-critical code like TLS, one may actually want to prove that no vulnerabilities exist. Software verification is time-consuming and requires expertise, but, unlike testing, it can actually guarantee mathematically the absence of entire classes of errors.”

For Everest programs, the team’s specifications cover a range of properties, including:

• Memory safety: A program never violates the memory abstractions, and, as a consequence, is free from common bugs and vulnerabilities like buffer overflows, null-pointer dereferences, use-after-frees, and double-frees.
• Type safety: A program respects the interfaces among its components, including any abstraction boundaries. For example, one component never passes the wrong kind of parameters to another or accesses its private state.
• Functional correctness: A program’s input/output behavior is fully characterized by a simpler mathematical function, which acts as its functional specification.
• Side-channel resistance: Observations about the implementation’s low-level behavior, such as the time it takes to execute or the memory addresses it accesses, are independent of the secrets manipulated by the program. Hence, an adversary monitoring these “side-channels” learns nothing about the secrets.
• Cryptographic security: Based on cryptographic assumptions, except for negligible probability, Everest programs are indistinguishable from ideal cryptographic functionalities, the mathematical definitions that cryptographers use to capture the notion of secrecy, integrity, and secure communication.

Formal verification can play a role throughout the software development process, from design to implementations and deployments. The value of verification is increasingly widely perceived, especially for security-critical code.

“Cryptographic protocols are notoriously hard to implement correctly, with errors in both the algorithms and the protocol implementation itself being common,” says Eric Rescorla, chief technology officer of Mozilla Firefox, security area director at the Internet Engineering Task Force, and the editor of the TLS standard. “Formal verification tools like those developed by the Project Everest team have transformed the way we design these protocols, allowing us to move faster while having much higher confidence in protocol correctness.”

Benjamin Beurdouche, Karthik Bhargavan, Antoine Delignat-Lavaud, and Cédric Fournet, all members of Project Everest, have contributed features and fixes to the TLS standard. Beyond assisting with designs and specifications, verified implementations are also increasingly attractive for mainstream deployment.

All Everest code is programmed and verified using F*, a framework that brings together three strands of research in programming languages.

• F* is an effectful, general-purpose higher-order programming language in the tradition of languages like F#, OCaml, and Haskell, among others.
• F* includes a full-fledged dependent type theory and tactic framework in the tradition of proof assistants like Coq and Nuprl, allowing nearly arbitrary expressive power for conducting formal mathematical proofs.
• Like other program verifiers, including Dafny and Why3, F* is integrated with an automated theorem prover, Z3, which can automate many of the tedious, low-level proof steps necessary to prove programs correct.

For various cryptographic primitives, peak performance can only be obtained by going still lower level and programming in assembly language, often taking advantage of specialized hardware instructions, such as Intel AES-NI. Vale stands for “Verified Assembly Language for Everest” and provides a domain-specific language for writing and verifying assembly programs targeting different platforms, like Windows, MacOS, and Linux, and architectures, like x86, x64, and ARM. It also supports multiple verification systems for carrying out proofs, including F* and Dafny.

In addition to the availability of Everest components on GitHub, the Project Everest team is planning the first integrated release of Everest’s verified stack, its libraries, and its verification tools for early summer 2019.

For instance, the Everest team is also working on verifying implementations of post-quantum cryptography and proving the security of key components used in high-assurance enterprise blockchains.