Linux Packages and Tree Transducers
Abstract
This project deals with verification of install and uninstall scripts for Linux distributions. We aim at formalizing scripts by tree tranduscers in order to verify static properties during their activity. For instance, we aim at checking whether the composition of the install and the uninstall script is equivalent to identity.
Key Words : Tree Transducers, Linux
Team : Links (CRIStAL/INRIA Lille)
Supervisors
Prerequisite
- Finite State Automata
- Tree Automata
Localisation
INRIA Lille
Parc scientifique de la Haute Borne – Villeneuve d’Ascq
Context
Linux distributions perform installation of softwares by a system of packages that create directories, create files, modify config files, … When a file system evolve during time, the number of softwares which are installed and desinstalled increase considerably, in particular from the constant update of the various programs installed on it. When this process is not perfect, that can cause many problems, from the creation of files that become useless and slow down the system or occupy disk space, to the destruction of important files and the various bugs that can occur.
In order to avoid those situation, we need to model the behavior of the scripts. In particular, we see scripts as process that modify the tree structure of the file system. If we manage to define a model of finite state machine that can perform transformation which are expressive enough to describe install scripts, and which is adapted to static analysis technics, it become possible to verify automatically that those programs maintain the consistency of file systems.
Problems
Among models of finite state machines that can perform transformations, one the most studid are tree transducers. There are several good reasons for this. First, they extend finite state automata to describe trasnsformations. They also have several variant that can include for instance the usage of registers to deal with data values. They also have strong theoretical links with logic formalisms that make them suitable with many analysis technics.
The objective of this project is to study classes of tree transducers in order to establish a class which is adapted to package management. We aim at sstudying to which extent analysis methodes can be applied to those models. In particular, we will aim at studying the problem of equivalence of tree transudcers. Indeed, one of our main objective is to study whether the composition of an install script and its associated uninstall script correspond to the identity. Such an algorithm could also verify that the isntallation of a two package followed by the uninstall of the first package correspond to the sole installation of the second package.
Tasks
During this project, the student will study a specific class of tree transducer which is linked to monadic second order logic which is close to a model proposed in the literature. We need to:
- this class can indeed model correctly scripts,
- clearly establish the link between this class of machine and logic transformations,
- study some formal properties of this class, such as the closure by composition.
Bibliography
[1] Rajeev Alur, Loris D’Antoni: Streaming Tree Transducers. ICALP (2) 2012: 42-53
[2] Bruno Courcelle: Monadic Second-Order Definable Graph Transductions: A Survey. Theor. Comput. Sci. 126(1): 53-75 (1994)
[3] Joost Engelfriet, Sebastian Maneth: The Equivalence Problem for Deterministic MSO Tree Transducers Is Decidable. FSTTCS 2005: 495-504
[4] Joost Engelfriet, Sebastian Maneth: Characterizing and Deciding MSO-Definability of Macro Tree Transductions. STACS 2000: 542-554
