Date November 17, 2016
Speaker Nickolai Zeldovich
Massachusetts Institute of Technology
Title Certifying a Crash-Safe File System
Abstract Users and applications rely on file systems to store their data, but file systems themselves can have bugs that lead to data loss, especially after a system crashes and restarts.

This talk will describe our work on FSCQ, the first file system that (1) comes with a precise specification of its behavior, including what can occur after a crash, and that (2) provides a machine-checked proof that its implementation meets this precise specification, using the Coq proof assistant. FSCQ's proofs avoid crash-safety bugs that have plagued file systems, such as forgetting to insert a disk write barrier between writing the data to the log and writing the log's commit block. FSCQ's specification also allows applications to prove their own crash safety, avoiding application-level bugs such as forgetting to invoke fsync on both the file and the containing directory. As a result, applications on FSCQ can provide strong guarantees: they will not lose data under any sequence of crashes.

Our experimental evaluation shows that the FSCQ prototype achieves reasonable I/O performance, on par with Linux ext4, and that, empirically, the theorems appear to work: FSCQ can recover from all possible crashes for small test programs, and FSCQ passes a variety of stress tests. One limitation of the FSCQ prototype is its high CPU overhead, owing to its use of Haskell for generating executable code .
Bio Nickolai Zeldovich is an Associate Professor at MIT's department of Electrical Engineering and Computer Science, and a member of the Computer Science and Artificial Intelligence Laboratory. His research interests are in building practical secure systems, from operating systems and hardware to programming languages and security analysis tools. He received his PhD from Stanford University in 2008, where he developed HiStar, an operating system designed to minimize the amount of trusted code by controlling information flow. In 2005, he co-founded MokaFive, a company focused on improving desktop management and mobility using x86 virtualization.

These seminars supported by the Ming Hsieh Institute.