Separation Logic-Based Verification Atop a Binary-Compatible Filesystem Model
| Autor: | Mihir Parang Mehta, William R. Cook |
|---|---|
| Přispěvatelé: | University of Texas at Austin [Austin], Mehta, Mihir |
| Rok vydání: | 2020 |
| Předmět: |
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
Correctness Computer science Programming language 05 social sciences [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 02 engineering and technology Separation logic ACL2 computer.software_genre Binary code compatibility Automated theorem proving Logical framework [INFO.INFO-OS] Computer Science [cs]/Operating Systems [cs.OS] 020204 information systems 0502 economics and business Data_FILES 0202 electrical engineering electronic engineering information engineering 050211 marketing [INFO.INFO-OS]Computer Science [cs]/Operating Systems [cs.OS] Formal verification computer Software verification computer.programming_language |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030638818 SBMF |
| Popis: | 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 un-derserved 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|