Verification of a Virtual Filesystem Switch

Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, and Wolfgang Reif

This work presents part of our verification effort to construct a correct file system for Flash memory. As a blueprint we use UBIFS, which is part of Linux. As all file systems in Linux, UBIFS implements the Virtual Filesystem Switch (VFS) interface. VFS in turn implements top-level POSIX operations. This paper bridges the gap between an ab- stract specification of POSIX and a realistic model of VFS by ASM refinement. The models and proofs are mechanized in the interactive the- orem prover KIV. Algebraic directory trees are mapped to the pointer structures of VFS using Separation Logic. We consider hard-links, file handles and the partitioning of file content into pages.
published 2014 In Proc. of Fifth Working Conference on Verified Software: Theories, Tools and Experiments

Publisher: Springer

DOI: Springer Link


The final publication is available at Springer via 978-3-642-54108-7_13.

For questions regarding the publication, please contact!