Project Everest
Building and deploying provably secure communication software
新闻与深度文章
新闻报道 | 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…
新闻报道 | 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 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…
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…
新闻报道 | 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…
新闻报道 | 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.
新闻报道 | 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…
新闻报道 | 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…
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…