Assurer la sécurité informatique des infrastructures numériques est un enjeu crucial. Un des points clés est de s’assurer que le logiciel ne contient pas de faille exploitable. Les techniques de vérification automatique de programme, initialement développées pour assurer la sûreté, sont depuis peu adaptées aux besoins de la sécurité. Le problème est que, si ces méthodes permettent effectivement de trouver des bugs, ceux-ci ne sont pas forcément pertinents en termes de sécurité (pas exploitables).
Sujet proposé : Le thème général du stage est l’analyse de l’exploitabilité d’un bug, à partir d’une trace menant à ce bug. Nous nous situons dans le cadre où un bug a déjà été découvert (par fuzzing, remontée utilisateur ou autre) et où une trace (suite d’instructions assembleur) menant au bug est disponible. Nous supposons que cette trace ne permet pas d’exploiter directement le bug.
Le but est de développer des méthodes automatiques pour classifier " l’exploitabilité ’’ du bug découvert, en utilisant des techniques de vérification automatique pour essayer de ``généraliser’’ la trace initiale en une trace effectivement exploitable.
Le candidat devra dans un premier temps comprendre et s’approprier les travaux existants Heelan-09,MCJGMPS-10, essentiellement basés sur l’exécution symbolique, l’utilisation de solveurs SMT KS-08 et la modélisation formelle du code bas niveau BHLOTV-11.
Une fois ces bases maitrisées, le candidat devra étendre l’approche, par exemple en proposant de nouveaux modèles d’exploitabilité ou en améliorant la méthode de généralisation. Les résultats seront implantés dans un prototype existant JB-14.
Références :
BHLOTV-11 Bardin, S., Herrmann, P., Leroux, J., Ly, O., Tabary, R., Vincent, A.: The BINCOA Framework for Binary Code Analysis. In: CAV 2011. Springer, Heidelberg (2011)
Heelan-09 Heelan, S.: Automatic generation of control-flow hijacking exploits for software vulnerabilities. Msc. dissertation, University of Owford, 2009
JB-14 Jeanne, G., Bardin, S.: Génération automatique d’exploits à partir de traces d’erreurs. Technical report, CEA LIST, 2014
KS-08 Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, 2008.
MCJGMPS-10 Miller, C., Caballero, J., Johnson, N., Gyunng Kang, M., McCamant, S., Poosankam, P., Song, D.: Crash Analysis with BitBlaze. In: BlackHat 2010.
