Offre de thèse : Symbolic execution for deobfuscation, and application to malware analysis

Equipes : Carbone (LORIA) et CEA

Encadrement et contact : Sébastien Bardin (CEA sebastien.bardin at cea.fr), Jean-Yves Marion (LORIA Jean-Yves.Marion at loria.fr)

Lieu : CEA (Paris-Saclay) avec visites au LORIA (Nancy)

Mots clés : reverse, déobfuscation, malware, désassembage, méthodes formelles, exécution symbolique

La sécurité logicielle est un problème majeur de la société de l’information, les conséquences d’un système non sécurisé pouvant affecter aussi bien des individus (phishing, paiement non autorisé, etc.) que des compagnies (fuite d’informations confidentielles) ou des états (attaques cybernétiques, virus stuxnet). Un des vecteurs d’attaque les plus privilégiés est l’utilisation de codes malveillants (malware), tels que les virus ou les vers [2]. La contre-mesure classique consiste à détecter le malware par des techniques de signature syntaxique [2]  puis à l’éradiquer. Cependant cette approche est très simple à contourner en utilisant des méthodes d’obfuscation (modification automatique d’un programme pour en altérer la forme sans modifier son comportement) [3].

La recherche en matière de détection de malware s’oriente actuellement vers des notions de signatures “sémantiques” plus robustes, voir par exemple les travaux menés au Laboratoire de Haute Sécurité (LHS) du LORIA [1]. Cependant, à cause de l’obfuscation, la signature calculée ne prend en compte qu’une partie du programme malveillant, ce qui entraine des pertes de précision en termes de détection. D’un autre côté, des progrès récents ont été obtenus au Laboratoire de Sécurité Logicielle (LSL) du CEA LIST dans le domaine de l’analyse automatique de code binaire. Ainsi la plate-forme open-source BINSEC [5] fournit une représentation intermédiaire multi-plateforme et différentes analyses sémantiques, permettant notamment l’exploration partielle des comportements du code exécutable ou encore la reconstruction du Graphe de Flot de Contrôle (CFG) d’un programme (non protégé) donné sous forme exécutable.

Nos premiers travaux, en collaboration CEA-LORIA, ont déjà permi l’ajout d’un moteur puissant d’exploration des chemins d’un malware [5] (via *exécution symbolique*), ainsi qu’une première étude de l’utilisation de l’exécution symbolique pour aider à la déobfuscation — notamment via la détection de “prédicats opaques” [6,7]. Le but de ce sujet de thèse est de consolider ces premiers résultats, en explorant de manière systématique l’utilisation de l’exécution symbolique pour la déobfuscation et la reconnaissance de malware. Le candidat devra notamment :

1. Etudier comment  reconstruire des approximations fidèles du CFG de codes exécutables obfusqués, en étendant et/ou combinant les techniques actuelles d’analyse de code binaire. C’est la tâche principale de la thèse. Le candidat devra notamment considérer un spectre large des principales obfuscations de code rencontrées en pratique (automodification, virtualisation, etc.). D’un point de vue technique, la combinaison de techniques d’exécution symbolique, de tracing dynamique (disponible au LORIA) et d’analyse statique niveau binaire (également disponible dans BINSEC) est une piste prometteuse pour attaquer les codes protégés, continuant les efforts déjà entrepris [6,4].

2. Etudier comment connecter ces résultats peuvent se combiner avec les techniques de reconnaissance sémantique de malware du LORIA [1], et en évaluer le gain. Au-delà du bénéfice d’un désassemblage plus précis, on pourra par exemple étudier comment les techniques symboliques d’analyse de binaire [6,7] peuvent être utilisées directement pour calculer des éléments pertinents de signature sémantique, complétant les approches déjà proposées [1].

Références

[1] Bonfante, G., Kaczmarek, M., Marion, J.-Y. : Architecture of a morphological malware
detector. In : Journal in Computer Virology (2009)

[2] Filiol, É. : Les virus informatiques : théorie, pratique et applications. Springer (2004)

[3] Moser, A., Kruegel, C., Kirda, E. : Limits of Static Analysis for Malware Detection. In: Annual Computer Security Applications Conference (ACSAC 2007)

[4] Bonfante, G., Fernandez, J. M., Marion, J.-Y., Rouxel, B., Sabatier, F., Thierry, A.: CoDisasm: Medium Scale Concatic Disassembly of Self-Modifying Binaries with Overlapping Instructions. In: ACM Conference on Computer and Communications Security (CCS 2015)

[5] David, R., Bardin, S., Ta, T. D., Feist, J., Mounier, L., Potet, M.-L., Marion, J.-Y.: BINSEC/SE : A Dynamic Symbolic Execution Toolkit for Binary-level Analysis. In: IEEE International Conference on Software Analysis, Evolution, and Reengineering (SANER 2016)

[6] S. Bardin, R. David, JY Marion. Backward-bounded DSE: Targeting Infeasibility Questions on Obfuscated Codes. In: IEEE Symposium on Security & Privacy (S&P 2017)

[7] R. David, S. Bardin. Code Deobfuscation: Intertwining Dynamic, Static and Symbolic Approaches. In: Black Hat Europe 2016

En ce moment

Logo du CNRS
Logo Inria
Logo Université de Lorraine