File Systems Deserve Verification Too!

Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein, Gernot Heiser

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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 filesystems are now within reach for the first time.
Original languageEnglish
Title of host publicationProceedings of the Seventh Workshop on Programming Languages and Operating Systems
Place of PublicationNew York, NY, USA
PublisherACM Association for Computing Machinery
Number of pages7
ISBN (Print)9781450324601
DOIs
Publication statusPublished - 3 Nov 2013
Event7th Workshop on Programming Languages and Operating Systems - Farmington, United States
Duration: 3 Nov 20133 Nov 2013

Conference

Conference7th Workshop on Programming Languages and Operating Systems
Abbreviated titlePLOS 2013
Country/TerritoryUnited States
CityFarmington
Period3/11/133/11/13

Fingerprint

Dive into the research topics of 'File Systems Deserve Verification Too!'. Together they form a unique fingerprint.
  • File Systems Deserve Verification Too!

    Keller, G., Murray, T., Amani, S., O'Connor, L., Chen, Z., Ryzhyk, L., Klein, G. & Heiser, G., 15 May 2014, In: Operating Systems Review. 48, 1, p. 58–64 7 p.

    Research output: Contribution to journalArticlepeer-review

Cite this