Skip to main content
SpringerLink
Log in

Separation Logic-Based Verification Atop a Binary-Compatible Filesystem Model

  • Conference paper
  • First Online:
Formal Methods: Foundations and Applications (SBMF 2020)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12475))

Included in the following conference series:

  • 247 Accesses

Abstract

Filesystems have held the interest of the formal verification community for a while, with several high-performance filesystems constructed with accompanying proofs of correctness. However, the question of verifying an existing filesystem and incorporating filesystem-specific guarantees remains unexplored, leaving those application developers underserved who need to work with a specific filesystem known to be fit for their purpose. In this work, we present an implementation of a verified filesystem which matches the specification of an existing filesystem, and with our new model AbsFAT tie it to the reasoning framework of separation logic in order to verify properties of programs which use the filesystem. This work is intended to match the target filesystem, FAT32, at a binary level and return the same data and error codes returned by mature FAT32 implementations, considered canonical. We provide a logical framework for reasoning about program behavior when filesystem calls are involved in terms of separation logic, and adapt it to simplify and automate the proof process in ACL2. By providing this framework, we encourage and facilitate greater adoption of software verification by application developers.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We use the values \(\mathsf {ENOENT}\), \(\mathsf {ENOTDIR}\) as the return values of system calls, but POSIX enumerates these as values assigned to the global variable errno, which is different from the function’s actual return value. Our implementation of each system call must return both these values, in order to capture the entirety of the effect of the system call in ACL2, a functional language lacking global program state. For brevity in this paper, however, we find it convenient to refer to a single return value which is zero in the case of success, and one of the errno values enumerated by POSIX  [15] in the case of failure. This is no less informative than providing the return value and the errno value separately, since none of our system calls sets errno to 0 upon success.

  2. 2.

    We replace inodes in the original grammar with strings. In FAT32, with no hardlinks, it is easier to just represent the contents of regular files as strings.

  3. 3.

    This is a term from ACL2 lore, and often used in the ACL2 source code.

References

  1. ACL2 Community: ACL2 documentation for MBE. http://www.cs.utexas.edu/users/moore/acl2/current/manual/index.html?topic=ACL2____MAKE-EVENT

  2. Amani, S., et al.: Cogent: verifying high-assurance file system implementations. ACM SIGPLAN Not. 51(4), 175–188 (2016)

    Article  Google Scholar 

  3. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)

    Book  Google Scholar 

  4. Chajed, T., Tassarotti, J., Kaashoek, M.F., Zeldovich, N.: Argosy: verifying layered storage systems with recovery refinement. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 1054–1068. ACM (2019)

    Google Scholar 

  5. Chen, H., et al.: Verifying a high-performance crash-safe file system using a tree specification. In: Proceedings of the 26th Symposium on Operating Systems Principles (SOSP), pp. 270–286. ACM (2017)

    Google Scholar 

  6. Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N.: Using crash Hoare logic for certifying the FSCQ file system. In: USENIX Annual Technical Conference (USENIX ATC 2016). USENIX Association (2016)

    Google Scholar 

  7. Floyd, R.W.: Assigning meanings to programs. Proc. Am. Math. Soc. Symp. Appl. Math. 6, 19–31 (1967)

    Article  MathSciNet  Google Scholar 

  8. Gardner, P., Ntzik, G., Wright, A.: Local reasoning for the POSIX file system. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 169–188. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54833-8_10

    Chapter  Google Scholar 

  9. Goel, S.: Formal verification of application and system programs based on a validated x86 ISA model. Ph.D. thesis, Department of Computer Science, The University of Texas at Austin (2016)

    Google Scholar 

  10. Hesselink, W.H., Lali, M.: Formalizing a hierarchical file system. Electron. Not. Theoret. Comput. Sci. 259, 67–85 (2009). Proceedings of the 14th BCS-FACS Refinement Workshop (REFINE)

    Google Scholar 

  11. Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  Google Scholar 

  12. Ileri, A., Chajed, T., Chlipala, A., Kaashoek, F., Zeldovich, N.: Proving confidentiality in a file system using DiskSec. In: 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pp. 323–338. USENIX Association, October 2018

    Google Scholar 

  13. Kerrisk, M.: Basename (3)-Linux manual page. Accessed 01 Aug 2020

    Google Scholar 

  14. Kerrisk, M.: Dirname (3)-Linux manual page. Accessed 01 Aug 2020

    Google Scholar 

  15. Kerrisk, M.: Errno (3)-Linux manual page. Accessed 01 Oct 2019

    Google Scholar 

  16. Koh, N., et al.: From C to interaction trees: specifying, verifying, and testing a networked server. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pp. 234–248. ACM (2019)

    Google Scholar 

  17. Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)

    Book  Google Scholar 

  18. Mehta, M.P., Cook, W.R.: Binary-compatible verification of filesystems with ACL2. In: 10th International Conference on Interactive Theorem Proving (ITP). Leibniz International Proceedings in Informatics (LIPIcs), vol. 141, pp. 25:1–25:18. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019)

    Google Scholar 

  19. Microsoft: Microsoft extensible firmware initiative FAT32 file system specification, December 2000. https://download.microsoft.com/download/1/6/1/161ba512-40e2-4cc9-843a-923143f3456c/fatgen103.doc

  20. Morgan, C., Sufrin, B.: Specification of the UNIX filing system. IEEE Trans. Softw. Eng. SE-10(2), 128–142 (1984)

    Google Scholar 

  21. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  22. Myreen, M.O.: Separation logic adapted for proofs by rewriting. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 485–489. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_34

    Chapter  Google Scholar 

  23. Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer, Heidelberg (2002)

    Book  Google Scholar 

  24. Ntzik, G., da Rocha Pinto, P., Sutherland, J., Gardner, P.: A concurrent specification of POSIX file systems. In: 32nd European Conference on Object-Oriented Programming (ECOOP). Leibniz International Proceedings in Informatics (LIPIcs), vol. 109, pp. 4:1–4:28. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018)

    Google Scholar 

  25. O’Hearn, P., Reynolds, J., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44802-0_1

    Chapter  Google Scholar 

  26. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 55–74. IEEE Computer Society (2002)

    Google Scholar 

  27. Bug: file-system file-size limit handling (2011). http://shareaza.sourceforge.net/phpbb/viewtopic.php?f=7&t=1118

  28. Sigurbjarnarson, H., Bornholt, J., Torlak, E., Wang, X.: Push-button verification of file systems via crash refinement. In: 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pp. 1–16. USENIX Association, November 2016

    Google Scholar 

  29. Wright, A.: Structural separation logic. Ph.D. thesis, Imperial College London (2013)

    Google Scholar 

  30. Yang, H., O’Hearn, P.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 402–416. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45931-6_28

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Texas at Austin, Austin, TX, 78712, USA

    Mihir Parang Mehta & William R. Cook

Authors
  1. Mihir Parang Mehta
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. William R. Cook
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mihir Parang Mehta .

Editor information

Editors and Affiliations

  1. Federal University of Pernambuco, Recife, Brazil

    Gustavo Carvalho

  2. Western Norway University of Applied Sciences, Bergen, Norway

    Volker Stolz

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Mehta, M.P., Cook, W.R. (2020). Separation Logic-Based Verification Atop a Binary-Compatible Filesystem Model. In: Carvalho, G., Stolz, V. (eds) Formal Methods: Foundations and Applications. SBMF 2020. Lecture Notes in Computer Science(), vol 12475. Springer, Cham. https://doi.org/10.1007/978-3-030-63882-5_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-63882-5_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-63881-8

  • Online ISBN: 978-3-030-63882-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation