Nicolas Jeannerod

Symbolic Execution of Maintainer Scripts

We attempt to compute a description of the possible effects a maintainer script may have on the file system. Our final objective is to use this information for the quality assessment of Debian maintainer scripts.

The technique of symbolic execution consists in following all the possible execution paths of a script, while recording in a symbolic form the interaction with the file system. The symbolic form (technically a formula in some logical formalism) describes the modification of the file system performed by the script on any initial file hierarchy. For the moment we have used these symbolic descriptions to extract cases in which a script may fail. Plans for future work include analyzing the symbolic descriptions in order to decide properties like idempotency of scripts, or relations between scripts like that their order of execution is independent, or that one script undoes the effect of an other script.

Our analysis applies to an abstraction of *nix file systems, and also abstracts away from some aspects of scripts, in particular from tools that operate on the contents of files. Despite these limitations we have already some first interesting results. It is important to remember, however, that a possible error case detected by our tool is not automatically a bug, not only because of possible false positives of our tool, but also because it may be the right decision of a maintainer to make their script fail in case it encounters a situation it cannot cope with. We hope to have some discussion with the audience about how one can decide whether a failure is a bug or not.

This work is part of the ongoing CoLiS project which aims at applying formal methods to the quality assessment of Debian maintainer scripts. Previous results on the syntactic analysis of maintainer scripts had been presented at Debconf18.

This is joint work with Benedikt Becker, Claude Marché, Mihaela Sighireanu and Yann Regis-Gianas from our research teams in Saclay and Paris.