Events Calendar

EE 598 Computer Engineering Seminar

Speaker: Nickolai Zeldovich, Associate Professor, MIT

Talk 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.


Biography: 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.

Host: Xuehai Qian

Location: Olin Hall of Engineering (OHE) - OHE 100D

Audiences: Everyone Is Invited

Contact: Estela Lopez