Verified Static Analyses for Low-Level Languages

Vincent Laporte

project-team CELTIQUE

PhD's defense- Wednesday 25th november 2015
The talk [40:31 mn] Download file(MP4)

 

Les membres du Jury:

Anders Møller, Associate Professor Aarhus University, Danemark, rapporteur
Greg Morissett, Professor at Cornell University, USA, rapporteur
Marie-Laure Potet, Professeur à INP/Ensimag, examinatrice
Xavier Leroy, DR Inria Rocquencourt, examinateur
Antoine Miné, Professeur à l'Université Pierre et Marie Curie (Paris 6), examinateur
Sandrine Blazy, Professeur à l'Université de Rennes 1, co-directrice de thèse
David Pichardie, Professeur à l'ENS Rennes, co-directeur de thèse

Résumé:

L’analyse statique des programmes permet d’étudier les comportements possibles des programmes sans les exécuter. Les analyseurs statiques sont employés par exemple pour garantir que l’exécution d’un programme ne peut pas produire d’erreurs. Ces outils d’analyse étant eux-mêmes des programmes, ils peuvent être incorrects. Pour accroitre la confiance que l’on peut accorder aux résultats d’une telle analyse, nous étudions dans cette thèse comment on peut formellement établir la correction de l’implantation d’un tel analyseur statique.

En particulier, nous construisons au moyen de l’assistant à la preuve Coq des interpréteurs abstraits et prouvons qu’ils sont corrects; c’est-à-dire nous établissons formellement que le résultat de l’analyse d’un programme caractérise bien toutes les exécutions possibles de ce programme. Ces interpréteurs abstraits s’intègrent, dans la mesure du possible, au compilateur vérifié CompCert, ce qui permet de garantir que les propriétés de sûreté prouvées sur le code source d’un programme sont aussi valides pour la version compilée de ce programme.

Nous nous concentrons sur l’analyse de programmes écrits dans des langages de bas niveau. C’est-à-dire des langages qui ne fournissent que peu d’abstractions (variables, fonctions, objets, types…) ou des abstractions que le programmeur a loisir de briser. Cela complexifie la tâche d’un analyseur qui ne peut pas s’appuyer sur ces abstractions pour être précis. Nous présentons notamment comment reconstruire automatiquement le graphe de flot de contrôle de programmes binaires auto-modifiants et comment prouver automatiquement qu’un programme écrit en C (où l’arithmétique de pointeurs est omniprésente) ne peut pas produire d’erreurs à l’exécution.