Document Open Access Logo

Binary-Compatible Verification of Filesystems with ACL2

Authors Mihir Parang Mehta, William R. Cook

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.25.pdf
  • Filesize: 492 kB
  • 18 pages

Document Identifiers

Author Details

Mihir Parang Mehta
  • University of Texas at Austin, USA
William R. Cook
  • University of Texas at Austin, USA

Funding

  • Mehta, Mihir Parang: This material is based upon work supported by the National Science Foundation under Grant No. CNS-1525472.

Acknowledgements

Thanks to Warren A. Hunt Jr. and Matt Kaufmann for their guidance.

Cite AsGet BibTex

Mihir Parang Mehta and William R. Cook. Binary-Compatible Verification of Filesystems with ACL2. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.25

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • interactive theorem proving
  • filesystems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253-284, 1991. URL: https://doi.org/10.1016/0304-3975(91)90224-P.
  2. ACL2 Community. ACL2 documentation for B*. See URL URL: http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=ACL2____B_A2.
  3. ACL2 Community. ACL2 documentation for DEFUND-NX. See URL URL: http://www.cs.utexas.edu/users/moore/acl2/current/manual/index.html?topic=ACL2____DEFUND-NX.
  4. ACL2 Community. ACL2 documentation for MBE. See URL URL: http://www.cs.utexas.edu/users/moore/acl2/current/manual/index.html?topic=ACL2____MBE.
  5. ACL2 Community. ACL2 documentation for READ-FILE-INTO-STRING. See URL URL: http://www.cs.utexas.edu/users/moore/acl2/current/manual/index.html?topic=ACL2____READ-FILE-INTO-STRING.
  6. Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, et al. Cogent: Verifying high-assurance file system implementations. ACM SIGPLAN Notices, 51(4):175-188, 2016. URL: https://doi.org/10.1145/2872362.2872404.
  7. Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions. Springer Science & Business Media, 2013. URL: https://doi.org/10.1007/978-3-662-07964-5.
  8. William R. Bevier and Richard M. Cohen. An executable model of the Synergy file system. Technical report, Technical Report 121, Computational Logic, Inc, 1996. Google Scholar
  9. Robert S. Boyer and J Strother Moore. Single-threaded objects in ACL2. In International Symposium on Practical Aspects of Declarative Languages, pages 9-27. Springer, 2002. URL: https://doi.org/10.1007/3-540-45587-6_3.
  10. Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay İleri, Adam Chlipala, M Frans Kaashoek, and Nickolai Zeldovich. Verifying a high-performance crash-safe file system using a tree specification. In Proceedings of the 26th Symposium on Operating Systems Principles, pages 270-286. ACM, 2017. Google Scholar
  11. Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Using Crash Hoare Logic for Certifying the FSCQ File System. In USENIX Annual Technical Conference, 2016. Google Scholar
  12. Russ Cox, M. Frans Kaashoek, and Robert T. Morris. Xv6, a simple Unix-like teaching operating system, 2016. URL: http://pdos.csail.mit.edu/6.828/2014/xv6.html.
  13. Jared Davis. Reasoning about ACL2 file input. In Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications, pages 117-126. ACM, 2006. Google Scholar
  14. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  15. Paul Eggert, Mike Haertel, David Hayes, Richard Stallman, and Len Tower. diff (1)-Linux manual page, accessed: 07 Sep 2018. Google Scholar
  16. Philippa Gardner, Gian Ntzik, and Adam Wright. Local reasoning for the POSIX file system. In European Symposium on Programming Languages and Systems, pages 169-188. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54833-8_10.
  17. Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann, and Soumava Ghosh. Simulation and formal verification of x86 machine-code programs that make system calls. In Formal Methods in Computer-Aided Design (FMCAD), 2014, pages 91-98. IEEE, 2014. URL: https://doi.org/10.1109/FMCAD.2014.6987600.
  18. David Greve. Address enumeration and reasoning over linear address spaces. In 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX, 2004. Google Scholar
  19. David Greve and Matt Wilding. Dynamic datastructures in ACL2: A challenge, 2002. URL: http://hokiepokie.org/docs/festival02.txt.
  20. Dave Hudson, Peter Anvin, and Roman Hodek. mkfs.fat (8)-Linux manual page, accessed: 09 Jul 2018. Google Scholar
  21. Atalay Ileri, Tej Chajed, Adam Chlipala, Frans Kaashoek, and Nickolai Zeldovich. Proving confidentiality in a file system using DISKSEC. In 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI'18), pages 323-338, 2018. Google Scholar
  22. Matt Kaufmann. Fixed read-file-into-string bug. (commit message), July 2018. URL: https://github.com/acl2/acl2/commit/8388ac10289d5cab791953238057294604af6d60.
  23. Matt Kaufmann and J Strother Moore. ACL2: An industrial strength version of Nqthm. In Proceedings of 11th Annual Conference on Computer Assurance (COMPASS'96), pages 23-34. IEEE, 1996. Google Scholar
  24. Michael Kerrisk. errno (3)-Linux manual page, accessed: 07 Sep 2018. Google Scholar
  25. Michael Kerrisk. mmap (2)-Linux manual page, accessed: 09 Dec 2018. Google Scholar
  26. Michael Kerrisk. pread (2)-Linux manual page, accessed: 09 Jul 2018. Google Scholar
  27. Michael Kerrisk. pwrite (2)-Linux manual page, accessed: 09 Jul 2018. Google Scholar
  28. Michael Kerrisk. rmdir (2)-Linux manual page, accessed: 17 Mar 2019. Google Scholar
  29. Michael Kerrisk. statfs (2)-Linux manual page, accessed: 09 Dec 2018. Google Scholar
  30. Evan Klitzke. PATH_MAX is tricky, April 2017. URL: https://eklitzke.org/path-max-is-tricky.
  31. Alain Knaff. mtools (1)-Linux manual page, accessed: 09 Dec 2018. Google Scholar
  32. Leslie Lamport. Verification and specification of concurrent programs. In Workshop/School/Symposium of the REX Project (Research and Education in Concurrent Systems), pages 347-374. Springer, 1993. URL: https://doi.org/10.1007/3-540-58043-3_23.
  33. Avantika Mathur, Mingming Cao, Suparna Bhattacharya, Andreas Dilger, Alex Tomas, and Laurent Vivier. The new ext4 filesystem: current status and future plans. In Proceedings of the Linux symposium, volume 2, pages 21-33, 2007. Google Scholar
  34. Mihir Parang Mehta. Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32. Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, page 18, 2018. Google Scholar
  35. Microsoft. Microsoft Extensible Firmware Initiative FAT32 File System Specification, December 2000. URL: https://download.microsoft.com/download/1/6/1/161ba512-40e2-4cc9-843a-923143f3456c/fatgen103.doc.
  36. Jayashree Mohan, Ashlie Martinez, Soujanya Ponnapalli, Pandian Raju, and Vijay Chidambaram. Finding Crash-Consistency Bugs with Bounded Black-Box Crash Testing. arXiv preprint, 2018. URL: http://arxiv.org/abs/1810.02904.
  37. Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-Button Verification of an OS Kernel. In Proceedings of the 26th Symposium on Operating Systems Principles, SOSP'17, pages 252-269, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3132747.3132748.
  38. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283. Springer Science & Business Media, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  39. N. Rath and M. Szeredi. The reference implementation of the Linux FUSE (Filesystem in Userspace) interface, 2018. Google Scholar
  40. Murray Shanahan. The Frame Problem. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, 2016. Google Scholar
  41. Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-Button Verification of File Systems via Crash Refinement. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 1-16, 2016. Google Scholar
  42. Peter Snyder. tmpfs: A virtual memory file system. In In Proceedings of the Autumn 1990 European UNIX Users' Group Conference, pages 241-248, 1990. Google Scholar
  43. Richard M Stallman. GNU Make, 1988. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact