Parallel & Distributed Operating Systems Group

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. A followup paper (presented in SOSP 2017) improved performance by deferring durability of writes and specifying the new relaxed behavior.

Research directions

We are actively working on FSCQ from several angles.

Concurrency

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.

Security

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.

People

Publications

Publicity

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.