2018-00533 - Spécialisation d’un moteur d’exécution concolique pour l’analyse de programmes obfusqués

Type de contrat : CDD de la fonction publique

Niveau de diplôme exigé : Bac + 5 ou équivalent

Fonction : Doctorant

A propos du centre ou de la direction fonctionnelle

Le centre Inria Rennes - Bretagne Atlantique est un des huit centres d’Inria et compte plus d'une trentaine d’équipes de recherche. Le centre Inria est un acteur majeur et reconnu dans le domaine des sciences numériques. Il est au cœur d'un riche écosystème de R&D et d’innovation : PME fortement innovantes, grands groupes industriels, pôles de compétitivité, acteurs de la recherche et de l’enseignement supérieur, laboratoires d'excellence, institut de recherche technologique.

Contexte et atouts du poste

Travail sur analyse de malwares avec une équipe de recherche dynamique et en lien avec l'entreprise Cisco. 

La détection de programmes malveillants, ou malwares, est une tâche fondamentale pour garantir la sécurité d’un système informatique. Ce traitement se fait généralement au moyen d’anti-virus qui ont pour but de détecter/bloquer l’exécution de programmes malveillants voir même de réparer les dommages qu’ils ont causé. Malheureusement, les anti-virus, largement basés sur des analyses syntaxiques des instructions du programme, sont de plus en plus mis en échec par les créateurs de malwares. En fait, il est assez facile de flouer un anti-virus en modifiant la signature syntaxique du malware sans en changer la sémantique. Parmi les techniques qui permettent d’atteindre cet objectif, on trouve l’obfuscation de code qui a pour but de complexifier la compréhension du code en y ajoutant, par exemple, des chemins non atteignables ou en transformant des conditions de branchements simples en conditions complexes [Ore13, BGI+01, Gar14, GGH+13, BGG18]. Pour ce faire, on utilise des prédicats dits opaques [CTL97]. Ce sont des expressions qui peuvent dépendre du contexte d’exécution et dont l’évaluation reste binaire, mais pour lesquels il est difficile de deviner l’ensemble des solutions possibles sans les énumérer [UDM05]. Cela se traduit par une explosion du nombre de tests à réaliser. Afin d’énumérer et de représenter efficacement ces solutions, nous suggérons d’utiliser des solveurs de contraintes et des méthodes de synthèse dynamique. Nous avons montré l’efficacité de cette approche sur des prédicats obtenus à partir de formules de l’algèbre Booléenne mixte [BJLS17]. Le premier objectif de cette thèse est de voir si notre approche se généralise à d’autres types de prédicats qu’il faudra classifier. Le second objectif est l’évaluation des résultat obtenus par intégration dans un outil d’analyse développé au sein de l’équipe Tamis.

 

 

Mission confiée

Objectifs principaux

Cette thèse a pour objet de tester la résistance de certaines transformations d’obfuscation vis-à-vis des solveurs de contraintes. La présente étude se propose de spécialiser un moteur d’analyse symbolique, en améliorant l’efficacité d’un solveur de contraintes, dans le cadre de l’exploration de multiples chemins d’exécution d’un programme obfusqué. Dans un premier temps, cela se traduit par les axes de recherche suivants:

• Améliorer la détection et l’extraction des prédicats opaques du code binaire. Cela nécessite de bien de distinguer un fragment de code obfusqué de façon malveillante dans le but d’empêcher l’analyse d’un code exécutable légitime mais complexe.

• Développer de nouveaux algorithmes, méthodes heuristiques, et techniques simplifiant la manipulation des prédicats opaques afin de rendre possible leur résolution par solveurs de contraintes.

• Explorer d’autres techniques que les solveurs. Cela inclut par exemple la synthèse dynamique, l’exploration exhaustive de l’espace d’entrée (ou attaque par force brute) et la simplification algébrique.

Il existe des prédicats dont la résolution dépend du contexte d’exécution. Il est donc très important de lier l’analyse du prédicat à la technique utilisée pour explorer les exécutions du programme. Dans Tamis nous utilisons l’exécution symbolique [BCD+16] qui permet de tester le programme pour plusieurs valeurs des variables en même temps. Son utilisation en association avec des tests concrets (on parle alors d’exécution concolique, c’est-à-dire à la fois concrète et symbolique) permet d’obtenir une exploration plus large des chemins d’exécution. Dans un second temps, il faudra intégrer tout ce qui précède dans un moteur d’exécution concolique développé par l’équipe Tamis. Le but étant de prouver l’efficacité des méthodes développées sur l’analyse de malwares obfusqués. 

Positionnement et originalité

La recherche sur la désobfuscation a tendance à se focaliser sur la suppression de propriétés spécifiques avec des outils ciblés, et souvent non publiés [YJWD15,MXWW15]. D’un autre côté, les moteurs d’analyse symbolique et concolique supposent que les binaires ne sont pas obfusqués [SWS+16] ou que le code source des programmes est disponible [CDE08]. Alors que les techniques d’obfuscation et d’exécution concolique ont été analysées séparément, il n’existe pas aujourd’hui de moteur d’analyse concolique intégrant des techniques spécifiques pour lutter contre l’obfuscation, réduisant ainsi l’efficacité de ces outils face à des programmes malveillants obfusqués. La concrétisation de cette thèse sera de stimuler de manière efficace la recherche sur les malwares en étudiant et en mettant en œuvre des techniques et des outils de désobfuscation intégrés ayant un impact pratique et immédiat pour les analystes de malwares et les programmes anti-virus.

