Project Everest
Building and deploying provably secure communication software
News & features
In the news | CyLab
Building a verifiably-secure internet
In security, almost nothing is guaranteed. It’s impossible to test the infinite ways a criminal hacker may penetrate a proverbial firewall. But what if, by the laws of mathematics, something could be proven to be secure without running an infinite…
In the news | Jonathan Protzenko Blog
Generating C code that people actually want to use
Project Everest is a large, collaborative research effort that aims to verify and deploy a new, secure HTTPS stack. All of our code is verified using the F* programming language. Using KreMLin, a dedicated compiler, the verified F* code is…
Project Everest: Reaching greater heights in internet communication security
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 verification tools and techniques the Everest team is using and…
Scaling the Everest of software security with Dr. Jonathan Protzenko
Episode 58, January 9, 2019 – Dr. Protzenko talks about what’s wrong with software (and why it’s vitally important to get it right), explains why there are so many programming languages (and tells us about a few he’s been working…
In the news | LWN.net
Zinc: a new kernel cryptography API
We looked at the WireGuard virtual private network (VPN) back in August and noted that it is built on top of a new cryptographic API being developed for the kernel, which is called Zinc. There has been some controversy about…
In the news | reddit r/tezos
Tezos Switches Cryptographic Libraries from TWEETNACL to HACL!
We just saw a result from INRIA (Institution which developed Ocaml and partners with Tezos ) audit. The Tezos Devs changed the library from TWEETNACL to HACL which is developed by INRIA itself.
In the news | Franzis Kuskiefer Blog
Shipping (some) HACL*
In this second blog post I describe the process of integrating code from HACL*, a researchy crypto library, into NSS, a production library shipping to millions of people, running on a plethora of platforms. In short, how to ship (some…
In the news | Franzis Kuskiefer Blog
The HACL* approach
HACL* (High-Assurance Cryptographic Library) is a formally verified cryptographic library in F*, developed by the Prosecco team at INRIA Paris in collaboration with Microsoft Research, as part of Project Everest. HACL* was inspired by discussions at the HACS workshop and…
How Programming Languages Quietly Run the World with Dr. Ben Zorn
In an era of AI breakthroughs and other exciting advances in computer science, Dr. Ben Zorn would like to remind us that behind every great technical revolution is… a programming language. As a Principal Researcher and the Co-director of RiSE…