Principal Investigator M Kaashoek
Co-investigators Nickolai Zeldovich , Adam Chlipala
Project Website http://www.nsf.gov/awardsearch/showAward?AWD_ID=1563763&HistoricalAwards=false
Project Start Date June 2016
Project End Date May 2020
Applications rely on file systems to store their data, but even carefully written applications and file systems may have bugs that cause data loss, especially in the face of system crashes (e.g., due to power failure). Even in mature file systems such as ext4, bugs that can lead to data loss are not uncommon. Application developers also misuse file-system APIs in ways that lead to user data being lost after a crash.
Formal verification is a good way to prove the absence of bugs in a file system. By considering all possible operations and crashes, verification can ensure that the file system is bug-free. The goal of this proposal is to develop a certified high-performance file system, VCFS (Verified Concurrent File System). The investigators aim to make VCFS's performance good enough to support demanding applications while guaranteeing crash safety. VCFS and its applications will come with mathematical proofs that their implementations meet their specifications under any sequences of crashes.
The main outcomes of this research will be as follows: (1) A logic system, CFSL (Concurrent File System Logic), that allows reasoning about parallelism and crashes. (2) A precise specification of the POSIX API under concurrency and crashes. (3) The VCFS file system, for which we will prove that its implementation meets our POSIX specification under crashes and concurrency. VCFS will include sophisticated performance optimizations. (4) A certified high-performance mail server, as a test case of using VCFS and its formally specified APIs to prove application-level properties (in this case, that the server will not lose acknowledged messages).
CFSL will enable developers to reason about concurrency and crashes in the context of file systems. The POSIX specification, along with VCFS, will help programmers develop applications that are both high-performance and safe under computer crashes. The investigators will use their understanding of writing certified software to create a new class on certified software.