A team of researchers is looking to put an end to the industry’s longstanding software security problem. As part of a five-year, US$10 million grant from the National Science Foundation (NSF), computer scientists from MIT, Princeton, the University of Pennsylvania and Yale are coming together to develop integrated tools that exterminate software bugs.
“In our interconnected world, software bugs and security vulnerabilities pose enormous costs and risks,” said Andrew Appel, computer science professor at Princeton University. “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.”
(Related: MIT researchers developer automatic bug-cleaning software)
The project, known as Expeditions in Computing: The Science of Deep Specification (DeepSpec), will look into correcting decades of flawed software-development practices, and create deep specifications—precise descriptions of the behavior of software elements based on formal logic—that will enable engineers to use mathematically-based techniques to develop bug-free programs, and to verify that their programs behave exactly as intended.
“Today’s critical software systems are neither secure nor reliable. Existing programming tools and languages do not provide good support for writing certified software,” said Zhong Shao, computer science professor at Yale. “With the proliferation of new robots, the Internet of Things and cloud computers, computer software is only going to become even more complex. To control such complexity, we have to develop new technologies and tools that turn software development into a more principled and rigorous practice.”
According to Shao, the researchers have already been working on developing better programming languages and formal methods to help secure software for years, and the DeepSpec project is a natural extension of those projects. For instance, Yale researchers have developed CertiKOS, a certified kernel for secure cloud computing that uses deep specification. And at Princeton, researchers worked on a project called CompCert to create a verified software compiler that can accurately translate a programming language into machine instructions.
“CompCert demonstrated that it’s indeed possible to develop deep specifications for industry-strength software,” said Lennart Beringer, associate director for DeepSpec. “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 the researchers assigned to the project, the team is inviting other researchers and practitioners 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,” said Beringer.
The grant is part of a larger NSF investment to expand the frontiers of computing. The NSF announced $30 million in funding to three Expeditions in Computing projects. The projects include the Science of Deep Specification; Evolvable Living Computing, for understanding and quantifying synthetic biological systems’ applicability, performance and limits; and Computational Sustainability, an effort to balance environmental, economic and societal needs to support sustainable development and a sustainable future.
“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, head of computer and information science and engineering at the NSF. “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.”
