License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.25
URN: urn:nbn:de:0030-drops-110807
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11080/
Go to the corresponding LIPIcs Volume Portal

Mehta, Mihir Parang ; Cook, William R.

Binary-Compatible Verification of Filesystems with ACL2

pdf-format:
LIPIcs-ITP-2019-25.pdf (0.5 MB)

Abstract

Filesystems are an essential component of most computer systems. Work on the verification of filesystem functionality has been focused on constructing new filesystems in a manner which simplifies the process of verifying them against specifications. This leaves open the question of whether filesystems already in use are correct at the binary level.
This paper introduces LoFAT, a model of the FAT32 filesystem which efficiently implements a subset of the POSIX filesystem operations, and HiFAT, a more abstract model of FAT32 which is simpler to reason about. LoFAT is proved to be correct in terms of refinement of HiFAT, and made executable by enabling the state of the model to be written to and read from FAT32 disk images. EqFAT, an equivalence relation for disk images, considers whether two disk images contain the same directory tree modulo reordering of files and implementation-level details regarding cluster allocation. A suite of co-simulation tests uses EqFAT to compare the operation of existing FAT32 implementations to LoFAT and check the correctness of existing implementations of FAT32 such as the mtools suite of programs and the Linux FAT32 implementation. All models and proofs are formalized and mechanically verified in ACL2.

BibTeX - Entry

@InProceedings{mehta_et_al:LIPIcs:2019:11080,
  author =	{Mihir Parang Mehta and William R. Cook},
  title =	{{Binary-Compatible Verification of Filesystems with ACL2}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11080},
  URN =		{urn:nbn:de:0030-drops-110807},
  doi =		{10.4230/LIPIcs.ITP.2019.25},
  annote =	{Keywords: interactive theorem proving, filesystems}
}

Keywords: interactive theorem proving, filesystems
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: The proof development described in this paper has been incorporated into the ACL2 Community books; these are part of the ACL2 distribution on GitHub (http://www.github.com/acl2/acl2). The source code for the models and proofs, with instructions for certifying the models, is available (https://github.com/acl2/acl2/tree/master/books/projects/filesystems).

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI