Have you ever been working when the power goes poof and then you’ve lost all the data since you last saved? The day may be coming when you never have to worry about losing data again if a computer crashes thanks to a new “file system that could lead to computers guaranteed never to lose your data.” Big brains at MIT have come up with “the first file system that is mathematically guaranteed not to lose track of data during crashes.”
MIT's Electrical Engineering and Computer Science (EECS) Department announced that MIT researchers will present their new research on “Using Crash Hoare logic for Certifying the FSCQ File System” at the 25th ACM Symposium on Operating Systems Principles (SOSP'15) in October.
FSCQ is a novel file system with a machine-checkable proof (using the Coq Proof Assistant) that its implementation meets its specification, even under crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover the file system correctly without losing data. To state FSCQ's theorems, this paper introduces the Crash Hoare logic (CHL), which extends traditional Hoare logic with a crash predicate, a recovery function, and name spaces (which allow specifying disk states at different abstraction levels in the file system). To help prove FSCQ's theorems, we chose a simple design for FSCQ. However, experiments with FSCQ running as a user-level file system show that even this simple design is sufficient to run Unix applications with usable performance.
MIT explained, “Formal verification involves mathematically describing the acceptable bounds of operation for a computer program and then proving that the program will never exceed them. It’s a complicated process, so it’s generally applied only to very high-level schematic representations of a program’s functionality. Translating those high-level schema into working code, however, can introduce myriad complications that the proofs don’t address.”
Although high-level schema existed, MIT was the first to “prove properties of the file system’s final code.” Theirs was “not some whiteboard idealization that has no formal connection to the code,” Chlipala said.
According to Daniel Ziegler, an undergraduate in EECS who took part in the 2014 Chaos Communication Congress lecture ‘Now I sprinkle thee with crypto dust,’ “All these paper proofs about other file systems may actually be correct, but there’s no file system that we can be sure represents what the proof is about.”
Sign up for CIO Asia eNewsletters.