Top

Published in:

2020 | OriginalPaper | Chapter

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

Authors : Mihir Parang Mehta, William R. Cook

Published in: Formal Methods: Foundations and Applications

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Reversal Fuzzy Switch Graphs

next chapter Merging Cloned Alloy Models with Colorful Refactorings

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.

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.

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

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

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

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

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)

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)

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)

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

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_10CrossRef

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)

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)

11.

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

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

13.

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

14.

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

15.

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

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)

17.

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

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)

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)

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_24CrossRef

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_34CrossRef

23.

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

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)

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_1CrossRef

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)

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

29.

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

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_28CrossRef

Title: Separation Logic-Based Verification Atop a Binary-Compatible Filesystem Model
Authors: Mihir Parang Mehta
William R. Cook
Publisher: Springer International Publishing
Book: Formal Methods: Foundations and Applications
Print ISBN: 978-3-030-63881-8

Electronic ISBN: 978-3-030-63882-5

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-63882-5_10

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner