Doctorat
Equipe : Toccata
Certification d'une chaine de vérification déductive de programmes
Début le 01/10/2009
Direction : MARCHÉ, Claude
[Benjamin MONATE]
Ecole doctorale :
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI INRIA
Soutenue le 14/01/2013 devant le jury composé de :
Xavier Leroy, Inria Rocquencourt
Gilles Barthe, IMDEA Software Institute
Roberto Di Cosmo, Laboratoire PPS, Université Paris Diderot 7
Emmanuel Ledinot, Dassault Aviation
Burkhart Wolff, LRI Université Paris-Sud 11
Claude Marché, Inria Saclay - Île-de-France
Benjamin Monate, CEA-LIST, Lab. de Sûreté du Logiciel
Activités de recherche :
Résumé :
Cette thèse s'inscrit dans le domaine de la vérification du logiciel. Le but de
la vérification du logiciel est d'assurer qu'une implémentation, un programme,
répond aux exigences, satisfait sa spécification. Cela est particulièrement
important pour le logiciel critique, tel que des systèmes de contrôle
d'avions, trains ou centrales électriques, où un mauvais fonctionnement
pendant l'opération aurait des conséquences catastrophiques.
Les exigences du logiciel peuvent concerner la sûreté ou le fonctionnement.
Les exigences de sûreté, tel que l'absence d'accès à la mémoire en dehors des
bornes valides, sont souvent implicites, dans le sens que toute implémentation
est censée être sûre. Beaucoup de langages de programmation de haut niveau
garantissent les principales exigences de sûreté en fournissant au programmeur
une abstraction de la machine qui interdit les opérations non sûres. Par
contre, les langages de bas niveau, comme le langage C, accordent au
programmeur l'accès total à la machine tout en l'exposant à la totalité des
risques. Malheureusement, l'usage de langages de bas niveau ne peut souvent
pas être évité -- particulièrement dans les implémentations desdits systèmes
de contrôle. En effet, le langage C reste aujourd'hui le langage de choix pour
le développement du logiciel embarqué critique.
D'autre part, les exigences fonctionnelles spécifient ce que le programme est
censé faire. La spécification d'un programme est souvent exprimée
informellement en décrivant en anglais ou en une autre langue naturelle la
mission d'une partie du code source. La vérification du programme se fait alors
habituellement par relecture manuelle, simulation et tests approfondis. Par
contre, ces méthodes ne garantissent pas que tous les possibles cas
d'exécution sont capturés. Il peut y avoir une rare séquence d'événements à
laquelle le programmeur n'avait pas pensé et avec laquelle il omet donc de
tester son programme.
La preuve déductive de programme est une méthode complète pour assurer la
correction du programme. Ici, un programme, ainsi que sa spécification
formalisée à l'aide d'un langage logique, est un objet mathématique et ses
propriétés désirées sont des théorèmes logiques à prouver formellement. De
cette façon, si le système logique sous-jacent est cohérent, on peut être
complètement sûr que la propriété prouvée est valide pour le programme en
question et pour n'importe quel cas d'exécution.
La génération de conditions de vérification est une technique censée aider le
programmeur à prouver les propriétés qu'il veut sur son programme. Ici, un
outil (VCG) analyse un programme donné avec sa spécification et produit une
formule mathématique, dont la validité implique la correction du programme vis
à vis de sa spécification, ce qui est particulièrement intéressant lorsque les
formules générées peuvent être prouvées automatiquement à l'aide de solveurs
SMT.
Cette approche, basée sur des travaux de Hoare et Dijkstra, est bien comprise
et prouvée correcte en théorie. Des outils de vérification déductive ont
aujourd'hui acquis une maturité qui leur permet d'être appliqués dans un
contexte industriel où un haut niveau d'assurance est requis. Mais leurs
implémentations doivent gérer toute sorte de fonctionnalités des langages et
peuvent donc devenir très complexes et contenir des erreurs elles mêmes -- au
pire des cas affirmer qu'un programme est correct alors qu'il ne l'est pas. Il
se pose donc la question du niveau de confiance accordée à ces outils.
Le but de cette thèse est de répondre à cette question. On développe et
certifie, dans le système Coq, un VCG pour des programmes C annotés avec ACSL,
le langage logique pour la spécification de programmes ANSI/ISO C. Notre
première contribution est la formalisation d'un VCG exécutable pour le langage
intermédiaire Whycert, un langage impératif avec boucles, exceptions et
fonctions récursives, ainsi que sa preuve de correction par rapport à la
sémantique opérationnelle bloquante à grand pas du langage. Une deuxième
contribution est la formalisation du langage logique ACSL et la sémantique des
annotations ACSL dans Clight de Compcert. De la compilation de programmes C
annotés vers des programmes Whycert et sa preuve de préservation de la
sémantique combiné avec une axiomatisation en Whycert du modèle mémoire
Compcert résulte notre contribution principale: une chaîne intégrée certifiée
pour la vérification de programmes C, basée sur Compcert. En combinant notre
résultat de correction avec celui de Compcert, on obtient un théorème en Coq
qui met en relation la validité des l'obligations de preuve générées avec la
sûreté du code assembleur compilé.
