salle A. Turing CE4
25 mars 2014 - 15h45
Lazart : une approche symbolique pour évaluer la robustesse d'un code aux attaques par injection de fautes
par Laurent Mounier de VERIMAG
Résumé : Dans le domaine des cartes à puces, il est nécessaire de protéger les equipements contre toutes attaques potentiellement dangereuses pour leur sécurité. Les normes de développement de type Critères Communs exigent d'effectuer des analyses de vulnérabilités prenant en compte les attaques les plus performantes connues à ce jour. Une catégorie très classique d'attaques sont celles basées sur l'injection de fautes, obtenues par exemple en perturbant l'exécution du code à l'aide d'un laser.
Nous proposons une approche globale, baptisée Lazard, permettant d'évaluer la robustesse d'un code à des injections de fautes destinées à perturber son flot d'exécution. L'originalité de Lazart est double.
Tout d'abord cette approche englobe le processus d'évaluation de manière globale : à partir d'un modèle de faute, elle permet de produire (ou de prouver l'absence) d'attaques, en prenant en compte les éventuelles contre-mesures incluses dans le code. De plus, elle s'applique à des combinaisons d'injections multiples de fautes transitoires.
L'approche Lazard a été implémentée sur le format LLVM en utilisant l'outil Klee pour la génération de tests symboliques.
