Ralf Treinen
https://www.irif.univ-paris-diderot.fr/~treinen/
Ralf Treinen is a debian developer since 2000. He has been active in
maintaining packages (mostly in the context of the OCaml packaging
team), as an application manager, and more recently in debian quality
assurance.
In his spare time, Ralf is working as professor for computer science
at University Paris-Diderot, where he teaches various courses from
theory to practice. His research activities are centered around formal
methods; recently he has participated in the EDOS and Mancoosi
projects on applying formal methods to the quality assurance of FOSS
distributions.
Accepted Talks:
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.