File Systems Deserve Verification Too!

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

doi:10.1145/2626401.2626414

File Systems Deserve Verification Too!

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

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Pages (from-to)	58–64
Number of pages	7
Journal	Operating Systems Review
Volume	48
Issue number	1
DOIs	https://doi.org/10.1145/2626401.2626414
Publication status	Published - 15 May 2014

Access to Document

10.1145/2626401.2626414Licence: All Rights Reserved

https://dl.acm.org/doi/abs/10.1145/2626401.2626414Licence: All Rights Reserved

1 Conference contribution

File Systems Deserve Verification Too!
Keller, G., Murray, T., Amani, S., O'Connor, L., Chen, Z., Ryzhyk, L., Klein, G. & Heiser, G., 3 Nov 2013, Proceedings of the Seventh Workshop on Programming Languages and Operating Systems. New York, NY, USA: ACM Association for Computing Machinery, 7 p. 1
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Cite this

@article{eb60f160115f42e69e5d69b5e286dfa2,

title = "File Systems Deserve Verification Too!",

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.",

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

year = "2014",

month = may,

day = "15",

doi = "10.1145/2626401.2626414",

language = "English",

volume = "48",

pages = "58–64",

journal = "Operating Systems Review",

issn = "0163-5980",

publisher = "Association for Computing Machinery (ACM)",

number = "1",

}

TY - JOUR

T1 - File Systems Deserve Verification Too!

AU - Keller, Gabriele

AU - Murray, Toby

AU - Amani, Sidney

AU - O'Connor, Liam

AU - Chen, Zilin

AU - Ryzhyk, Leonid

AU - Klein, Gerwin

AU - Heiser, Gernot

PY - 2014/5/15

Y1 - 2014/5/15

N2 - 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.

AB - 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.

U2 - 10.1145/2626401.2626414

DO - 10.1145/2626401.2626414

M3 - Article

SN - 0163-5980

VL - 48

SP - 58

EP - 64

JO - Operating Systems Review

JF - Operating Systems Review

IS - 1

ER -

File Systems Deserve Verification Too!

Abstract

Access to Document

Fingerprint

Research output

File Systems Deserve Verification Too!

Cite this