With computer security, it sometimes seems like the good guys are always playing catch up. No sooner have programmers patched one vulnerability then hackers exploit another.
A large part of the problem is the complexity of modern software. Most programs we use contain so many lines of code that it’s nearly impossible to thoroughly check all the code and certify it free of bugs. This leads to situations like the Heartbleed bug, discovered in 2014, which was created by a coding error and threatened to undermine online security.
“It’s really hard for people to pay complete attention to every detail in someone else’s code. It’s just not interesting enough,” says Adam Chlipala, a computer scientist at MIT.
Soon, however, we may not need to rely on human attention at all. Chlipala is part of a newly launched project called DeepSpec that intends to change the way we conceive of computer security. Rather than depend on people to check for bugs, DeepSpec plans to demonstrate that it’s possible to write software in such a way that it can be proven to be invulnerable to certain kinds of attacks.
And by proven, they really mean 100 percent secure. A proof is a formal argument that demonstrates that given some starting assumptions, certain conclusions follow inexorably. Proofs crop up most often in mathematics. There’s a way to prove, for instance, that the square root of two is an irrational number. That proof doesn’t just say we think the square root of two is an irrational number or that we have very good evidence that it’s an irrational number. It says that according to the axioms of mathematics, it has to be an irrational number.
Computer programs are amenable to the same kinds of absolutes. If code is written in the correct formal style and checked properly, it’s possible to send software out into the world with complete certainty that it can only be used to do a specific set of pre-approved tasks. This guarantee is built on the idea of “deep specification,” which gives the project its name.
“When you give a formal specification of what software is supposed to do and prove the software correctly implements that specification, then you’re sure that the attacker can’t get to you by working outside the model,” says Andrew Appel, a computer scientist at Princeton University and the DeepSpec project leader.
The concept of program verification has been around for a while. But it’s only recently that technology has made deep specification possible. The main advance has been the development of proof assistant programs, like a program called Coq, which check proofs, identifies holes, and pronounces with complete certainty that a proof works.
“These are proofs in logic using rules of inference that the Ancient Greeks almost would have recognized,” says Appel. “Since software systems are big things, the things you want to prove about them are big. Since the proofs are big, you want to have a computer check them and make sure every step in the proof is correct.”
DeepSpec is advised by representatives from a number of major technology companies, including Microsoft, Facebook, and Google. The project intends to create a demonstration system, like an Internet server, that shows the computer industry it’s possible to build products with this deep level of security. To do this, they’ll have to prove the security of each piece of the system—the computer chips, the operating system, the software that runs on the operating system — and then prove the security of the end-product produced when all these pieces are plugged together.
“We want to demonstrate to industry that these techniques have come of age and are usable in production,” Appel says.
A longer-term goal of the project is to change the way programmers write code. In order to be checked in proof assistants like Coq, code needs to be written in a specific formal style. DeepSpec is creating educational materials that can be used to teach computer science students to code this way and Appel is already teaching these methods in some of his courses at Princeton.
Even if deep specification were to be widely adopted, it would not mean the end of our computer security woes. Hackers would still be able to launch social engineering attacks, in which, for example, unsuspecting users are tricked into opening infected attachments. Deep specification provides guarantees about what a program can and cannot be used to do — but it’s much harder to prove that those intended purposes can only ever be used in desired ways.
“You can’t be sure there’s not some clever way to work inside the model and combine the operations software is supposed to do as a possible attack. You can only say here are the operations the software is designed to support,” says Appel.Kevin Hartnett is a writer in South Carolina. He can be reached at firstname.lastname@example.org.