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 including associate professor Adam Chlipala of MIT's Computer Science and Artificial Intelligence Laboratory (CSAIL) aims to exterminate software “bugs,” the maddening but unintended programming errors that can open our lives to hackers and thieves, wreck 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 that's part of a new $30 million intitiative from the National Science Foundation (NSF), Chlipala and fellow principal investigators at Princeton, UPenn and Yale 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.
“The development of computer systems has benefited tremendously from advances in ways of dividing large systems into smaller parts, comprehensibly, with effective ways of reasoning about how the pieces fit back together,” says Chlipala. “I believe that formal mathematical proofs will be the glue that supports the next generation of increasingly effective system decomposition techniques, lowering the costs of implementing new functionality, to the point where systems that seem impossibly difficult to build today can be constructed routinely.”
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 so-called 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).
DeepSpec
"This 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 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.
“I'm betting that deep specifications and proofs will come to fill the kind of role that data abstraction and static type systems fill today,” says Chlipala, who received an NSF CAREER Award in 2012 for related work.
Chlipala and professor Arvind will work on Kami, a system for proving the correctness of hardware designs written in a language called Bluespec.
“Within DeepSpec, we plan to verify hardware implementations that run the software code being verified in other parts of the larger project,” says Chlipala.
Other projects of Chlipala’s aim to support what he calls an “even further-out” style of programming: starting from a deep specification and having a tool build the associated program automatically, with a proof that it will run correctly on the actual hardware.
Read more