Project overview

FSCQ is the first file system with a machine-checkable proof (in the Coq proof assistant) that its implementation meets its specification and whose specification includes behavior under crashes.

The original version of FSCQ (as presented in the SOSP 2015 paper) guaranteed transactional behavior for every system call: if the system crashes and recovers, either the entire system call or none of it appears to execute. We also wrote a CACM paper, which is a more accessible version of the SOSP paper. A followup paper (presented in SOSP 2017) improved performance by deferring durability of writes and specifying the new relaxed behavior. We’ve also extended the system with a proof that file data remains confidential, as described in the DiskSec paper in OSDI 2018.

People

• Tej Chajed (PhD)
• Atalay İleri (PhD)
• Alex Konradi (MEng, alum)
• Daniel Ziegler (MEng, alum)
• Haogang Chen (PhD, alum)
• Prof. M. Frans Kaashoek
• Prof. Nickolai Zeldovich
• Prof. Adam Chlipala

Publications

• Proving confidentiality in a file system using DiskSec
  Atalay Ileri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich

  OSDI 2018

• Verifying a high-performance crash-safe file system using a tree specification
  Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay Ileri, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich

  SOSP 2017

• Verifying an I/O-Concurrent File System
  Tej Chajed

  Master’s thesis, advised by M. Frans Kaashoek and Nickolai Zeldovich.

• Using Crash Hoare Logic for Certifying the FSCQ File System
  Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich

  SOSP 2015 (Best paper award)

• Specifying crash safety for storage systems
  Haogang Chen, Daniel Ziegler, Adam Chlipala, M. Frans Kaashoek, Eddie Kohler, and Nickolai Zeldovich.

  HotOS 2015

Publicity

• MIT researchers create file system guaranteed not to lose data even if a PC crashes, Computer World.
• MIT Researchers Create Crash-Tolerant File System Guaranteed Not To Lose Data, Forbes.

Source code

Our source code is available on GitHub at mit-pdos/fscq.

Funding support

This research was supported in part by NSF award 1563763.