The Science of Deep Specification

The next time a software maker tells you to update your favorite computer application immediately to fix serious defects or patch gaping security holes, don't lose faith. Help is on the way.

A team led by Princeton computer scientist Andrew Appel aims to exterminate software "bugs," the maddening but unintended programming errors that can open our lives to hackers and thieves, mess up our cellphones, our cars and the growing list of electronic devices that we rely on in our daily lives, and cause inaccuracies in computers performing critical tasks such as tracking and tabulating election returns.

Funded by a $10 million, five-year grant from the National Science Foundation, Appel and fellow researchers at the University of Pennsylvania, Yale University and the Massachusetts Institute of Technology plan to develop integrated tools to eliminate uncertainty from the complex task of software development. A goal beyond the core research is to reshape the industry itself by erasing the gap between researchers, who have made significant strides in the fight against bugs, and educators who are teaching the next generation of programmers and engineers.

"In our interconnected world, software bugs and security vulnerabilities pose enormous costs and risks," said Appel, the Eugene Higgins Professor of Computer Science. "When you press the accelerator pedal or the brake in a modern car, for instance, you're really just suggesting to some computer program that you want to speed up or slow down. The computer had better get it right."

The researchers' initial challenge will be to dissect the overwhelming complexity of modern hardware and software to uncover the factors that determine how various computer components work together. The next step is to develop "deep specifications" — gritty, precise descriptions of the behavior of software based on formal logic (deductive reasoning, the use of syllogisms and mathematics) — that will enable engineers not only to build bug-free programs but to verify that their programs behave exactly as they should. Hence, the project's official name, Expeditions in Computing: The Science of Deep Specification (DeepSpec, for short).

"The Expeditions in Computing program enables the computing research community to pursue complex problems by supporting large project teams over a longer period of time," said Jim Kurose, NSF’s head for Computer and Information Science and Engineering. "This allows these researchers to pursue bold, ambitious research that moves the needle for not only computer science disciplines, but often many other disciplines as well."

In a way, the DeepSpec project marks a coming of age for an industry in which many practitioners still consider development, especially software writing, as much an art as a science. Software writers often work on isolated tasks, and many don't bother to annotate their coding in ways that would allow others to learn from their thinking. The weak institutional knowledge base has slowed progress toward a solution to the riddle of unintended consequences, especially in complex situations that involve multiple programs working at the same time.

"Even if the engineer who builds one component writes in English 'this is what it does and here is how to use it,' the engineer of another component might interpret the English-language description the wrong way, and their two components won't work properly together," Appel said.

Appel's participation in a French-led project called CompCert helped frame his quest to stamp out bugs. CompCert, based at Inria, the French Institute for Research in Computer Science and Automation near Paris, created a verified software compiler— that is, a program that has been proven to accurately translate programming language into machine instructions that can be executed on a computer chip.

"The logical next step," Appel said, "is to connect verified components—   compilers, operating systems, program analysis tools, processor architectures—so no bugs can creep in because of misunderstandings at component boundaries."

DeepSpec will facilitate this integration by improving the way specifications are written, using formal logic, Appel added. "But to test whether this approach is really an improvement, we need a big consortium with multiple components to connect together. That's the DeepSpec 'expedition.'"

Research Scholar Lennart Beringer, who serves as Appel's associate director for DeepSpec, also stressed the importance of having a consortium of four universities participating in the project.

"CompCert demonstrated that it's indeed possible to develop deep specifications for industry-strength software," said Beringer, who came to Princeton in 2009 and has also collaborated with the CompCert project. "Since then, individual projects at UPenn, Yale, MIT, Princeton and elsewhere have applied this approach to other pieces of software, but their efforts were isolated, so each project developed its own version.

The point of DeepSpec is to bring everybody together in a multi-institutional effort."

In addition to Appel, principal investigators are Benjamin Pierce, Stephanie Weirich, Steve Zdancewic, all professors in UPenn's Department of Computer and Information Science; Adam Chlipala, an associate professor of computer science at MIT; and Zhong Shao, a professor of computer science at Yale who received his Ph.D. from Princeton in 1994.

Each participant brings unique expertise to the project.

"My own work is in tools for reasoning about programs," Appel said. "Steve Zdancewic works on verified compilers, for translating programs to machine language. Adam Chlipala will work on the next lower level, in verified computer chips. Above all those layers, Zhong Shao is building a verified operating system, and Stephanie Weirich is working at the level of programming languages in which people could write application programs. Benjamin Pierce is working on program testing tools that are informed by specifications."

The DeepSpec project is committed to revamping the business of software by promulgating its findings throughout the computer industry. The key will be changing what's taught in colleges and universities.

"I'm very excited about our plans for education," Appel said.  At Yale, Shao is developing an innovative operating systems course informed by deep specifications. Zdancewic at Penn is developing an innovative compilers course informed by deep specs.

"Students in these courses will learn more, with less effort, because the DeepSpec approach allows us to clarify how the pieces fit together," Appel said. "I'm looking forward to test-driving this new curriculum at Princeton, to evaluate how much of a difference it makes. At the same time it will freshen our computer science curriculum in those subjects at Princeton."

Beringer added that the DeepSpec team is inviting researchers and practitioners from elsewhere to become involved. "All our specifications will be open source, and we'll run events to educate people on how to develop, evaluate, and maintain them."

DeepSpec plans to train the next generation of researchers by hosting a two- or three-day scientific workshop in each of the five years of the NSF grant and a summer school for researchers during the second year.

The group's website, deepspec.org, gives an overview of the project's research and education plans:  the individual projects at Princeton, Penn, MIT, and Yale, and the means of connecting them via deep specifications.  It also lists opportunities for prospective students and postdocs, and opportunities for long-term visits to Princeton and the other universities by collaborators from academia and industry.

-- Doug Hulette