Ralf Treinen

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.

Other people: Nicolas Jeannerod

Debian sid contains more than 31.000 maintainer scripts, the vast majority of which are written in the POSIX shell language. We have written, in the context of the CoLiS project, the tool shstats which allows us to do a statistical analysis of a large corpus of shell scripts. The tool operates on concrete syntax trees of shell scripts constructed by the morbig shell parser. The morbig parser has already been presented at a devroom at FOSDEM 2018, and at the minidebconf 2018 in Hamburg. The shstats tool comes with a number of analysis modules, and it is easy to extend it by adding new modules. In this talk we will present both the design of the analyzer tool and how it can be extended by new analysis modules, and some of the results we have obtained so far on the corpus of sid maintainer scripts. Among these are answers to questions like: - are recursive functions used in maintainer scripts? - how many variable assignments are in reality definition of constants? - how many shell scripts don't do any variable assignments, besides definitions of constants? - how often are shell constructs like while, for, if, etc. used? - which UNIX commands are most commonly used in the corpus, and with which options? - are there any syntax errors in the arguments of complex commands like test?

Other people: Nicolas Jeannerod

This talk describes a recently started research project named [http://colis.irif.univ-paris-diderot.fr/ Colis] with the goal of developing techniques and tools for the formal verification of maintainer scripts (preinst, postinst, prerm, postrm). *Program verification* aims at obtaining a formal assurance that a program is correct with respect to a given specification. This is achieved by constructing a formal proof of correctness of the program. In contrast to *program testing*, the existence of a proof assures that the program behaves correctly in *any* situation described by the specification. Failure of an attempt to verify a program, on the other hand, can often be used to generate useful test cases. A possible example of a program specification is absence of execution error under certain initial conditions. Automatic program verification even for this kind of specification is an extremely challenging task. In case of Debian maintainer scripts we are faced with even more challenging properties like idempotency of scripts (required by policy), or commutation of scripts. The project is still in the beginning, so there are no results yet to present. However, I will explain why I think that the case of Debian maintainer scripts is very interesting for program verification : some aspects of scripts (POSIX shell, manipulation of a complex data structure) make the problem very difficult, while other aspects of the Debian case are likely to make the problem easier. I am also very interested in the inputs from the audience about possible use cases of script verification in the context of Debian.