Description
Date depot: 1 janvier 1900
Titre: Combinaisons de domaines abstraits pour une analyse statique efficace et précise
Directeur de thèse:
Emmanuel CHAILLOUX (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
De taille et complexité croissante, les logiciels embarqués sont de
plus en plus difficiles à vérifier. Les activités de test et relecture
constituent plus de 50% du cycle complet de développement. Néanmoins,
garantir le fonctionnement correct de logiciels embarqués est d'autant
plus important que la tendance à les connecter au sein de réseaux
s'accentue. Ainsi, non seulement, une erreur de programmation peut
entraîner un dysfonctionnement dans des conditions imprévues; mais de
plus un attaquant peut s'efforcer de générer sciemment de telles
conditions afin de prendre le contrôle du logiciel.
L'analyse statique permet en théorie de démontrer automatiquement et
avant son utilisation qu'un programme s'exécutera toujours
correctement. Très schématiquement, un outil d'analyse statique conçu
par interprétation abstraite se compose des éléments suivants :
1. un domaine abstrait, c'est-à-dire une structure de données qui
représente de façon finie et approchée les ensembles d'états de la
mémoire du programme;
2. un algorithme de résolution qui calcule une approximation
supérieure de l'ensemble des comportements possibles du programme à
l'aide du domaine abstrait.
La conception du domaine abstrait est un élément déterminant à la fois
dans la précision des résultats et l'efficacité de l'outil. Pour cela
des domaines abstraits <<élémentaires>> numériques ou symboliques
doivent être assemblés judicieusement afin de capturer les divers
aspects du modèle de la mémoire.
L'objectif de cette thèse est d'étudier les combinaisons de domaines
abstraits élémentaires afin d'obtenir des abstractions de la mémoire à
la fois efficaces et précises sur cas d'études industriels provenant de l'embarqué aéronautique et spatial. Ces combinaisons de domaines
autorisent alors le passage à l'échelle qui permet des analyses plus
précises sur des programmes plus importants. La validation de cette
démarche passera par la réalisation d'un prototype.
Doctorant.e: Millon Etienne