Project Everest

Building and deploying provably secure communication software

新闻与深度文章

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.”
微软研究院博客

| Tahina Ramananandro, Aseem Rastogi, 和 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;…

新闻报道 | 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…

新闻报道 | 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,…

新闻报道 | 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
微软研究院博客

| 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…

新闻报道 | 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.

微软研究院博客

| Jonathan Protzenko 和 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…

新闻报道 | Quanta Magazine

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

新闻报道 | 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…