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.
Talk (45 mins) session with Ralf Treinen during Debconf 16