TY - GEN
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 - 2013/11/3
Y1 - 2013/11/3
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 filesystems 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 filesystems are now within reach for the first time.
U2 - 10.1145/2525528.2525530
DO - 10.1145/2525528.2525530
M3 - Conference contribution
SN - 9781450324601
BT - Proceedings of the Seventh Workshop on Programming Languages and Operating Systems
PB - ACM Association for Computing Machinery
CY - New York, NY, USA
T2 - 7th Workshop on Programming Languages and Operating Systems
Y2 - 3 November 2013 through 3 November 2013
ER -