Yale has joined a $10 million computer science initiative that seeks to eliminate one of the major sources of flaws in computer software by applying formal logic to critical software developing tools.
The initiative will pave the way for a world even more reliant on secure computer technology in fields ranging from cryptography to transportation, said Benjamin Pierce, professor of computer science at the University of Pennsylvania and a member of the project. The five-year initiative involves researchers from Princeton, MIT and the University of Pennsylvania, and is funded by the National Science Foundation.
According to Adam Chlipala, a computer science professor at MIT who is involved with the project, said the project, known as DeepSpec, addresses specifications. A part of computer systems, specifications are written instructions for what actions a piece of software is meant to perform, as tools for developers working on other components of a piece of software. These descriptions are generally written in layman terms and can range from relatively brief documents to thousands of pages of instructions.
He added that errors in software development sometime come up when the specifications are imperfect descriptions of a program’s structure and function, leading to improper interrelations among software components.
“Significant correctness problems can result when components A and B connect to each other, but the authors of A and B have made different assumptions about how that interface works,” Chlipala said.
Yale computer science professor Zhong Shao, who is involved in the project, said that a mismatch between the software of a system and its specifications is one of the three primary sources of errors and bugs in computer systems. The other two are hardware and software.
“Bugs in hardware could come from physical material which we cannot completely eliminate; bugs in specifications may always exist because it is written by humans — we cannot always know exactly what a human wants,” Shao said. “Bugs in software, however, refer to the gap between the software and the specifications.”
The team is working to develop a successful link between specifications and software grounded in formal, provable logic, Chlipala explained. This link would ensure that any of the intended functions of a piece of software is true with certainty. Their project, using a method known as deep specification, seeks to prove that the specifications of a piece of software are precisely aligned with the software’s function, eliminating any possibility of error due to lack of clarity.
Chlipala added that this process does not eliminate the possibility that software developers simply chose the wrong specifications — only that the specifications that were chosen are met with certainty.
Pierce said that by putting these specifications in the language of formal logic through deep specification, developers are able to create new functionality for software specifications.
“Specifications have been an integral part of the software development process for decades — what we’re interested in is a class of specifications that is more powerful than many of the specifications that have been used in the past,” Pierce said. “Specifications are software, not in the sense that we run them but in the sense that they require the same thought process and the same methodology as the software that we do run.”
This deep specification process opens up several valuable opportunities for computer scientists in the future. Pierce said a cryptography program created using formal language under deep specification would be confirmed with absolute certainty to fulfill all of its objectives. As a result, the cryptography program would be much harder to crack and would not have an unexpected hole in its security. The certainty provided by deep specification is a step above random testing, a previous software development standard, where the program is tested in thousands or even millions of scenarios, but cannot be confirmed with certainty.
Shao said that this level of certainty provided by deep specification is necessary for the growing ways that society uses computer programs, from banking to self-driving cars. Even the slim possibility of error in these scenarios, he said, is unacceptable.
Shao added that other forms of error are still possible even if a piece of software is worked on using deep specification. If the underlying hardware is flawed or if the proof-based specifications do not cover every attribute of the desired software, then there could be errors in the final product regardless of the form of specification used.
“Deep specification can state that certain kinds of flaws are not present in code, but it is always possible that the specification author forgot to include a particular kind of problem,” Chlipala said. “A program might have a perfectly good proof that it meets one specification, and yet that specification might not have been the right one to choose, because it is too weak.”
Chlipala added that one of the projects within DeepSpec will be to develop ways to mitigate risks in poorly chosen specifications, including more precise forms of wording and improved formatting, organization or specifications.
Yale’s participation in the DeepSpec program will bring expertise in operating systems, Pierce said. Shao is involved in the creation of CertiKOS, an operating system grounded in formal proofs that ensure that certain forms of errors are eliminated. This operating systems expertise, Pierce added, would supplement MIT’s strength in hardware specifications, and Penn’s and Princeton’s focus on code compilers, a tool for converting written code into the material that computers use to function.
Pierce added that this collaborative program has a substantial educational component. The developments will be open source and shared through events on each of the campuses involved in DeepSpec.
The $10 million grant funding this research is part of the National Science Foundation’s Expeditions in Computing program.