Verifying filesystems for abstract separation logic-based program verification in the ACL2 theorem prover

The field of filesystem verification has been receiving steady attention from researchers from the filesystem and verification worlds, but some aspects remain unexplored. Considering it important to verify an existing filesystem with the property of binary compatibility - i.e. a filesystem which maintains a disk image in a state that can be read by existing implementations of that filesystem - we develop LoFAT, an efficient implementation of FAT32 in the language of the ACL2 theorem prover. Devising HiFAT, a directory-tree model of FAT32, we prove it to abstract LoFAT. This refinement relationship allows us to quickly prototype a number of filesystem calls in LoFAT, which we later replace with more efficient implementations that retain their correctness properties. We also validate LoFAT by co-simulation against mature implementations of FAT32, namely, the mtools and the Linux implementation of FAT32. Considering it important to support code proofs, i.e. proofs of correctness of programs making use of the filesystem, we develop such proofs for programs interacting with LoFAT. Initially relying on read-over-write properties of LoFAT, we later develop an abstract separation logic layer on top of HiFAT, which abstracts it and therefore abstract LoFAT. This layer, AbsFAT, allows us to concisely represent filesystem states and file operations on them. We show some code proofs that are simplified with the use of AbsFAT. Finally, we investigate the use of abstract separation logic to model concurrent operations on the filesystem. Choosing to focus on single-core concurrency, we use the standard approach which involves an oracle, i.e. an uninterpreted function that decides which of the waiting threads at any moment gets to execute the next instruction. We demonstrate a proof of code correctness based on this model, and conclude with some ideas for future work