Thèse de Valentin Lefils

Vérification externalisée du flot de contrôle : Comment adapter la sécurité système à l'informatique embarquée

Les systèmes embarqués sont utilisés pour accomplir des tâches critiques dans les systèmes industriels, l'automobile ou l’aéronautique. Pourtant, beaucoup d’entre eux possèdent une faible sécurité matérielle et logicielle. Par exemple, de nombreuses attaques (dépassement de tampon, injection de faute, etc…) visent à modifier le comportement du logiciel embarqué et mener à une exécution de code arbitraire. Une solution à ce problème est la mise en place d'une politique de vérification de l’intégrité du flot de contrôle (Control Flow Integrity ou CFI) qui vérifie en temps réel le comportement du programme par rapport à l'exécution attendue. Mais une telle solution ne correspond pas en l'état aux contraintes de l'informatique embarquée car elle est coûteuse en terme de temps de calcul. Dans la première partie de cette thèse j'évalue la pertinence d'une solution externalisée de CFI pour les systèmes embarqués. Celle-ci repose sur l'instrumentation du code source à protéger afin de produire, lors de l'exécution, une trace envoyée à un moniteur externe qui vérifie si elle est en accord avec un graphe de flot de contrôle extrait à la compilation. J'ai évalué la faisabilité de la démarche en démontrant qu'elle était pertinente vis à vis des systèmes embarqués. La deuxième partie de mes travaux concerne la vérification du flot de contrôle. Les solutions de CFI classiques reposent sur une analyse du code source afin de créer un modèle de référence pour la vérification de l'exécution. Mais de nombreuses études ont démontré les faiblesses de ce modèle car il est difficile de prédire avec précision le comportement du programme. Pour résoudre ce problème, j'ai proposé une solution basée sur l'apprentissage automatique afin de passer d'un modèle de prédiction du comportement à un modèle de déduction du comportement. Cette solution repose sur la mise en place d'un algorithme d'apprentissage capable d'induire un modèle précis à partir de traces réelles d'exécution. Afin de valider cette démarche, l'efficacité du mécanisme d'apprentissage ainsi que la validité et la précision du nouveau modèle sont évalués. Finalement, ces travaux incluent le résultat des expériences menées sur cette nouvelle approche ainsi que des pistes de recherche pour des travaux futurs.

Jury

Rapporteurs : M. Pierre PARADINAS, CNAM Paris Mme Vania MARANGOZOVA-MARTIN, Université de Grenoble Examinateur : M. Didier DONSEZ, Université de Grenoble 1 Directeur de Thèse : M. Gilles GRIMAUD, Université de Lille Co-Directeur de Thèse : M. Julien CARTIGNY, Université de Lille Invité : M. Frédéric MAJORCZYK, DGA-MI

Thèse de l'équipe 2XS soutenue le 26/06/2019