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. A followup paper (presented in SOSP 2017) improved performance by deferring durability of writes and specifying the new relaxed behavior.
We are actively working on FSCQ from several angles.
One line of work focuses on making FSCQ concurrent. Our current approach focuses on I/O concurrency (overlapping disk usage with servicing system calls from in-memory caches) and read-only concurrency on multiple cores. It achieves these limited forms of concurrency without making any changes to the existing code or proofs.
Second, we are interested in extending FSCQ’s implementation and specification with security-related guarantees. Ordinary functional correctness specifications can guarantee isolation in a straightforward manner by showing no user can change other users’ data. However, less straightforward is to formalize and prove a confidentiality property, namely that users never observe other users’ data. Furthermore, the file system doesn’t provide complete confidentiality (eg, users can infer something about the number of files based on sequential inode numbers), but we do want to prove that file data is confidential. Our approach is focused on proving confidentiality while making minimal changes to existing code and proofs.
- 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
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.