Mike's Notes
- Follow up on Project Everest (Microsoft Research)
- Look for ongoing test results
Resources
References
Repository
-
Home > Ajabbi Research > Library > Subscriptions > Quanta
-
Home > Handbook >
Last Updated
11/05/2025
Cryptography That Can’t Be Hacked
By: Kevin Harnett
Quanta Magazine: 02/04/2019
Researchers have just released hacker-proof cryptographic code - programs with
the same level of invincibility as a mathematical proof.
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.
PHOTO: Karthik Bhargavan
Karthik Bhargavan, a computer scientist at Inria in Paris, has collaborated on
an approach to online security that is provably invulnerable to most types of
hacking attacks.
Courtesy of Karthik Bhargavan
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.”
PHOTO: Bryan Parno
Bryan Parno, a computer scientist at Carnegie Mellon University, uses
techniques from mathematics to prove that programs don’t have bugs.
Lauren Demby / Lauren Renee Photography
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."
