Achieving provably-secure encryption

With every text message we send, every email, every item we purchase online, we blindly rely on the process of encryption, the scrambling of data that protects it from unwanted eyes.

But encryption is hard to get right.

“Right now, encryption’s ability to protect our data is only as strong as the testing its endured,” says CyLab’s Bryan Parno, an associate professor of Computer Science and Electrical and Computer Engineering. “If the encryption implementation has a bug, then a clever adversary can see credit card information, bank details, emails—whatever you might consider private.”

With EverCrypt, we can rule out entire classes of vulnerabilities

Bryan Parno, Associate Professor, Computer Science and Electrical and Computer Engineering

For years, researchers have been working toward a holy grail of cybersecurity: developing code that is verifiably secure and hence requiring no penetration testing. This verifiably secure code would be mathematically-proven to be invincible against certain types of cyberattacks.

Earlier this week, a team consisting of researchers from Microsoft Research, Inria, and CyLab (Parno and his Ph.D. student Aymeric Fromherz) released the world's first verifiably secure industrial-strength cryptographic library—a set of code that can be used to protect data and is guaranteed to protect against the most popular classes of cyberattacks.

The library, titled “EverCrypt,” is available for download on Github.

“With EverCrypt, we can rule out entire classes of vulnerabilities,” says Parno. “We rule out memory safety vulnerabilities, correctness flaws, and we prove the implementations are resistant to some of the most popular types of side channel attacks.”

Side channel" attacks occur when an adversary is able to infer the secret key—a string of numbers that unlocks or decrypts encrypted data—simply by observing how an encrypted server responds to queries. For example, if the key is even, the server may respond faster than if the key is odd.

The encryption process takes time, of course, but Parno assures us that EverCrypt respects that.

“Weve worked really hard on making sure EverCrypt’s performance is at least as good as modern unverified cryptographic libraries,” Parno says. “If your crypto is slow, anything you want to do securely will also be slow. EverCrypt isn’t slow.”

Pieces of the EverCrypt code set are already being used by Firefox, Microsoft, the Tezos blockchain, and the Linux Virtual Private Network, Wireguard. Parno and the rest of the EverCrypt team hope that other developers will download their library and start test-driving it on their platforms.

EverCrypt is a part of Project Everest, a research initiative aimed at creating verifiably secure implementations of the HTTPS ecosystem, the foundation of secure Internet communications.