Towards the formal verification of maintainer scripts

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.

• Slides