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.
- 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
Proving confidentiality in a file system using DiskSec
Atalay Ileri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich
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
Verifying an I/O-Concurrent File System
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.
- 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.
Our source code is available on GitHub at mit-pdos/fscq.
This research was supported in part by NSF award 1563763.