Building the tools for bug-free software
Connecting state and local government leaders
With detailed descriptions of how software is expected to behave, researchers believe they can verify its operations and eliminate bugs.
With the complexity created by the massive number of interactions among today’s computer components, misinterpretations and mistakes can creep into software, often as a result of unexpected interactions. So how do you know if a program you’re running is doing what it is supposed to be doing and nothing more?
You don’t. But Andrew Appel, professor of computer science at Princeton University, has received a 5-year, $10 million grant from the National Science Foundation aimed at changing that response.
According to Appel, the inability to verify a program’s behavior opens the door to software bugs and security vulnerabilities. His “Deep Specification” project is creating tools for specifying exactly what programs are intended to do in most every imaginable circumstance and for verifying that they are, in fact, performing as expected.
The first step, Appel said, is requiring programmers to specify in standardized form exactly what operations their code is meant to execute.
“Between two different software components you have interfaces,” Appel said. The code that controls that interaction -- the application program interface, or API -- is written partly in source code and partly in English, with the latter being comments about how the code works. “It is the part that is written down in English that we want to formalize in logic to explain exactly what would happen if you make a call to it.”
Once there are precise descriptions of the behavior of software elements based on formal logic, specifications be written for testing the code. “By formalizing the interfaces in logic, that then allows us to write specifications for proving that some software component does what it is supposed to do and no more,” he said.
“The creative part is coming up with a proof. Checking it is completely mechanical.”
Researchers from the University of Pennsylvania, the Massachusetts Institute of Technology and Yale University are also participating in DeepSpec.
“With DeepSpec, we aim to replace the existing ‘patch and pray’ mentality, where software developers wait for vulnerabilities to be discovered in the wild,” Penn engineering professor Benjamin Pierce told Penn News. “The technology for constructing software that can be mathematically proven to adhere to desired specifications has matured to the point that we can do it for critical systems in the real world.”
The project aims to create specifications “that are both precise, that is, integrated with the code they describe, and live, that is, continuously and automatically checked, and that can express rich descriptions of correct system behaviors,” Pierce said.
Applying Deep Specification to software development, of course, is time consuming.
Given the demands, Appel said, “not all software is worth proving correct.” He said the project is focused on critical infrastructure components, such as operating system kernels, compilers and cryptographic libraries.
So how does Deep Specification impact IT operations? Appel noted that many IT managers run a hypervisor underneath applications to protect them from each other -- so that an exploit that afflicts one won’t be able to bleed over to another. “One of the components of our Deep Spec research is to build a really, really high-assurance hypervisor,” he said. “In the hypervisor of the future, you’d like to really know for sure that there’s not going to be zero-day exploit against one application that …[goes] through the hypervisor to take over another application running in another guest client.”
While the project involves primarily academic researchers, a number of security specialists from the private sector are being looped in. “There are a lot of companies in the last couple of years that of gotten very serious about trying to protect not only their own data but customers’ data from hackers,” Appel said.