Funded by a $10 million, five-year grant from the National Science Foundation, a team of researchers from Yale, Princeton, MIT, and the University of Pennsylvania aim to exterminate software bugs that can lead to security vulnerabilities and computing errors that disrupt devices and open our lives to hackers and thieves.
As part of the project, known as Expeditions in Computing: The Science of Deep Specification (DeepSpec), the researchers will develop integrated tools to eliminate uncertainty from the complex task of software development. That involves creating “deep specifications” — precise descriptions of the behavior of software based on formal logic (computer-assisted deductive reasoning, the use of syllogisms, mathematics, and machine-checkable proofs) — to enable engineers to build bug-free programs and verify that their programs behave exactly as designed.
Zhong Shao, a Yale professor of computer science, said the project is designed to correct decades of flawed software-developing practices. Software writing has long been treated as much as an art as a science, he said, and developers weren’t as rigorous as they could be in programming.
“I think at an earlier time, security and reliability were not considered to be as important,” he said. “Initially, computers were not used for critical applications.”
Today, however, eliminating bugs is crucial if robots, driverless cars, and the Internet of Things are to become part of everyday life.
Shao and his team have spent years working on developing certified software — that is, programs that have been proven capable of doing what they’re meant to do. They built CertiKOS, a verified operating system that uses deep specifications and plays a major role in the project. Shao said it proves wrong the long-held notion that it’s impossible to completely eliminate software bugs.
“We really can do much better than we’re doing now,” he said. “We can rule out these software-related bugs.”
Other collaborators in the project have developed their own software programs using deep specifications. Part of the DeepSpec project is connecting these verified components (compilers, operating systems, program analysis tools, and processor architectures) so that bugs can’t creep in due to misunderstandings at component boundaries.
For instance, said Princeton computer science professor Andrew Appel, if the engineer who builds one component writes a description in English of the component’s purpose and instructions for its use, another engineer could misinterpret the description. Then, the two components won’t work together properly.
“DeepSpec will address these issues by improving the way specifications are written, using formal logic,” Appel said.
In addition to Shao and Appel, principal investigators are Benjamin Pierce, Stephanie Weirich, Steve Zdancewic, all professors in UPenn’s Department of Computer and Information Science; and Adam Chlipala, an associate professor of computer science at MIT.
Another major part of the DeepSpec project involves getting its findings out to educators and the computer industry. The collaborators are developing a curriculum designed to change how software development is taught. At Yale, Shao said, this includes developing a new operating systems course based on the CertiKOS system.
Additionally, the researchers will make their specifications open source and will organize events to educate people on how to develop, evaluate, and maintain them.
The grant is one of three announced by the NSF. All of them are part of the NSF’s Expeditions in Computing program, designed to enable the computing research community to pursue complex problems. “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,” said Jim Kurose, NSF assistant director for computer and information science and engineering.
(Image via Shutterstock)