In an ideal world, computers would work fast, never fail, and be free of security exploits. In our current reality, though, systems tend to fail or have security exploits due to bugs in the software, and people spend a tremendous amount of time and resources trying to find bugs and testing software. How, then, do we make software and systems more provably secure?
Professors Frans Kaashoek and Nickolai Zeldovich of MIT CSAIL are interested in building practical secure systems, from operating systems and hardware to programming languages and security analysis tools. Together, they co-lead with Professor Adam Belay and Professor Robert Morris the Parallel and Distributed Operating Systems (PDOS) Group within CSAIL.
This vision for producing secure systems has a long history dating back to the 1960s, but in the last decade interest has been picking back up thanks to a tremendous improvement in verification technology that has enabled people to use verification practically for real-systems software. Previously, you could only use verification for toy programs, but now Prof. Kaashoek and Prof. Zeldovich are trying to figure out how to use that technology for serious software.
Their interest in security got them further into verification research. For example, in one of their past projects they found security bugs in Linux where the affected instruction sequences were only three or four lines of code. To the programmers, these lines of code appeared to be absolutely correct. As they investigated further, they realized that, due to undefined behavior, the lines were in fact incorrect, and the compiler would optimize them anyway, removing the security checks that those lines implemented.
This project raised the question: If not even experts could get a few lines of code correct or secure, then what tools or approaches could really convince them that a system is 100 percent, iron-clad secure? To answer this overarching question, they began to look into systems software verification for long-term solutions.
Infrastructure software for data centers powers many widely used cloud applications, and is therefore particularly important to be reliable and secure. Prof. Kaashoek and Prof. Zeldovich focus on the infrastructure of such systems. As an example, they implemented a provably correct crash-save file system, so that the file system’s data is still intact even if it crashes. In the past, systems have had ugs that can cause data to get lost, but their team developed a mathematical proof that eliminates this issue. Building on the file system, they also recently worked on a mail server that is concurrent and accepts email messages, and the team has been able to prove that no messages will get lost.
This research will ensure that eventually, important software will never crash and will be secure. In addition, programmers will be able to understand how the software operates more clearly because their systems will include more accurate specifications, allowing them to build better software.
Frans Kaashoek is the Charles Piper Professor in MIT's EECS department and a member of CSAIL, where he coleads the parallel and distributed operating systems (PDOS) group. He received his PhD from the Vrije Universiteit (Amsterdam, The Netherlands) for his work on group communication in the Amoeba distributed operating system. Frans is a member of the National Academy of Engineering and the American Academy of Arts and Sciences, the recipient of the ACM SIGOPS Mark Weiser award and the 2010 ACM Prize in Computing. He was a cofounder of Sightpath, Inc. and Mazu Networks, Inc.