SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems
复制标题
DOI：
10.1145/2815400.2815411
复制
发表时间：
2015-10
期刊：
影响因子：
--
通讯作者：
T. Ridge;David Sheets;T. Tuerk;A. Giugliano;Anil Madhavapeddy;Peter Sewell
中科院分区：
文献类型：
--
作者：
T. Ridge;David Sheets;T. Tuerk;A. Giugliano;Anil Madhavapeddy;Peter Sewell
系统在实现和每个实现之间以及POSIX（和其他）散文规范之间的许多细节上都取决于文件系统的行为，但是这种行为在许多细节上有所不同。构建健壮和便携式软件需要了解这些详细信息和差异，但是当前没有一个很好的方法来系统地描述，调查或测试该复杂多平台界面的文件系统行为。在本文中，我们展示了如何以实现实用且高度歧视的测试的形式来表征文件系统允许行为的信封。我们给出了一个数学上严格的文件系统行为模型SIBYLFS，该模型指定了我们范围内的任何系统调用序列的文件系统允许行为的范围，并且可以用作测试甲骨文来决定观察到的跟踪该模型允许验证模型和针对该模型测试文件系统。 SIBYLFS的模块化不仅足以描述POSIX，还可以描述特定的Linux，OS X和FreeBSD行为。我们使用超过21 000次测试的广泛测试套件对模型进行补充；这可以在目标文件系统上运行，并在不到5分钟的时间内进行检查，从而在实践中可用。最后，我们报告了许多文件系统的大约40个配置的实验结果，从而确定了许多差异和一些严重的缺陷。
Systems depend critically on the behaviour of file systems, but that behaviour differs in many details, both between implementations and between each implementation and the POSIX (and other) prose specifications. Building robust and portable software requires understanding these details and differences, but there is currently no good way to systematically describe, investigate, or test file system behaviour across this complex multi-platform interface. In this paper we show how to characterise the envelope of allowed behaviour of file systems in a form that enables practical and highly discriminating testing. We give a mathematically rigorous model of file system behaviour, SibylFS, that specifies the range of allowed behaviours of a file system for any sequence of the system calls within our scope, and that can be used as a test oracle to decide whether an observed trace is allowed by the model, both for validating the model and for testing file systems against it. SibylFS is modular enough to not only describe POSIX, but also specific Linux, OS X and FreeBSD behaviours. We complement the model with an extensive test suite of over 21 000 tests; this can be run on a target file system and checked in less than 5 minutes, making it usable in practice. Finally, we report experimental results for around 40 configurations of many file systems, identifying many differences and some serious flaws.