FSCQ: File-system verification

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.




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.