Cryptography That Is Provably Secure

Programmers are human, but mathematics is immortal. By making programming more mathematical, a community of computer scientists is hoping to eliminate the coding bugs that can open doors to hackers, spill digital secrets and generally plague modern society.

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 coding errors often manifest only in extreme “corner cases” — a perfect storm of unlikely events that reveals a critical vulnerability. Many of the most damaging hacking attacks in recent years have exploited just such corner cases.

“It’s some cascading failure, and it’s hard to systematically find because [the events leading to it] are individually all very unlikely,” said Bryan Parno, a computer scientist at Carnegie Mellon University who worked on EverCrypt.

By contrast, Parno and his colleagues have specified exactly what their code is supposed to do and then proved it does that and only that, ruling out the possibility that the code could deviate in unexpected ways under unusual circumstances. The general strategy is called “formal verification.”

“You can reduce the question of how code behaves into a mathematical formula, and then you can check if the formula holds. If it does, you know your code has that property,” said Parno.

Because it’s practically impossible to formally specify the function of complex software such as a web browser, researchers have instead focused on programs that are both critical and amenable to being defined mathematically. EverCrypt is a library of software that handles cryptography, or the encoding and decoding of private information. These cryptographic libraries are innately mathematical. They involve arithmetic with prime numbers and operations on canonical geometric objects like elliptic curves. Defining what cryptographic libraries do in formal terms is not a stretch.

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.”

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 platform needed the capacity of a traditional software language like C++ and the logical syntax and structure of proof-assistant programs like Isabelle and Coq, which mathematicians have been using for years. No such all-in-one platform existed when the researchers started work on EverCrypt, so they developed one — a programming language called F*.  It put the math and the software on equal footing.

“We unified these things into a single coherent framework so that the distinction between writing programs and doing proofs is really reduced,” said Bhargavan. “You can write software as if you were a software developer, but at same time you can write a proof as if you were a theoretician.”

Their new cryptographic library provides a number of security guarantees. 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. They also proved that EverCrypt gets the cryptographic math right every time — it never performs the wrong computation.

But the most striking guarantee EverCrypt makes has to do with an entirely different class of security weaknesses. These occur when a bad actor infers the contents of an encrypted message just by observing how a program operates.

For example, an observer might know that an encryption algorithm runs just a little faster when it adds “0” to a value and just a little slower when it adds “1” to a value. By measuring the amount of time an algorithm takes to encrypt a message, an observer could start to figure out whether the binary representation of a message has more 0s or 1s in it — and eventually infer the complete message. “Somewhere deep in your algorithm or the way you implement your algorithm you are leaking information, which can completely defeat the purpose of the entire encryption,” said Bhargavan. Such “side-channel attacks” were behind several of the most notorious hacking attacks in recent years, including the Lucky Thirteen attack. The researchers proved that EverCrypt never leaks information in ways that can be exploited by these types of timing attacks.

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.

In addition, even a verified cryptographic library has to work in concert with a host of other software, like an operating system and many common desktop applications, that are typically unverified, and likely will be for the foreseeable future. “We’re not targeting something as complex as a word processor or a Skype client,” said Protzenko, because it’s not obvious how you’d capture in a formal language what they’re supposed to do. “It’s hard to think about the intended behavior of those things.”

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 overarching goal of the initiative is to complete a fully verified implementation of Hypertext Transfer Protocol Secure (HTTPS), the software that secures most web communication. This will involve half a dozen individual software elements like EverCrypt, each of which is formally verified to work on its own and all of which are formally verified to work together.

“Project Everest is trying to build out a larger stack of software that’s all been verified and verified to work together. Over time we’re hoping the frontier [of verified software] will continue to grow,” said Parno.

This article was reprinted in Spanish at Investigacionyciencia.es.