Kathryn O'Neill | MIT EECS
Class teaches students how to apply new verification technologies to systems software.
Might it be possible one day to build software that is provably free of defects? Last spring 14 MIT students gathered to pursue this “holy grail” of computer science in a Department of Electrical Engineering and Computer Science (EECS) seminar class called 6.888 (Certified Systems Software).
The class centered on code verification, a programming technique used to mathematically ensure that a system is error-free.
“I think verification has turned a corner. In the next five to ten years, we will see more verified system software. But, it will require a lot more research,” said M. Frans Kaashoek, the Charles Piper professor of EECS and one of two instructors for the course. “Over the last three to four decades, there has been tremendous progress in building new tools to state and to prove the properties of real systems. One reason we taught the class was to try to use the new technologies and apply them to systems software.”
Bringing students up to speed on verification programming languages and theory was the first challenge. “To get to the point where we can verify something interesting requires quite a bit of background. It requires you take one tool and master it,” Kaashoek said, noting that he and his fellow instructor—Associate Professor Nickolai Zeldovich—offered a weeklong intensive class on the theorem-proving tool Coq during the Institute’s Independent Activities Period in January to help students prepare for 6.888.
Then, during the spring term, students presented case studies each week from the small body of existing research on building verified systems. “There’s not a book you can read about this topic,” Zeldovich said, noting that the case studies enabled students to see what tools and approaches others have used to try to create verified systems. This investigation in turn informed the students’ own strategies for developing provable software using such tools such as Coq, Dafny, and Bedrock.
The key deliverable for the class was a research paper highlighting findings from the students’ efforts to build verified systems. Students met one-on-one with professors each week to review their projects, which were intended primarily to advance the field rather than to develop practical skills. “It’s not likely you’ll go to a company and in five years be doing something like this, but [certified systems software is] a cool technology that’s intellectually fascinating and the holy grail is there in the back of your mind—is it really true that we might build be able to build provably correct software?” Zeldovich said.
The possibility certainly intrigues the business world. Research that emerged from this class made headlines last summer, when media outlets Forbes and ComputerWorld reported on a successful effort to develop a file system that was mathematically proved error-free. The system built by the MIT team is not optimized for practical use, but it comes with a mathematical proof that it will not lose data in a crash—which is groundbreaking.
“We were first to build a file system that proves implementation meets specifications,” said Kaashoek, noting that four EECS students worked on the project—graduate students Haogang Chen and Tej Chajed and undergraduates Daniel Ziegler and Stephanie Wang. In addition, the paper was co-authored by Zeldovich and EECS Associate Professor Adam Chlipala, whose research on the forefront of verification first inspired Kaachoek and Zeldovich to develop the class. The team’s paper, “Using Crash Hoare Logic for Certifying the FSCQ File System,” won a best paper award at the 2015 ACM Symposium on Operating Systems Principles in October.
Other research that emerged from the class included:
An effort to ensure that packet filters downloaded into the kernel is bug-free. This project addressed a fundamental cyber-security concern, since software downloads can serve as entry points for malicious code than can damage a computer’s operating system (OS). Louis Sobel ’14, MEng ‘15 endeavored to develop a verified compiler that generates provably correct code, which can then safely downloaded in the kernel.
A framework for verifying the security of various network protocols. Undergraduate Andres Erbsen addressed the challenge of how to prove that a network is safe from deliberate attack. For his project, Erbsen built a formal model of high-level cryptographic operations such as sign and verify using Coq and successfully proved that no action by an attacker could breach the model’s security.
Both professors said the 6.888 seminar was enjoyable to teach because it was a small class focused on collaboratively exploring new avenues in systems software.
“We learned a lot about this field ourselves,” Zeldovich said. “[This research] changes the way you think about building software and about the properties of systems.”
Both professors said they expect research into systems verification to become increasingly relevant in the years to come. “The systems verification community has made so much progress that the question is, are we at an inflection point? I think the answer is yes,” Kaashoek said, though he admitted that real-world applications were likely many years down the line. “Maybe in long run they’ll be an undergraduate class [on this topic] that everyone takes, but we’re far away from that point.”