Correction de scripts Linux – Colis

Le projet CoLiS a pour but d'appliquer des techniques de vérification
déductive et d'analyse de transformations d'arbres sur le problème de
l'analyse des scripts shell, en particulier ceux utilisés dans les
installations de paquetages logiciels. En effet, ces scripts jouent un
rôle majeur dans l'installation des machines UNIX, ainsi que dans les
tâches récurrentes de configuration, d'installation et de
maintenance. Les scripts interagissent avec l'état courant du système
d'exploitation, en particulier à travers le système de fichiers.

Des erreurs dans les scripts peuvent avoir des conséquences graves car
ils sont exécutés à des instants cruciaux, comme la mise à jour des
paquetages installés. Ces scripts doivent fonctionner correctement
dans des situations qui n'ont probablement pas été prévues par
l'auteur du script. Par exemple, un script d'installation doit
fonctionner indépendemment du choix des autres paquetages installés,
ainsi que dans les situations anormales comme lorsque que
l'administrateur relance une opération qui a été précédemment
interrompue.

Nous avons identifié trois défis principaux :

1) Le premier est le langage de programmation. Les langages de script
sont Turing-complets, et ont typiquement des traits impératifs :
diverses sortes de boucles, affectations de variables, fonctions
récursives. Ces langages étant fréquemment utilisés pour interagir
avec le système d'exploitation, ils fournissent des moyens simples
d'exécuter des commandes UNIX. Néanmoins, leur modèle d'exécution est
hautement dynamique, basé sur la combinaison d'expansion
(p.ex. expansion de variable), d'évaluation et d'exécution de
commandes système. Ils se placent à l'intermédiaire entre les langages
par macro-expansion et les langages de programmation classiques.

2) La structure de données manipulée par ces scripts est complexe : le
système de fichiers. Notre approche est de le considérer tel que vu
par le programmeur de script, comme une structure d'arbre,
indépendemment de la façon dont il est implémenté. Néanmoins, nous
devrons gérer des traits complexes comme l'absence de bornes en
largeur et en profondeur, la présence de liens multiples sur les
feuilles, les liens symboliques, les permissions d'accès.

3) Les propriétés qui nous intéressent sont variées dans leur
complexité. Une propriété simple typique est qu'un script n'est
autorisé à modifier que certaines parties bien identifiées du système
de fichiers. Les propriétés complexes concernant les séquences
d'exécution possibles de plusieurs scripts, comme l'exécution d'un
script d'installation puis d'un script de désinstallation, ou une
exécution réitérée d'un script après un premier échec.

À la fin du projet nous voulons proposer des outils qui analyseront
formellement les scripts, établiront leur correction, ou bien
signaleront des erreurs. C'est un objectif ambitieux, nous auront
probablement à faire des compromis, des hypothèses sur la structure
des scripts, et des approximations sur le système de fichiers et
l'exécution des commandes. Ces compromis seront guidés par des
études de cas sur la distribution GNU/Linux Debian.

Nous commencerons par développer des modèles formels du langage de
script et de la structure du système de fichiers, ainsi qu'un langage
pour spécifier les propriétés attendues. Nous suivrons deux approches
connues de méthode formelle : l'une basée sur les transducteurs
d'arbres (comme les arbres XML), l'autre basée sur les techniques de
preuve de programmes, avec l'environnement Why3. Nous chercherons
également à faire coopérer ces deux technologies.