Les méthodes actuelles d’analyse de programmes pour la sécurité simulent des attaquants faibles, seulement capables de fournir aux programmes des données malicieuses. Un attaquant puissant accède à d’autres vecteurs d’attaque tels que :
mais aussi, les attaques par injection de fautes induites par le logiciel (ex. : rowHammer) ou exploitant des mécanismes micro-architecturaux dans le processeur, deux vecteurs d’attaque dont le contexte d’application est bien plus large.
La notion usuelle d’atteignabilité (la recherche dans le programme d’un chemin qui atteint un certain état du système) ne permet pas de représenter cet attaquant puissant. Notre premier défi est de concevoir un environnement pour raisonner automatiquement et efficacement sur l’impact d’un attaquant puissant sur un programme. Notre second défi est de concevoir un algorithme efficace pour déterminer la vulnérabilité d’un programme à un modèle d’attaquant donné, sans explosion combinatoire, en particulier en cas d’attaques multiples. Les techniques existantes ne passent pas à l’échelle et ne fournissent pas de formalisation du problème sous-jacent.
Nous proposons un algorithme original, l’Exécution Symbolique Adversariale (ASE), étendant l’exécution symbolique (utilisée pour l’analyse de code standard) et la notion d’atteignabilité usuelle pour permettre l’analyse des chemins d’exécution d’un programme en présence d’un attaquant puissant. L’explosion combinatoire est évitée grâce à une nouvelle technique d’injection de vulnérabilités dite «Forkless», sans créer de chemin supplémentaire à explorer, contrairement aux techniques de l’état de l’art. Nous avons implémenté cet algorithme dans la plateforme BINSEC, sous la forme d’un outil appelé BINSEC/ASE. Les expérimentations faites avec BINSEC ont montré un gain important en performance, en termes de temps d’analyse et de nombre de chemins explorés.
