File systems deserve verification too

File systems are too important, and current ones are too buggy, to remain unverified. Yet the most successful verification methods for functional correctness remain too expensive for current file system implementations-we need verified correctness but at reasonable cost. This paper presents our visi...

Full description

Saved in:
Bibliographic Details
Main Authors: Keller, Gabriele, Murray, Toby, Amani, Sidney, O'Connor, Liam, Chen, Zilin, Ryzhyk, Leonid, Klein, Gerwin, Heiser, Gernot
Format: Conference Proceeding
Language:English
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:File systems are too important, and current ones are too buggy, to remain unverified. Yet the most successful verification methods for functional correctness remain too expensive for current file system implementations-we need verified correctness but at reasonable cost. This paper presents our vision and ongoing work to achieve this goal for a new high-performance flash file system, called BilbyFs. BilbyFs is carefully designed to be highly modular, so it can be verified against a high-level functional specification one component at a time. This modular implementation is captured in a set of domain specific languages from which we produce the design-level specification, as well as its optimised C implementation. Importantly, we also automatically generate the proof linking these two artefacts. The combination of these features dramatically reduces verification effort. Verified file systems are now within reach for the first time.
ISSN:0163-5980
DOI:10.1145/2626401.2626414