Trustworthy Systems

File systems deserve verification too!

Authors

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

NICTA

UNSW

University of Toronto

A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 58-64.

Abstract

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.

BibTeX Entry

  @inproceedings{Keller_MAOCRKH_13,
    address          = {Farmington, Pennsylvania, USA},
    author           = {Keller, Gabriele and Murray, Toby and Amani, Sidney and O'Connor, Liam and Chen, Zilin and Ryzhyk,
                        Leonid and Klein, Gerwin and Heiser, Gernot},
    booktitle        = {Workshop on Programming Languages and Operating Systems (PLOS)},
    doi              = {10.1145/2525528.2525530},
    month            = nov,
    pages            = {1--7},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7248.pdf},
    slides           = {https://trustworthy.systems/publications/nicta_slides/7248.pdf},
    title            = {File Systems Deserve Verification Too!},
    year             = {2013}
  }

Download