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 for practical, real-world software systems. 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 away, 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-safe file system, so that the file system’s data is still intact even if it crashes. In the past, file systems have had bugs 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.  

Bio

Nickolai Zeldovich is a professor of Electrical Engineering and Computer Science at MIT, and a member of the Computer Science and Artificial Intelligence Laboratory. He received his PhD from Stanford University in 2008. His research interests are in building practical secure systems. Recent projects by Prof. Zeldovich and his students and colleagues include the CryptDB encrypted database, the STACK tool for finding undefined behavior bugs in C programs, the FSCQ formally verified file system, the Algorand cryptocurrency, and the Vuvuzela private messaging system. He has been involved with several start-up companies, including MokaFive (desktop virtualization), PreVeil (end-to-end encryption), and Algorand (cryptocurrency). Prof. Zeldovich's work has been recognized by best paper awards at the ACM SOSP conference, a Sloan fellowship (2010), an NSF CAREER award (2011), the MIT EECS Spira teaching award (2013), the MIT Edgerton faculty achievement award (2014), the ACM SIGOPS Mark Weiser award (2017), and an MIT EECS Faculty Research Innovation Fellowship (2018).