Most students agree that Sparknotes will not give them perfect understanding of a book. Sure, it will work for major plot points, but not for the little details. A similar phenomenon occurs in the realm of computer science. Up until now, programmers and users alike have understood software on the basis of vague, inexact summaries of its functionality. This is where “bugs” come from; when software doesn’t work the way programmers expect, things can go wrong, diminishing the user experience.
As software becomes increasingly integrated into important parts of our lives—smart phones, cars, houses—bugs become more than just an inconvenience. They can be a serious security and safety issue. Software is expected to have inevitable bugs, and every user service agreement admits as much. A team of researchers—including faculty from Yale—seeks to reverse this expectation and create systems that make bug-free code a reality.
The researchers, known collectively as the DeepSpec team, are trying to develop robust systems to support ‘verified’ code. Verified, or certified, code comes with a specification program written in a specialized programming language, instead of inexact English. This high-level language assures developers of the precise functionality of a program at every stage of development.
The program is accompanied by mathematical proofs, which test its functions with logic statements; this way, the code is not just certified by more code, but by in-depth logic, which is either true or false for each test case. Verified code comes with a “proof checker,” so users do not need to validate the math. This system provides programmers and users with a promise that the code will work exactly the way they expect in every case. These promises bind the code to lasting perfection; unless developers require major changes in functionality, certified code should not require any updates.
Unless every aspect of the computer is verified, security flaws and bugs are still a possibility. To this end, Yale University professor of computer science Zhong Shao is working to develop certified operating systems that can run certified software programs. Other team members at Princeton University, University of Pennsylvania, and the Massachusetts Institute of Technology are developing certified compilers (which translate code into machine language), hardware verification (methods of confirming machine-language accuracy), and proof builders.
The DeepSpec team aims to connect the various systems that support verified software, so that there are no gaps at the seams. This corrects a major issue with current systems. “Loosely connected components do not adhere to the specification too well and do not always function together correctly, which leads to security problems,” Shao said.
Though Shao’s operating system is still in development, it holds great promise. Known as CertiKOS, the operating system is a simplified, more elegant version of mainstream operating system kernels like Linux. Instead of the “mess of wires” that constitute the source code of most operating systems, CertiKOS is more methodically organized.
Shao practices ‘correct by construction’ methodology, planning the complicated program as a well-organized stack of horizontal and vertical abstraction layers. This way, instead of a web of code—a mess of connections between different sections—there is a clear chain of command. Shao claims that this method makes it much easier to control the organization of his application interfaces. He hopes to release the operating system for public use in the near future. And with the DeepSpec team and its funding, that could be a possibility.
The DeepSpec team has received a $10 million grant from the National Science Foundation to fund its research over the course of five years. With funds from the grant, the researchers will also participate in outreach and education programs to ensure that the next generation of computer scientists learns good practices. They organize an Industry Advisory Board to inform corporations on the latest advances in computer science, and are integrating these new topics into their curricula.
Here at Yale, Professor Shao has completely restructured the historically difficult Operating Systems elective course to center on the layered, design-first approach of CertiKOS. The course has had very positive results. In the class, Professor Shao tries to show students the importance of structuring; complex software programs can be written with less difficulty when they are carefully planned. “Now [students] can build an operating system in class in one semester without becoming a monk,” he said.
Shao said he has been excited about certified bug-free software for over twenty years; however, only recently has he seen the topic’s popularity skyrocket. “Computers are faster, software is more mature, and security concerns are more pressing,” he said. As this research becomes more relevant, we could see a complete cultural shift, where bugs are no longer a necessary evil, but a sign of non-robust development. “Programmers should be held accountable for writing correct software,” Shao said. And with research like DeepSpec, they can be.