#hacker-proof

(...) Work on EverCrypt began in 2016 as a part of Project Everest, an initiative led by Microsoft Research. At the time — and still today — cryptographic libraries were a weak point in many software applications. They were slow to run, which dragged down the overall performance of the applications they were a part of, and full of bugs. “I think there’s been some realization from app developers that there’s a disaster waiting to happen,” said Jonathan Protzenko, a computer scientist at Microsoft Research who worked on EverCrypt. “The software world is ripe for something new that does provide [EverCrypt’s] guarantees.”

Now a set of computer scientists has taken a major step toward this goal with the release today of EverCrypt, a set of digital cryptography tools. The researchers were able to prove — in the sense that you can prove the Pythagorean theorem — that their approach to online security is completely invulnerable to the main types of hacking attacks that have felled other programs in the past. “When we say proof, we mean we prove that our code can’t suffer these kinds of attacks,” said Karthik Bhargavan, a computer scientist at Inria in Paris who worked on EverCrypt.

EverCrypt was not written the way most code is written. Ordinarily, a team of programmers creates software that they hope will satisfy certain objectives. Once they finish, they test the code. If it accomplishes the objectives without showing any unwanted behavior, the programmers conclude that the software does what it’s supposed to do.

(...) Yet while EverCrypt is provably immune to many types of attacks, it does not herald an era of perfectly secure software. Protzenko noted there will always be attacks that no one has thought of before. EverCrypt can’t be proven secure against those, if only for the simple reason that no one knows what they will be.