Project Everest

Building and deploying provably secure communication software

News & features

An animation showing an example of a high-level language message format specified by EverParse. From the message, two arrows labeled “EverParse” point to a rectangle labeled “formal specification” and a rectangle labeled “low-level implementation,” respectively, inside a larger rectangle labeled “F* code.” The figure represents EverParse’s ability to automatically generate safe, correct, and fast F* parsing code. “Correctness” is defined as “Correctness: ​parse (serialize msg) = msg​” and “valid msg ==> serialize (parse msg) = msg​.” The F* logo appears with the description that F* is a type theory–based programming language and proof assistant that can prove theorems about programs​. From the “F* code” rectangle, arrows point from the “low-level implementation” rectangle and a rectangle labeled “verified libraries for combinators” to a rectangle labeled “Safe high-performance C code.”
Microsoft Research Blog

| Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy

EverParse is a framework for generating provably secure parsers and formatters used to improve the security of critical code bases at Microsoft. EverParse is developed as part of Project Everest, a collaboration between Microsoft Research labs in Redmond, Washington; India;…

In the news | Inria blog

After Etalab helped them to get things off the ground back in 2016, and through close collaboration with the Direction Générale des Finances Publiques (the French public finance department), three researchers, among them Denis Merigoux (from Inria Paris), were given…

In the news | Mozilla Security Blog

Cryptographic primitives, while extremely complex and difficult to implement, audit, and validate, are critical for security on the web. To ensure that NSS (Network Security Services, the cryptography library behind Firefox) abides by Mozilla’s principle of user security being fundamental,…

In the news | Horizon: the EU Research & Innovation Magazine

Whenever you see a little padlock in the address bar of your internet browser, as well as when you use apps, email and messaging, you’re relying on something called ‘transport layer security’ or TLS. It’s a protocol that keeps us…

a view of a snow covered mountain
Microsoft Research Blog

| Nikhil Swamy

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 proving methodology and verification tools of Project Everest—is the third in…

In the news | Computer Business Review

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.

Microsoft Research Blog

| Jonathan Protzenko and Bryan Parno

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…

In the news | Quanta Magazine

Researchers have just released cryptographic code with the same level of invincibility as a mathematical proof.

In the news | Jonathan Protzenko Blog

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…