< Retour au sommaire

Soutenance de thèse de Grégoire Menguy

Titre: Analyse en boîte noire pour la rétro-ingénierie via acquisition de contraintes et synthèse de code

le

Lieu: Amphi 33/34

Résumé

Les logiciels deviennent de plus en plus grands et complexes. Ainsi, certaines tâches, pourtant cruciales, telles que le test et la vérification de code ou plus généralement la compréhension de code, sont de plus en plus difficiles à réaliser pour un humain. D’où la nécessité de développer des outils d’analyse de code automatiques. L’analyse de code automatique permet de prouver des propriétés sur le code, comme la correction ou l’incorrection. Plus généralement, cela permet de mieux comprendre les programmes. Ces méthodes sont usuellement en boîte blanche, i.e., elles utilisent la syntaxe du code pour déduire ses propriétés via des raisonnements logiques. Elles sont très efficaces mais présentend, néanmoins, certaines limitations: elles nécessitent le code source, elles sont sensilbe à la complexité syntaxique du code. Cette thèse explore comment les méthodes en boîte noire, ne se reposant que sur des observations d’execution du code, peuvent inférer des propriétés utiles pour la rétro-ingénierie et la compréhension de code. En premier lieu, nous étudions le problème de l’inférence de contrats de fonctions qui a pour objectif d’apprendre sur quelles entrées une fonction peut être exécutée pour obtenir les sorties souhaitées. Nous étudions ensuite le problème de la déobfuscation de code, qui vise à simplifier du code obfusqué.

Jury