To refine symbolic and concrete deobfuscation of programs protected by opaque predicates

Une forte demande existe aujourd’hui pour améliorer les techniques avancées d’obfuscation et de déobfuscation, dans le but d’éviter le vol de propriétés intellectuelles ou de perfectionner la défense face aux attaques en cybersécurité. Les travaux réalisés au cours de cette thèse portent sur la consolidation de la déobfuscation réalisée par des outils d’analyse symbolique et concrète de programmes protégés par des prédicats opaques. Ces outils s’appuient sur des outils d’analyse automatisée de programmes (moteur d’exécution symbolique dynamique) qui utilisent des solveurs de satisfiabilité modulo théorie (solveurs SMT). Nous souhaitons comprendre plus précisément certaines situations pour lesquelles l’analyse de prédicats effectuée par ces outils est mise en échec, pour ensuite pouvoir proposer des solutions pratiques évitant ces scénarios, et les tester dans des cas réels. C’est pourquoi notre travail se concentre sur la compréhension des concepts de raisonnement automatisé dans une théorie décidable et complète, afin de clarifier les mécanismes de capture de l’information. Nos premiers résultats montrent comment un jeu d’instructions machine assembleur (ISA) autorise l’apparition ou non de prédicats opaques. Nous proposons une amélioration de la détection de prédicats opaques à partir du comportement du solveur SMT. Nous proposons une redéfinition des requêtes SMT pour réduire les effets des prédicats opaques. Nous intégrons ces améliorations dans plusieurs outils automatiques tels que KLEE ou Angr, puis les testons sur différents programmes contenant des prédicats opaques.High demand exists nowadays to improve advanced obfuscation and deobfuscation techniques, with the purpose of preventing intellectual property piracy or improving defence against cyber security attacks. This thesis focuses on the improvement of the deobfuscation achieved by symbolic and concrete analysis tools of protected programs using opaque predicates. These tools rely on automated program analysis tools (dynamic symbolic execution engine) that use Satisfiability Modulo Theory solvers (SMT solvers). To understand more precisely some situations in which the predicate analysis performed by these tools fails, our aim is to be able to identify practical solutions to avoid these scenarios and test them in real cases. First results show how an Instruction Set Assembly (ISA) allows opaque predicates to appear or not. We suggest an improvement of the opaque predicates identification based on the SMT solvers behavior. We suggest a method to reshape SMT queries to reduce the effects of opaque predicates. These features are built into several automated tools such as KLEE or Angr, followed by testing them on different programs which contain opaque predicates