Verrous

Nous avons identifié deux verrous, l’un théorique et l’autre sur l’implémentation et l’intégration dans un outil.

• La désobfuscation est connue comme étant un problème difficile à aborder en pratique, en particulier lorsque les programmes obfusqués utilisent certaines techniques de prédicat opaque basées sur des fonctions de hachage cryptographiques. Il serait irréaliste de promettre une technique capable de casser n’importe quel prédicat opaque. Dans cette thèse, nous identifierons des classes de prédicats dans les cas d’études fournis par nos partenaires industriels. Nous nous concentrerons ensuite sur la résolution des plus pertinents.

• L’intégration de la désobfuscation dans les outils développés/utilisés par Tamis doit tenir compte des limitations des outils eux-mêmes. Une des difficultés du projet sera d’intégrer nos résultats dans un moteur concolique qui couvre un grand nombre d’architectures différentes. Critères d’objectivation de la qualité des résultats Nous avons un double objectif. Le premier est académique et consiste à publier dans les meilleures conférences du domaine (par exemple, IEEE S&P, USENIX Security, ACM CCS, NDSS, DIMVA). Le second est la comparaison d’efficacité de notre outil d’analyse de malwares, avant et après l’intégration des techniques développées dans la thèse.

Bibliographie

[BCD+16] Roberto Baldoni, Emilio Coppa, Daniele Cono D’Elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. arXiv preprint arXiv:1610.00502, 2016.

[BGG18] Roberto Bruni, Roberto Giacobazzi, and Roberta Gori. Code obfuscation against abstract model checking attacks. In Isil Dillig and Jens Palsberg, editors, Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, volume 10747 of Lecture Notes in Computer Science, pages 94–115. Springer, 2018.

[BGI+01] Boaz Barak, Oded Goldreich, Russell Impagliazzo, Steven Rudich, Amit Sahai, Salil P. Vadhan, and Ke Yang. On the (im)possibility of obfuscating programs. In Joe Kilian, editor, Advances in Cryptology - CRYPTO 2001, 21st Annual International Cryptology Conference, Santa Barbara, California, USA, August 19-23, 2001, Proceedings, volume 2139 of Lecture Notes in Computer Science, pages 1–18. Springer, 2001.

[BJLS17] Fabrizio Biondi, Sébastien Josse, Axel Legay, and Thomas Sirvent. Effectiveness of synthesis in concolic deobfuscation. Computers & Security, 70:500–515, 2017.

[CDE08] Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI’08, pages 209–224, Berkeley, CA, USA, 2008. USENIX Association.

[CTL97] Christian Collberg, Clark Thomborson, and Douglas Low. A taxonomy of obfuscating transformations. Technical report, Department of Computer Science, The University of Auckland, New Zealand, 1997.

[Gar14] Sanjam Garg. Program obfuscation via multilinear maps. In Michel Abdalla and Roberto De Prisco, editors, Security and Cryptography for Networks - 9th International Conference, SCN 2014, Amalfi, Italy, September 3-5, 2014. Proceedings, volume 8642 of Lecture Notes in Computer Science, pages 91–94. Springer, 2014.

[GGH+13] Sanjam Garg, Craig Gentry, Shai Halevi, Mariana Raykova, Amit Sahai, and Brent Waters. Candidate indistinguishability obfuscation and functional encryption for all circuits. IACR Cryptology ePrint Archive, 2013:451, 2013.

[MXWW15] Jiang Ming, Dongpeng Xu, Li Wang, and Dinghao Wu. LOOP: logic-oriented opaque predicate detection in obfuscated binary code. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, Denver, CO, USA, October 12-6, 2015, pages 757–768, 2015.

[Ore13] Oreans Technologies. Themida: Advanced windows software protection system. www.oreans.com/ themida.php, 2013.

[SWS+16] Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Audrey Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna. SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis. In IEEE Symposium on Security and Privacy, 2016.

[UDM05] S.K. Udupa, S.K. Debray, and M. Madou. Deobfuscation: reverse engineering obfuscated code. In Reverse Engineering, 12th Working Conference on, pages 10 pp.–, Nov 2005.

[YJWD15] B. Yadegari, B. Johannesmeyer, B. Whitely, and S. Debray. A generic approach to automatic deobfuscation of executable code. In 2015 IEEE Symposium on Security and Privacy, pages 674–691, May 2015.

Principales activités

Programmation

Recherche théorique

Ecriture d'articles scientifiques (et rapports) 

Compétences

Anglais (langue de travail)

Français est un plus

Langage C, python, assemblage

Représentations par modèles

Bon niveau en logique mathématique

 

Avantages sociaux

  • Restauration subventionnée
  • Transports publics remboursés partiellement
  • Installations sportives

Rémunération

A partir de 1982 euros brut (1ère et seconde année) puis 2085 euros brut (3ème année).