In our interconnected world, software bugs and security vulnerabilities pose enormous costs and risks. The Deep Specification project addresses this problem by showing how to build software that does what it is supposed to do, no less and (just as important) no more: No unintended backdoors that allow hackers in, no bugs that crash your app, or your computer, or your car. “What the software is supposed to do” is called its specification.
The DeepSpec consortium develops new science, technology, and tools–for specifying what programs should do, for building programs that conform to those specifications, and for verifying that programs do behave exactly as specified. We focus on core software-systems infrastructure such as operating systems, programming-language compilers, and computer chips; with applications such as elections and voting systems, cars, and smartphones.
Experience has shown that it is extremely challenging to write good specifications for software. A maximally useful interface specification must be simultaneously:
- rich (describing complex component behaviors in detail)
- two-sided (connected to both implementations and clients)
- formal (written in a mathematical notation with clear semantics to support tools such as type checkers, analysis and testing tools, automated or machine-assisted provers, and advanced IDEs)
- live (connected via machine-checkable proofs to the implementation and client code).
We call specifications with all of these properties deep specifications. Our research is described here.
Faculty
Students and Postdocs
- Antal Spector-Zabusky
- Antoine Voizard
- Christine Rizkallah (postdoc)
- Joachim Breitner (postdoc)
- Leonidas Lampropoulos
- Li-Yao Xia
- Yao Li
- Yishuai Li
Collaborators
The participating universities funded by this grant are Princeton University, the University of Pennsylvania, Yale University, and the Massachusetts Institute of Technology.
Funding
The Science of Deep Specification is funded by the National Science Foundation as an Expedition in Computing.
