Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32

TL;DR

This paper presents a method for creating and verifying executable specifications of filesystems, demonstrated through FAT32, enabling formal verification of filesystem properties in a theorem prover.

Contribution

It introduces a systematic methodology for building incremental, reusable models of filesystems for formal verification in ACL2, applied specifically to FAT32.

Findings

Successfully verified functional properties of FAT32

Developed reusable models for filesystem features

Demonstrated incremental modeling approach

Abstract

In this work, we present an approach towards constructing executable specifications of existing filesystems and verifying their functional properties in a theorem proving environment. We detail an application of this approach to the FAT32 filesystem. We also detail the methodology used to build up this type of executable specification through a series of models which incrementally add features of the target filesystem. This methodology has the benefit of allowing the verification effort to start from simple models which encapsulate features common to many filesystems and which are thus suitable for reuse.