DIFFuzzer: one more step toward specification-based file system quality checking

DIFFuzzer: one more step toward specification-based file system quality checking

Yanin A.S. (ITMO University, St. Petersburg, Russia)
Itsykson V.M. (ITMO University, St. Petersburg, Russia)
Kechin V.V. (ITMO University, St. Petersburg, Russia)
Kovalevsky V.M. (ITMO University, St. Petersburg, Russia)

Abstract

We present a refinement of DIFFuzzer, a mutation-based differential file system fuzzer, by integrating formal specifications to improve its testing capabilities. Initially, DIFFuzzer relied on a reference-based approach and embedded POSIX behavior into the source code for workload generation, which limited its flexibility and scalability. Our improved approach decouples the fuzzer's logic from these rules by incorporating an external formal file system specification written in the LibSL language. This enables the creation of more precise test oracles and facilitates specification-driven workload generation. We detail the current state of the project, including the extension of LibSL and the implementation of a specification-based test oracle. We also discuss future directions and their associated challenges, such as the evolution of our POSIX formalization and the planned development of a specification-based workload generation module.

Keywords

model-based testing; fuzzing; formal specification; file systems; POSIX.

Edition

Proceedings of the Institute for System Programming, vol. 38, issue 5, 2026, pp. 91-102

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(5)-6

For citation

Yanin A.S., Itsykson V.M., Kechin V.V., Kovalevsky V.M. DIFFuzzer: one more step toward specification-based file system quality checking. Proceedings of the Institute for System Programming, vol. 38, issue 5, 2026, pp. 91-102 DOI: 10.15514/ISPRAS-2026-38(5)-6.

Full text of the paper in pdf Back to the contents of the volume