Push-Button Verification of File Systems via Crash Refinement
Push-Button Verification of File Systems via Crash Refinement
复制标题
通过崩溃优化对文件系统进行一键式验证
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
L. Cranor
中科院分区：
文献类型：
--
作者：
Helgi Sigurbjarnarson;James Bornholt;Nicolas Christin;L. Cranor
文件系统是用于持续存储设备上数据的必不可少的操作系统组件。编写无错误的文件系统是不平凡的，因为即使在系统崩溃和磁盘操作的重新排序的情况下，它们也必须正确实现并维护复杂的盘中数据结构。
本文介绍了Yggdrasil，这是一种用于编写按钮验证的文件系统的工具包：Yggdrasil不需要有关实现代码的手动注释或证明，并且如果有错误，则会产生反例。 Yggdrasil通过称为Crash Refinement的文件系统正确性的新颖定义来实现此自动化，这要求由实现（包括崩溃产生的状态）产生的一组可能的磁盘状态作为规范允许的子集。崩溃的精炼可以适合完全自动化的满意度模型理论（SMT）推理，并使开发人员能够以模块化的方式实现文件系统进行验证。
使用Yggdrasil，我们已经实施并验证了YXV6日记文件系统，YCP文件复制实用程序和YLOG持久日志。我们的经验表明，易于证明和基于反例的调试支持使YGGDRASIL可以实用用于构建可靠的存储应用程序。
The file system is an essential operating system component for persisting data on storage devices. Writing bug-free file systems is non-trivial, as they must correctly implement and maintain complex on-disk data structures even in the presence of system crashes and reorderings of disk operations.
This paper presents Yggdrasil, a toolkit for writing file systems with push-button verification: Yggdrasil requires no manual annotations or proofs about the implementation code, and it produces a counterexample if there is a bug. Yggdrasil achieves this automation through a novel definition of file system correctness called crash refinement, which requires the set of possible disk states produced by an implementation (including states produced by crashes) to be a subset of those allowed by the specification. Crash refinement is amenable to fully automated satisfiability modulo theories (SMT) reasoning, and enables developers to implement file systems in a modular way for verification.
With Yggdrasil, we have implemented and verified the Yxv6 journaling file system, the Ycp file copy utility, and the Ylog persistent log. Our experience shows that the ease of proof and counterexample-based debugging support make Yggdrasil practical for building reliable storage applications.
在经过验证的闪存文件系统内部：事务和垃圾收集
DOI：
10.1007/978-3-319-29613-5_5
发表时间：
2015
期刊：
影响因子：
--
作者：
G. Ernst;J. Pfähler;G. Schellhorn;W. Reif
通讯作者：
W. Reif
DOI：
10.1145/2815400.2815411
发表时间：
2015-10
期刊：
Proceedings of the 25th Symposium on Operating Systems Principles
影响因子：
--
作者：
T. Ridge;David Sheets;T. Tuerk;A. Giugliano;Anil Madhavapeddy;Peter Sewell
通讯作者：
T. Ridge;David Sheets;T. Tuerk;A. Giugliano;Anil Madhavapeddy;Peter Sewell