Summary of “How the EverCrypt Library Creates Hacker-Proof Cryptography”

“It’s some cascading failure, and it’s hard to systematically find because are individually all very unlikely,” said Bryan Parno, a computer scientist at Carnegie Mellon University who worked on EverCrypt.
EverCrypt is a library of software that handles cryptography, or the encoding and decoding of private information.
Work on EverCrypt began in 2016 as a part of Project Everest, an initiative led by Microsoft Research.
The main challenge to creating EverCrypt was developing a single programming platform that could express all the different attributes the researchers wanted in a verified cryptographic library.
The researchers proved that EverCrypt is free of coding errors, like buffer overruns, that can enable hacking attacks – in effect, provably ruling out susceptibility to all possible corner cases.
The researchers proved that EverCrypt never leaks information in ways that can be exploited by these types of timing attacks.
While EverCrypt is provably immune to many types of attacks, it does not herald an era of perfectly secure software.
Because vulnerabilities in adjacent, unverified programs can undermine a cryptographic library, Project Everest aims to surround EverCrypt with as much verified software as it can.

The orginal article.