[Caml-list] [sujet de thèse] déobfuscation et analyse de malware (CEA-LORIA, deadline 15 mai)

[Caml-list] [sujet de thèse] déobfuscation et analyse de malware (CEA-LORIA, deadline 15 mai)

[sebastien bardin]

Le CEA Saclay propose un sujet de thèse sur l'utilisation des méthodes
formelles pour l'analyse de malware et de programmes obfusqués, en
co-encadrement avec le LORIA (Jean-Yves Marion).


deadline : 15 mai
contact : sebastien.bardin@cea.fr




------------------------------------------------

titre : Symbolic execution for deobfuscation, and application to malware
analysis


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


- bourse DGA-CEA, co-encadrement CEA-Université de Lorraine
- lieu : CEA (Paris-Saclay), avec visites au LORIA (Nancy)
- encadrants : Sébastien Bardin (CEA),
	      Jean-Yves Marion (LORIA, directeur de thèse)
- démarrage en octobre 2017
- deadline pour répondre : 15 mai

- contact, plus d'information : sebastien.bardin@cea.fr




sujet
-----

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 entraîne
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à permis
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

[Caml-list] [sujet de thèse] déobfuscation et analyse de malware (CEA-LORIA, deadline 15 mai)

[sebastien bardin]

Le CEA Saclay propose un sujet de thèse sur l'utilisation des méthodes
formelles pour l'analyse de malware et de programmes obfusqués, en
co-encadrement avec le LORIA (Jean-Yves Marion).


deadline : 15 mai
contact : sebastien.bardin@cea.fr




------------------------------------------------

titre : Symbolic execution for deobfuscation, and application to malware
analysis


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


- bourse DGA-CEA, co-encadrement CEA-Université de Lorraine
- lieu : CEA (Paris-Saclay), avec visites au LORIA (Nancy)
- encadrants : Sébastien Bardin (CEA),
	      Jean-Yves Marion (LORIA, directeur de thèse)
- démarrage en octobre 2017
- deadline pour répondre : 15 mai

- contact, plus d'information : sebastien.bardin@cea.fr




sujet
-----

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 entraîne
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à permis
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