Cette thèse n'aurait jamais vu le jour sans la contribution et l'aide de nombreuses personnes. En particulier je souhaite remercier Sébastien Bardin qui a fait preuve d'une patience infinie et d'une disponibilité à laquelle peu d'encadrants peuvent prétendre. Il a su m'inculquer une rigueur et une discipline scientifique qui ont porté leurs fruits tout au long de cette thèse. Je souhaite aussi remercier tout particulièrement Jean-Yves Marion qui en dépit de toutes ses attributions a réussi à m'accorder maintes de ses précieuses heures pour m'aider à progresser sur mon sujet et me donner son analyse objective et éclairée.

Je tiens à remercier profondément tous mes collègues du LSL avec qui passer ces trois années fut un immense plaisir. Je remercie toutes les personnes ayant pris le temps de répondre à mes questions; Adel pour avoir répondu à toutes mes requêtes de décodage d'instructions, Patricia pour sa relecture minutieuse et ses conseils avisés concernant l'administratif au CEA, Florent pour les discussions toujours très enrichissantes autout de la sécurité ainsi que Guillaume pour son passage fugace au CEA, avec qui partager le bureau fut autant agréable qu'inversement proportionnellement productif.

Par ailleurs, je remercie les cousins de Vérimag et Josselin avec qui collaborer fut enrichissant, Fabrice qui m'a encouragé à poursuivre en thèse et Thanh Dinh pour toutes ses discussions autour de l'obfuscation. Je souhaite remercier chaleureusement Joan Calvet qui a joué un rôle clé dans la validation expérimentale de ma thèse en me fournissant le meilleur cas d'utilisation auquel on puisse rêver.

Je souhaite remercier du plus profond du coeur mes parents et ma famille pour leur soutien inconditionnel en leur aide en toute circonstances. Enfin je remercie profondément tous mes amis qui m'ont aidé à sortir la tête de ma thèse, qui ont su être présents quand il le fallait et qui ont probablement pâti de mon implication acharnée sur mon sujet. i

Pour mon grand-père qui m'avait toujours encouragé à persévérer aussi loin que possible dans mes études

iii

Résumé long Introduction Contexte

Le terme générique Logiciel malveillant, ou "malware" en anglais, désigne un logiciel développé dans l'intention de nuire à un système ou à des personnes. Ce type de logiciels a énormément évolué en une décennie, passant du vol de données ou de coordonnées bancaires [START_REF] Ioactive | Reversal and Analysis of Zeus and SpyEye Banking Trojans[END_REF] à des attaques programmées, commanditées et développées par des états ou organisations à des fins géopolitiques [START_REF] Langner | To Kill a Centrifuge[END_REF][START_REF]Alert (TA14-353A) Targeted Destructive Malware[END_REF]. Le coût induit par ce genre de menaces rend de plus en plus important et critique la mise en oeuvre de protections. La première étape consiste à analyser et comprendre le fonctionnement de ce type de logiciels. Le code source n'étant pas disponible, des techniques d'analyses au niveau binaire doivent être développées. Malheureusement, ces programmes mettent en oeuvre des techniques visant à ralentir la compréhension par l'analyste ou à gêner des algorithmes automatiques. Une de ces protections, l'obfuscation, vise à cacher le comportement ou la structure d'un programme. Ainsi, cette thèse a pour but d'étudier et de développer des algorithmes robustes de détection et de suppression d'obfuscation.

Défis Scientifiques

Le but de cette thèse est de fournir des algorithmes d'analyse efficaces de détection de code obscurci au niveau binaire. L'analyse binaire est reconnue plus difficile que l'analyse de code source pour plusieurs raisons : la distinction entre code et donnée n'est pas triviale. De plus, le graphe de flot de contrôle n'est pas forcément disponible [BHV11; BR10; MM16], l'identification des fonctions du programme n'est pas aisée et les données ne sont pas typées comme elles le seraient sur du code source. Notons enfin que la grande diversité d'architectures complique la création d'outils d'analyse. Effectuer ce genre d'analyses sur des programmes obscurcis est donc d'autant plus dur que ceux-ci mettent en oeuvre des contre-mesures pour les contourner. Les deux principaux défis scientifiques sont :

• Comment faire des algorithmes robustes qui passent à l'échelle sur du code obscurci ?,

xvii

• Comment localiser l'obfuscation et l'enlever pour rendre le code plus exploitable pour l'analyste ?

Répondre à ces deux questions permettrait de grandes avancées dans le domaine de l'analyse de virus.

Contributions

Cette thèse s'inspire et prend racine dans les méthodes formelles initialement développées pour des analyses de sûreté de logiciels critiques. Nous mettons l'accent sur l'Éxecution Dynamique Symbolique (DSE) [START_REF] Cadar | Symbolic Execution for Software Testing: Three Decades Later[END_REF] théoriquement plus adaptée pour des questions d'obfuscation de par sa grande robustesse. Nos quatre principales contributions sont listées ci-dessous.

Contribution #1 Nous proposons deux variantes du DSE adaptées à l'obfuscation.

• la gestion des concrétisations et des symbolisations via un langage de règle CSml intégré dans le calcul du prédicat de chemin permettant de définir des politiques. Cela permet un réglage fin de la correction et de la complétude;

• une variante de l'algorithme de DSE mais fonctionnant en arrière et de manière bornée bb-dse. Cet algorithme permet la résolution de certains problèmes d'obfuscation.

Contribution #2 Les algorithmes ont été implémentés dans différents outils, Binsec/se, Pinsec et Idasec puis testés sur des exemples concrets. Ces trois outils sont respectivement le moteur d'exécution symbolique, le moteur d'instrumentation dynamique et un plugin IDA pour l'exploitation des données. En particulier Binsec/se intègre différentes optimisations novatrices en terme de DSE dont la plus notable est le STMC-Read-over-Write permettant une gestion optimisée des lectures/écritures en mémoire. Ces outils ont été testés avec succès aussi bien sur des malware Windows que des binaires Linux tels que les coreutils.

Contribution #3 En sus, trois combinaisons d'analyse ont été élaborées afin de répondre à des problématiques annexes telles que le désassemblage ou la détection de vulnérabilités. Les trois combinaisons sont :

• combinaison de désassemblage dynamique et de désassemblage statique contrôlé par du bb-dse. Le but est de l'appliquer à l'obfuscation afin de fournir un désassemblage plus précis tirant parti des informations d'obfuscation calculée par le bb-dse,

• détection de Use-After-Free en collaboration avec le laboratoire Vérimag,

• détection de critères de tests infaisables appliquée dans une thématique de test sur du code source. Cette combinaison se base sur une combinaison entre interpretation abstraite en avant et calcul de plus faible-précondition (WP).

xviii Contribution #4 La dernière contribution majeure est l'étude, la formalisation et l'expérimentation de deux algorithmes de détection d'obfuscation appliqués respectivement à deux obfuscations: les prédicats opaques et les corruptions de pile d'appel. Une validation expérimentale des deux algorithmes a été effectuée avec succès sur un large échantillon de packers et sur certains malwares comme X-Tunnel. Ce dernier développé par le groupe APT28/Sednit a pour but l'exfiltration de données et fut connu pour son utilisation lors du piratage du Comité national démocrate aux Etats-Unis [START_REF] Alperovitch | Bears in the Midst: Intrusion into the Democratic National Committee[END_REF]. L'analyse de ce dernier a mis en évidence la présence de très nombreux prédicats opaques ayant pu être supprimés grâce à la méthode de détection sus-citée.

État de l'art

Obfuscation D'un point de vue théorique un obfuscateur est défini par Barak [Bar+12] comme une transformation O sur un programme P satisfaisant trois propriétés : la fonctionnalité, le ralentissement polynomial et la boite-noire virtuelle. De cette définition découle l'impossibilité de faire un obfuscateur parfait dans le cas général. Cependant en pratique, de nombreux obfuscateurs existent. On approchera donc le problème de l'obfuscation d'un point de vu pragmatique avec la définition donnée par Collberg [START_REF] Collberg | Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection[END_REF]. En effet, il caractérise une obfuscation à partir de 4 critères : l'efficacité, la puissance, la furtivité et le coût se referrant à la propriété de ralentissement polynomial.

Code Vs données Une obfuscation affecte généralement soit le flot de contrôle soit les données d'un programme. Une obfuscation du flot va tenter de brouiller la structure logique des instructions et des fonctions alors qu'une obfuscation de donnée va essayer de cacher certaines ressources du programmes comme des chaînes de caractères ou des constantes. Parmi les obfuscations de contrôle, on peut citer le "code flattening" servant à applatir le CFG, les obfuscations par signaux et exceptions servant à faire des sauts nonexplicites ou encore le "code overlapping" permettant à deux instructions différentes de partager certains octets. Parmi les obfuscations de données, on peut citer le chiffrement des chaînes de caractères ou encore le "mixed-boolean arithmetic" [START_REF] Zhou | Information Hiding in Software with Mixed Boolean-Arithmetic Transforms[END_REF] permettant notamment de cacher certaines constantes ou clés en les décomposant.

Désobfuscation

Le terme désobfuscation regroupe toute technique visant à contourner ou enlever les protections sus-citées. Elle peut donc être divisée en deux étapes différentes : la détection de l'obfuscation et la suppression, cette dernière étape étant potentiellement beaucoup plus complexe à mettre en oeuvre. Basé sur les définitions ci-dessus, voici les trois actions envisageables une fois la détection effectuée :

• inverser la transformation d'obfuscation (généralement impossible),

• récupérer une information précise dans le code obscurci, xix

Résumé long

• simplifier le code obscurci pour faciliter des analyses ultérieures.

Nous orientons nos recherches vers la dernière possibilité, étant donné que le but de cette thèse est de faciliter l'analyse d'un ingénieur en retro-ingénierie.

État de la technique Dans l'industrie les méthodes employées sont généralement statiques ou dynamiques et dans la plupart des cas, syntaxiques. Ces approches sont parfaitement viables mais néanmoins peu résistantes à la combinaison d'obfuscation ou l'apparition de nouvelles obfuscations. En effet, l'analyse statique est souvent syntaxique et basée sur des heuristiques. L'analyse dynamique quant à elle, s'effectue généralement dans une sandbox ou directement manuellement via un debugger.

Méthodes formelles Les approches formelles statiques se basent pour certaines sur l'interprétation abstraite [START_REF] Dalla Preda | Opaque Predicates Detection by Abstract Interpretation[END_REF][START_REF] Kinder | Towards Static Analysis of Virtualization-Obfuscated Binaries[END_REF] et visent particulièrement les techniques de machines virtuelles ou de "code flattening". Cependant, ces analyses considèrent souvent le CFG comme disponible et immuable sans aucune auto-modification. Ceci limite donc beaucoup le domaine d'application. A l'inverse, les approches dynamiques cherchent à contourner le polymorphisme ou le chiffrement des données [START_REF] Kang | Renovo: A Hidden Code Extractor for Packed Executables[END_REF][START_REF] Ugarte-Pedrero | SoK: Deep Packer Inspection: A Longitudinal Study of the Complexity of Run-Time Packers[END_REF]. Les approches dynamiques étant généralement plus lentes, il est parfois difficile de les mettre en oeuvre sur un grand nombre de programmes. Enfin, plusieurs approches symboliques ont été expérimentées pour traiter différents problèmes d'obfuscation [Bru+07; LPG13; YD15]. Cette thèse s'inscrit dans cette ligne de recherche et propose des algorithmes permettant le passage à l'échelle sur du code obscurci, ce qui reste le principal défaut des techniques sémantiques existantes.

Attaques sur la désobfuscation Une obfuscation tente généralement d'empêcher soit les techniques d'analyse statique soit les techniques d'analyse dynamique. L'analyse statique est hautement dépendante du graphe de flot de contrôle (CFG), toute obfuscation le ciblant est donc potentiellement efficace. L'obfuscation dynamique cherche généralement à empêcher l'exécution ou le debug du programme dans une machine virtuelle ou un environnement instrumenté. Enfin très peu d'obfuscations ciblent directement l'exécution symbolique car la mise en oeuvre est difficile. Le concept de "secure triggers" [START_REF] Futoransky | Foundations and Applications for Secure Triggers[END_REF] exploite généralement la difficulté d'inverser les fonctions de hachage pour protéger leur code et rendre inefficace toute analyse symbolique.

Exécution Symbolique Dynamique

L'exécution symbolique (SE) est une approche qui, pour un chemin donné dans un programme, va calculer un ensemble de relations sous forme d'une formule pour laquelle une solution est un jeu d'inputs permettant d'emprunter ce chemin [START_REF] King | Symbolic Execution and Program Testing[END_REF]. Il est ensuite possible d'énumérer les chemins pour couvrir et tester tout le programme. L'exécution symbolique dynamique ou encore exécution concolique utilise une exécution concrète (réelle) afin de déterminer le chemin à calculer. Les avantages sont nombreux : l'exécution est correcte (faisable en pratique), l'instruction suivante est toujours connue et le dépliage xx des boucles est automatique. Cette approche est donc robuste aux différentes constructions inhérentes au binaire. Néanmoins, l'exécution est sous-approximée et dépendante des entrées utilisées. L'exploration est donc partielle (incomplète).

Prédicat de chemin Le calcul du prédicat de chemin est la composante essentielle du DSE. Pour un chemin π, ϕ est un prédicat de chemin de π si pour toute valuation des entrées t (solution de ϕ), l'exécution de programme P sur t noté P (t) emprunte le chemin π. Il est correct si toutes les solutions couvrent π et il est complet si tout jeu d'entrées couvrant π est une solution. Intuitivement, un prédicat de chemin est la conjonction de toutes les conditions de sauts conditionnels rencontrées sur ce chemin. En DSE, sur un chemin concret, il est possible de remplacer des valeurs logiques par leurs valeurs lors de l'exécution afin de simplifier le prédicat de chemin (concrétiser). A l'inverse, il est aussi possible de symboliser une valeur afin de simuler des valeurs inconnues ou des effets non-déterministes. Ces deux mécanismes sont un point essentiel pour une analyse robuste et offrent un compromis entre correction et complétude. La Figure 1 montre respectivement un programme, le prédicat de chemin associé, le même prédicat où a = 5 a été concrétisé et le même prédicat où x 1 a été symbolisé avec un nouveau symbole. Faire varier les concrétisations et les symbolisations permet d'ajuster et choisir un compromis entre précision et complétude. Un des leviers disponibles pour améliorer le passage à l'échelle du calcul de prédicat de chemin est la modulation des concrétisations et des symbolisations. Alors que les approches existantes abordent le problème comme un élément mineur de l'implémentation nous proposons un nouvel algorithme de calcul du prédicat de chemin intégrant un système de politique de concrétisation/symbolisation permettant de moduler le comportement du calcul de chemin (cf 1 via un langage de règles [START_REF] David | Specification of Concretization and Symbolization Policies in Symbolic Execution[END_REF]. Pour une variable donnée, trois actions sont possibles :

• Concrétiser (C) remplace la valeur logique par la valeur à l'exécution. Cela sousapproxime le prédicat de chemin mais réduit la complexité de la formule,

• Symboliser (S) remplace la valeur logique par un nouveau symbole (nouvelle variable libre). Cela sur-approxime en généralisant certaines valeurs du prédicat de chemin et permet donc de simuler des valeurs complètement inconnues (retour de fonctions, etc),

• Propager (P) calcule la valeur logique sans aucune approximation (comportement par défaut).

Politique de C/S & CSml

Le but est de définir un mécanisme clair et flexible permettant de moduler les concretisations et symbolisations tout en assurant la correction et ce pour chaque expression de l'exécution. L'idée est de concevoir un langage de spécification haut-niveau pour les politiques de C/S fournissant les propriétés suivantes:

• un langage et une sémantique claire qui soient simple et concis,

• indépendant vis-à-vis du moteur de DSE,

• possiblité d'encoder toutes les politiques de la litterature.

Cela a été effectué via CSml intégré dans Binsec/se offrant un langage de règles de C/S. Une règle est de la forme guard ⇒ ρ où guard permet de vérifier si la règle doit être déclenchée et ρ indique l'action à effectuer dans ce cas ({C, S, P}). Chaque règle est testée séquentiellement, la première satisfaisant la condition de guard renvoie l'action associée. Formellement guard est défini par (φ loc , φ ins , φ expr , φ Σ ) qui sont respectivement un prédicat sur le point de contrôle, l'instruction, l'expression et l'état mémoire. Ces différents prédicats permettent de filtrer précisement l'expression sur laquelle effectuer l'action associée.

Expérimentations Différentes expérimentations on été effectuées formant la première évaluation quantitative et systématique des politiques de C/S dans le DSE. Nous avons évalué différentes politiques issues de la litterature, traitant les accès mémoires de manière différente. Cinq politiques ont été évaluées sur un total de 169 programmes tirés de différentes suites de benchs et des coreutils de Linux. Les résultats montrent qu'aucune politique ne surpasse toutes les autres et qu'en fonction du besoin, le choix de la politique peut avoir une grande influence. Ces résultats ont validé a posteriori le besoin d'un méchanisme générique et flexible pour moduler les C/S.

DSE arrière-borné

Le DSE appliqué en avant avec des politiques de C/S permet un meilleur passage à l'échelle sur de gros prédicats de chemins. Cependant, il est parfois insuffisant voire inadapté pour résoudre certains problèmes, en particulier les problèmes d'infaisabilité. On définit ce problème par : Une requête d'infaisabilité vise à vérifier l'infaisabilité de certains évènements où de certaines configurations dans un environement donné. Par exemple l'impossibilité de prendre une branche, de sauter à une adresse particulière ou encore d'avoir une valeur précise dans un registre donné d'une adresse particulière. Le DSE classique (en avant) vise à résoudre des problèmes de faisabilité (i.e. ateignabilité, faisabilité de chemin, valeur de registre etc) et ce, afin de générer de nouvelles entrées satisfaisant le problème à résoudre. Plusieurs problèmatiques d'obfuscation entrent dans le cadre des problèmes d'infaisabilité (détection de code mort, etc).

bb-dse Le bb-dse [START_REF] David | Backward-Bounded DSE: Targeting Infeasibility Questions on Obfuscated Codes[END_REF] est un algorithme de DSE fonctionnant en arrière, et ce, de manière bornée pour assurer le passage à l'echelle. Il s'agit d'une approche orientée par les buts dans laquelle l'analyse démarre du point de contrôle de la propriété à prouver et calcule le prédicat de chemin en arrière un nombre borné k d'instructions. La principale conséquence du point de vue de la formule est de sur-approximer tous les états possibles, au-delà de la borne k. Une propriété prouvée insatisfiable sur un sous-chemin k reste donc insatisfiable sur le sous-chemin k + 1. En effet, l'ajout de contraintes ne peut pas rendre une formule à nouveau satisfiable pour des raisons de monotonie. La figure 2 illustre le fonctionnement de l'algorithme. Cet algorithme ne remplace pas le DSE classique mais le complète pour un certain type de propriétés à prouver.

Formellement le DSE se base sur l'opération post tandis que le bb-dse se base sur l'opération pre et plus particulièrement sur un nombre borné d'itérations de la fonction notée pre ≤k . La problématique est d'ajuster la borne k afin de limiter le nombre de faux négatifs ou de faux positifs. Les expérimentations effectuées dans la Contrib#4 démontrent l'utilité de l'approche pour certains problèmes d'obfuscation comme les prédicats opaques ou corruption de pile d'appel. Il permet aussi de récupérer les paramètres des fonctions via des "stubs", de récupérer ou de patcher à la volée des valeurs arbitraires lors de l'instrumentation ou encore de communiquer avec le DSE via un protocole d'échange de messages.

Binsec/se est développé dans la plateforme d'analyse Binsec [START_REF] Djoudi | BINSEC: Binary Code Analysis with Low-Level Regions[END_REF] et y apporte un moteur de DSE [START_REF] David | BINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis[END_REF]. Le moteur supporte tous les algorithmes mentionnés cidessus et fournit un grand choix d'options de configuration. Il est notamment possible de paramétrer la politique de C/S, la convention d'appel, le solveur, les optimisations sur les formules ou encore le timeout. Les options peuvent notamment être fournies sous forme d'un fichier de configuration en JSON. Avec cela, n'importe quelle analyse peut être implémentée via les API fournies. Par ailleurs, Binsec/se peut recevoir et traiter directement les requêtes par le réseau. En ce qui concerne les solveurs il supporte Z3, CVC4, boolector et Yices grâce à une intégration boite noire via le format SMTLIB2.

Idasec est développé en Python et s'intègre au désassembleur IDA [START_REF]Hex Rays. IDA Pro -Hex-Rays[END_REF] via son mécanisme de plugins. Parmi ses fonctions basiques, il permet d'obtenir la mnémonique d'une instruction, visualiser une trace d'exécution ou encore surligner le chemin emprunté sur le CFG. Ce plugin peut se comporter comme un intermédiaire entre Pinsec et Binsec lorsque les analyses sont effectuées à distance en flux continu.

Optimisations des formules

L'optimisation des formules générées est une composante essentielle pour le passage à l'échelle des analyses et compte parmi les contributions de cette thèse. Les optimisations présentées ci-dessous ambitionnent une réduction soit en espace soit en temps. Le gain de temps est privilégié car la contrainte de temps est le principal facteur limitant en DSE. Parmi les optimisations développées nous distinguons deux categories ; (1) les optimisations offrant un pré-processing minimal visant à uniformiser les formules générées ce qui, de manière opportuniste, améliore les performances de certains solveurs et (2) les optimisations dédiées à la simplification des tableaux.

Optimisations de pré-processing Les différentes optimisations de pré-processing implémentées sont:

• backward pruning, vise à retirer tous les termes d'une formule n'intervenant pas dans la résolution des contraintes,

• propagation constante, optimisation standard qui sans améliorer significativement le temps de résolution ou la taille de la formule, produit une forme plus canonique

• rebase, réduit le nombre d'identifiants de variables crées via la réutilisation d'identifiants plus anciens et la simulation des opérations arithmétiques. Par exemple, dans le cas esp 1 := esp 0 -4; esp 2 := esp 1 -4 la variable esp 2 est redéfinie par esp 2 := esp 0 -8. L'avantage est de fournir une base de comparaison commune entre esp 1 et esp 0 en les rendant facilement comparables vis-à-vis de esp 0 .

• prédicats haut-niveau, vise à remplacer des opérations de comparaison bas niveau par des conditions plus naturelles. Par exemple la condition associée à la comparaison cmp ecx, 24; jl xx en x86 est ((ecx -24) < s 0) = (ecx {31} = 24 {31} )&&(ecx {31} = (ecx -24) {31} ) alors que l'opération de haut niveau est : ecx < 24.

xxv

Résumé long

Optimisations de tableaux Le Read-over-Write est une propriété sur la théorie des tableaux qui indique que pour un tableau donné il est logiquement équivalent de substituer la lecture à un index donné par la valeur précédement écrite à ce même index. Effectuer cette opération permet donc de réduire le nombre de lectures en mémoire. Dans la théorie des tableaux, l'opération write renvoie un nouveau tableau mis à jour avec la valeur écrite. Un tableau est donc une suite, une séquence d'écriture dans un tableau initial vide. Effectuer l'opération de RoW nécessite donc de parcourir linéairement cette chaîne et ce, pour chaque opération read. La complexité est donc approximativement au pire cas quadratique en la taille de la chaîne de write. Une des contributions de ma thèse est de proposer un modèle novateur de représentation des écritures permettant d'effectuer cette optimisation en temps logarithmique dans le meilleur cas ou identique en complexité à l'approche classique dans le pire cas. L'efficacité dépend notamment de la politique de C/S employée vis-à-vis des lectures/écritures en mémoire. Cette thèse compare les deux approches et met en avant le gain en terme de temps de résolution des formules avec le store-map RoW. En sus, le memory flattening est une deuxième optimisation sur les tableaux qui sert à supprimer la théorie des tableaux de la formule lorsque le Read-over-Write à été suffisamment efficace pour supprimer tous les store et ramener tous les read sur la mémoire initiale à des indices constants.

Contribution #3: Combinaisons d'analyses

Désassemblage minutieux

Une instruction est authentique ou avérée si lors de l'exécution du programme elle est exécutée. Un désassembleur est sûr s'il désassemble uniquement des instructions authentiques (et non pas des données). Il est dit complet s'il retrouve toutes les instructions authentiques du programme. Les trois algorithmes de désassemblage classiques sont:

• le désassemblage récursif suit le flot du programme pour le désassembler. Cette approche est rapidement limitée par les sauts dynamiques (saut à une valeur connues seulement à l'exécution);

• le balayage linéaire désassemble séquentiellement chaque octet des sections exécutables d'un binaire. Le problème de cette approche est le "sur-désassemblage". En effet, de nombreux octets de padding ou de données seront décodés comme des instructions. L'approche n'est donc pas sûre;

• le désassemblage dynamique utilise les branches observées lors d'une exécution pour déterminer les cibles de saut. Cette méthode est sûre mais incomplète dans la mesure où une seule exécution est couverte.

Combinaison Le but de la combinaison proposée est d'enrichir un algorithme de désassemblage dynamique avec un désassemblage statique récursif contrôlé grâce à des informations d'obfuscation calculées par exécution symbolique. L'idée est donc, non pas xxvi de désassembler le plus d'instructions possibles, mais de désassembler plus justement les instructions.

Les enrichissements par rapport à un algorithme classique sont les suivants :

• utilisation des valeurs dynamiques pour désassembler les cibles de saut dynamique (comme pour un désassemblage dynamique),

• utilisation des informations de prédicats opaques pour ne pas désassembler les branches mortes,

Prédicats Opaques

Définition La première obfuscation traitée dans cette thèse est celle basée sur les prédicats opaques (PO). Un PO est une condition s'évaluant toujours à vrai (ou toujours faux) mais dont cette propriété est difficile à déduire à priori. Cette technique permet notamment de gonfler artificiellement le code d'un programme en ajoutant du code mort dans les branches mortes.

Corruption de pile d'appel

Évaluation à grande échelle de packers

Binaires analysés Cette étude s'intéresse aux packers qui constituent habituellement, la première, voire l'unique couche de protection pour beaucoup de codes malveillants.

Bien que les packers puissent être utilisés pour protéger des logiciels légitimes ils sont tout autant utilisés pour "packer" des virus. Plus en détail, les résultats permettent de constater que certains packers n'utilisent aucune des deux obfuscations tel que Expressor, tandis que d'autres comme Crypter ou ACProtect les utilisent de manière intensive. Une vérification manuelle a permis de valider la grande majorité des résultats observés. Les résultats laissent aussi à penser que l'instrumentation dynamique a parfois été déjouée par le packer comme c'est peutêtre le cas pour Molebox ou EP Protector dont la trace est étrangement petite (250 instructions). Par ailleurs, l'analyse de corruption de pile d'appel a permis de détecter pour certains packers l'instruction ret corrompue effectuant la transition finale entre le code du packer et le payload. Dans ce cas, ce dernier est systématiquement détecté comme violé.

Cas d'étude : X-Tunnel

Contexte X-Tunnel est un proxy chiffrant utilisé pour l'exfiltration de données de machines non-directement reliées à internet. Ce malware a été utilisé lors de différentes attaques ciblées à visées géopolitiques menées notamment contre des infrastructures de l'OTAN [START_REF] Micro | Operation Pawn Storm, Using Decoys to Evade Detection[END_REF], le parlement Allemand [von15] ou encore le parti démocrate américain (DNC) [START_REF] Alperovitch | Bears in the Midst: Intrusion into the Democratic National Committee[END_REF]. Le groupe derrière ces attaques est dénommé APT28, Sednit ou encore Sofacy group [START_REF] Calvet | Visiting The Bear Den, A Journey in the Land of (Cyber-)Espionage[END_REF].

Contexte d'analyse

L'analyse se focalise sur 3 échantillons de X-Tunnel compilés à plusieurs mois d'intervalle et dont les deux derniers ont la particularité d'être obfusqués. La nécessité d'analyser les binaires obfusqués est motivée par la question de savoir si de nouvelles fonctionnalités ont été ajoutées. Le malware se connectant à des serveurs C&C et attendant des connexions de clients pour effectuer le tunneling, il est préférable d'effectuer l'analyse de manière complètement statique. De plus, les binaires ne semblent pas utiliser d'auto-modification. L'ensemble du code, bien qu'obfusqué, est donc disponible. Un examen rapide du code a révélé la présence de prédicats opaques. Le principal objectif est de les supprimer afin d'en révéler, éventuellement, de nouvelles fonctionnalités dans une analyse ultérieure. Développement de l'analyse L'exécution symbolique est effectuée de façon statique (SE) ce qui ne change pas l'analyse de prédicats opaques puisque celle-ci est effectuée de façon complètement symbolique, qui plus est, sur de petits prédicats de chemins (16 instructions). L'analyse développée est guidée par Idasec qui génère des sous-chemins pour chaque prédicat à tester. Ces chemins sont ensuite envoyés pour résolution à Binsec/se configuré en mode serveur. En fonction du résultat renvoyé, Idasec assure le marquage des prédicats opaques et surtout des parties de code mort. Afin de rendre les résultats exploitables, trois traitements ont été implémentés dans Idasec:

• extraction(synthèse) du prédicat opaque haut-niveau (afin de les répertorier),

• identification des instructions fallacieuses servant uniquement à calculer un PO,

• extraction d'un CFG réduit basé sur la suppression du code mort et des instructions fallacieuses.

Résultats Pour chacun des 2 échantillons obscurcis, l'analyse a duré environ 1h30 pour environ 35000 prédicats chacun (Core i7-4800MQ 2.7GHz, 16Go RAM). Ce temps inclut toutes les communications réseaux, la création des chemins et le post-traitement. Les deux prédicats identifiés sont 7x 2 -1 = x 2 et 2 x 2 +1 = y 2 + 3. Plus de 30% de toutes les conditions dans le code ont été identifiées et validées comme opaque. Une évaluation approximative a permis d'identifier parmi tous les prédicats, 10% de prédicats valides identifiés comme opaques (faux positifs) et seulement 2.3% de prédicats opaques non détectés (faux négatifs). L'analyse a permis de supprimer dans chaque échantillon environ 44% du code identifié comme mort ou inutile. La figure 4 montre un exemple de fonction après extraction du CFG réduit.

En conclusion, l'analyse de prédicats opaques a permis d'élaguer considérablement les fonctions obfusquées et d'en extraire des représentations non-obfusquées beaucoup plus compactes. Les deux programmes une fois désobscurcis obtiennent un nombre d'instructions similaires à la version non-obscurcie. De plus, en vertu de la faible différence de temps entre chaque version, il est peu probable que de nouvelles fonctionnalitées aient été ajoutées.

Conclusion

Résumé des contributions

Variantes du DSE pour la désobfuscation Les principales contributions de ma thèse sont la formalisation, l'implémentation et le test d'un algorithme de calcul de prédicat de chemin pour le DSE intégrant les concrétisations et les symbolisations de manière flexible. Ceci est rendu possible via l'élaboration d'un méta-langage CSml permettant la spécification de politiques. Cette flexibilité a permis de tester et mettre en évidence l'impact des concrétisations et des symbolisations sur le temps de résolution des prédicats. Afin d'accentuer ce gain en temps, cette thèse décrit, formalise et implémente différentes optimisations sur les formules dont la plus notable est le STMC-RoW. Différentes expérimentations ont permis de mettre en évidence la plus-value de ces optimisations sur le temps de résolution. L'algorithme de bb-dse est une autre contribution majeure de mes travaux. En effet, peu d'études ont été effectuées sur le DSE arrière et ses avantages, notamment pour les problèmes d'infaisabilité. Cette thèse formalise un algorithme robuste et précis permettant de résoudre ce type de problèmes, appliqué à l'obfuscation. Cet algorithme s'est révelé très efficace pour la détection de prédicats opaques et la détection de corruption de pile d'appel. Bien qu'il ne remplace pas le DSE en avant, cet algorithme le complète. Étude de cas L'obfuscation étant la pierre angulaire de cette thèse, mes travaux proposent deux algorithmes d'identification et de caractérisation pour deux obfuscations, les prédicats opaques et les corruptions de pile d'appel. Ces algorithmes ont été utilisés avec succès, aussi bien sur des packers commerciaux que sur des codes malveillants. Ces contributions ont permis de mettre en évidence des phénomènes et des structures inattendues. Par exemple, le prédicat opaque 2

x 2 +1 = y 2 + 3 identifié dans X-Tunnel n'avait à notre connaissance jamais été vu ailleurs. Autre effet inattendu, l'analyse de corruption de pile xxxiv d'appel a permis dans certains cas de mettre en évidence l'instruction précise effectuant la transition entre le code du packer et le payload, lorsque celui-ci utilise l'instruction ret pour faire le saut.

Combinaison d'analyses

Les combinaisons d'analyses étudiées ont permis de mettre en évidence l'intérêt et les bénéfices de certaines combinaisons avant/arrière et ce, aussi bien sur du code binaire que sur du code source. Dans le cadre de cette thèse, la combinaison la plus notable est le désassemblage "sparse" qui combine un désassemblage statique avant avec une exécution symbolique arrière bornée. La combinaison avec le DSE est d'autant plus efficace qu'elle est intégrée dans l'algorithme et le processus de désassemblage et non pas comme une passe de post-processing.

Contributions à la communauté

Une idée clé est de rendre les algorithmes utilisables en pratique par des ingénieurs en rétro-ingéniérie et utilisables au niveau industriel. Pour cela, tous les algorithmes ont été développés dans des outils open-source, notamment Pinsec, Binsec/se et Idasec. Ces trois outils fournissent respectivement une instrumentation dynamique, un moteur d'exécution symbolique et un plugin IDA pour une exploitation plus aisée des données. Ces travaux ont été présenté dans des conférences comme BlackHat Europe 2016 [START_REF] David | Code Deobfuscation: Intertwining Dynamic, Static and Symbolic Approaches[END_REF] ou bien dédiées à la communauté de la sécurité [START_REF] Bardin | Binsec: Binary-Level Semantic Analysis to the Rescue[END_REF].

Perspectives

Cette thèse ouvre la voie à de nombreuses applications et améliorations comme la détection d'obfuscations à base de machines virtuelles ou encore la création de signatures sémantiques du code désobfusqué. Dans ce sens, la prochaine étape clé est d'intégrer les résultats de désobfuscation dans les travaux d'analyse morphologique basés sur de l'isomorphisme de graphes, développés au LORIA. Ceci dans le but de calculer des signatures de malwares plus précises et efficaces. Ainsi, cette thèse a montré que des méthodes formelles telles que le DSE peuvent être employées pour des problématiques de sécurité en fournissant des analyses sémantiques efficaces pour la retro-ingéniérie et l'analyse de malwares. Cela ouvre la voie à de futurs algorithmes de détection sémantique des codes malveillants, potentiellement plus efficaces que les algorithmes actuels.

xxxv

Part I

Introduction & Background

Chapter 1

Introduction 1.1 Context

Malware is a generic term grouping all software developed with the intention to harm and to threaten computer systems or their users. These malicious softwares have moved from cracking jokes in the late 90' to mass mailing worms like MyDoom and banking trojans like Zeus [START_REF] Ioactive | Reversal and Analysis of Zeus and SpyEye Banking Trojans[END_REF] in 2007 to evolve nowadays with ransomwares and government-grade cyber-espionage tools like Stuxnet or Flame. In this last scenario, malwares are the cornerstone of stealth and persistent attacks. These advanced attacks generally involve deception, zero-day exploits, various bots across the globe and a whole ecosystem of malicious softwares like infected documents, droppers, rootkits or bootkit. The sophistication of such attacks has grown tremendously the last few years and the collateral costs it implies for companies become more and more significant. For example, the famous Stuxnet malware managed to infect a Siemens Programmable Logic Controller (PLC) used in nuclear centrifuges in the Natanz Iranian nuclear facilities. It presumably destroyed up to 1000 centrifuges amounting for 10% of the total centrifuges assets [START_REF] Langner | To Kill a Centrifuge[END_REF]. Another famous case is the Sony Pictures Entertainment hack in December 2015 that led to the leak of 100 To of data. Among this data, personal employees information and four unreleased movies. The direct investigation and remediation costs were evaluated up to 35M$ and more than 100M$ for the loss of earnings. The usage of a specifically crafted worm [START_REF]Alert (TA14-353A) Targeted Destructive Malware[END_REF] made this hack possible. At a smaller scale, this kind of sabotage and blackmail occurs frequently. It was notably the case for the Hollywood Presbyterian Medical Center who paid 17K$ to recover data ciphered by a ransomware. A first step toward preventing these infections and understanding the motivations and the origin of such attacks is to analyze these malwares at binary-level.

As no source code is usually available for malware, the binary executable should be analysed directly to understand its behavior and goals. But as this area of research has grown rapidly leading to the emergence of antivirus companies and incident response companies, malware authors have also designed some counter-measures. Indeed, they started to protect their malwares as their main goal is to remain stealth and undetected as long as possible. Among those protections, obfuscation takes a significant place. It embraces any mean aiming at slowing down the analysis of a program, either by an analyst or an automated algorithm. While it has taken a significant place in the software protection field like the video-game industry, it is also now widely used in the malware ecosystem. Thus, addressing obfuscation is one of the main challenges in the malware analysis process.

My thesis was performed in collaboration with two laboratories. First my hosting laboratory, the Safety and Security Lab of the Commissariat à l'Énergie Atomique et aux energies alternatives is specialized in formal methods for software analysis. It is most notably known for its open-source C software analyzer Frama-C [START_REF] Cuoq | Frama-C: A Software Analysis Perspective[END_REF]. Secondly, the "Laboratoire de Haute Sécurité (LHS)" of LORIA Nancy focusing on virus analysis, dynamic analysis and notoriously known for its morphological malware signature technology. My whole thesis takes place in an Agence Nationale de la Recherche (ANR) project called Binsec aiming at developing a Binary Analysis platform geared for software security. The project is composed of the CEA, Irisa, LORIA, Vérimag and Airbus Group.

Research challenges

The first challenge to address toward analyzing malware is to analyze programs at binary-level. Despite the fact that analyzing binary programs helps avoiding some uncertainty about the compilation process [START_REF] Balakrishnan | WYSINWYX: What You See Is Not What You eXecute[END_REF] and is independent from the source language, it also raises some other challenges [START_REF] Bardin | Refinement-Based CFG Reconstruction from Unstructured Programs[END_REF][START_REF] Balakrishnan | WYSINWYX: What You See Is Not What You eXecute[END_REF]. Indeed, at binary-level there is no clear distinction between code and data. Furthermore, all the information available in the source code, like function bounds, function parameters and the control flow graph is not available. Moreover, there is no high-level typing especially for the memory which is seen as a flat untyped array. Thus, making formal and reliable algorithm is a challenging task [START_REF] Meng | Binary Code Is Not Easy[END_REF]. Finally, the large diversity of processor architectures (x86,ARM, MIPS..) makes the modeling of the binary instruction a tedious task. We solely in this thesis on x86 architectures as it is the most widespread architecture for desktop computers and by consequence for malwares.

Performing such analyses on malwares is even more challenging as they usually make use of multiple anti-analysis tricks. An inherent goal of obfuscation is to make the behavior of the program less understandable both for the analyst and automated algorithms by swelling the code size and shadowing the real behavior at the same time. Since my thesis focuses on real world malwares, the first research challenge is:

RC1: How to make analysis algorithms scale on real-world obfuscated malwares ?

Dealing with obfuscation can be considered as a two step process. First, it is required to detect the obfuscation with reliable algorithms. Detecting obfuscation is characterized by the ability to locate obfuscation and to differenciate what is part of the obfuscation and what is part of the original program, the payload. Once this step is achieved a second phase consists in thwarting the obfuscation or providing a non-obfuscated representation of the program. This lead to the second research challenge:

RC2: How to locate and how to remove obfuscation ?

In this context, my thesis focuses on Dynamic Symbolic Execution (DSE) [SMA05; Wil+05] (a.k.a concolic) to detect different obfuscations techniques via generic algorithms. DSE provides good promising properties to detect some obfuscations. However, as it works on a path enumeration basis, an inherent shortcoming of this approach is its difficulty to scale on real programs. This is a limitation that all existing symbolic engines are facing. We do not necessarily aim for sound nor complete DSE-based analyses but rather analyses that provides relevant obfuscation informations. The first research problem addressed is:

Problem 1. Elaborating relevant DSE-based deobfuscation algorithms that scale on oversized & highly obfuscated codes

A second problem is how to remove it or at least how to emphazise it in pursuance of distinguishing it from the payload. Performing such task might be particularly difficult without prior knowledge of the program behavior and functionalities. The second problem addressed is: Problem 2. Developping algorithms to highlight or discard obfuscation in order to make the code more understandable for the reverse-engineer Solving these two research problems would provide great advances in the academic research on binary analysis and malware analysis. Finding ways to address obfuscation with formal and sound algorithm would greatly enhance malware understanding capabilities and would lead to great practical application in the malware analysis field.

Contributions

Foundations of my thesis lay on the edge of safety based formal methods and dynamic security analysis for malware comprehension. From a global perspective, it aims at studying formal static, dynamic and symbolic approaches for deobfuscation. My thesis gather four major contributions described below.

Contribution #1: DSE geared for deobfuscation

The first main contribution of my thesis is the conception of two DSE algorithms which main particularity is to better scale on obfuscated codes than standard approaches:

• An essential part of DSE is the management of concrete values and new symbols injected in the formula. As it tends to be hardcoded in existing DSE tools, we formalize and define a new flexible path predicate computation algorithm allowing a fine tuning between soundness and completeness. For that, we define a specification for modulating concretization and symbolization (C/S) within a DSE engine. This is subsequently defined as a rule-based language, CSml, that can easily be integrated in the path predicate computation. This langage is designed to have a clear semantic, to be independant from the DSE engine and to be able to encode all existing policies from the litterature but also new ones. Experiments showed that no policy performs better than another, it all depends on the context. Thus, it validates the need of such flexible mechanisms. Optimizations For a path π, various optimizations can be performed when computing the path predicate ϕ π . We proposed two kinds of optimizations. First, basic preprocessing optimizations aiming at providing more uniformity performances across solvers. Second, we designed optimizations aiming at simplifying array manipulations in formula, which tends to be the most costly operations of solving. Among standard pre-processing algorithms we can denote constant propagation or backward pruning which remove all unused terms for the predicate to solve. Then, the rebase optimization aims at limiting the number of terms created by reusing older term definitions (see Section 7.1.3).

Array optimizations are used to significantly improve the solving time. The store-map chain Read-over-Write optimization (STMC-RoW) is a variant of the standard Readover-Write. On arrays, the standard read-over-write aims at replacing a logical select in an array by its previous stored value (if any). Our optimization enjoys a very good complexity on arrays with constant indexes (O(log(n))) and performs in the worst case as the standard RoW (O(n)) for one operation. Besides that, the memory flattening allows to completely remove the array theory when the STMC-RoW managed to remove all store operations.

Contribution #3: Analysis combinations

Trying to get the best of the two algorithms developed (cf. Contribution #1) we studied different combinations approaches, like static/dynamic, forward/backward, overapproximated/under-approximated applied to the deobfuscation but also on vulnerability discovery and software testing purposes. The idea suggested by these combinations is to take advantage of the different approaches, considering that dealing with obfuscation is a multiple facets work and requires to deal with its different aspects. We formalize and develop three combinations aiming at solving three very different problematics:

• The sparse disassembly is a combination targeting obfuscation whose main goal is to improve a dynamic disassembly algorithm with a static disassembly controled by symbolic execution enforcing not to disassemble obfuscated dead code or obfuscated function call/ret. The first entity of the combination is a static/dynamic recursive disassembly algorithm. The dynamic aspect helps getting a sound disassembly for indirect or calculated jumps which is not the case for static disassemby. This algorithm is then intertwined with a static recursive disassembly and a bb-dse algorithm to drive the disassembly not to disassemble spurious code and to disassemble some hidden control flow edges. Experiments shows that this combination performs better than IDA which over-disassemble various bytes.

• The Use-After-Free (UaF) vulnerability finding in legitimate programs. This work was performed in collaboration with Verimag and especially Josselin Feist that drove most of the design and experiments. This analysis combines a static abstract interpretation analysis aiming at finding relevant code functionalities (ie. malloc, free, use) in order to extract one or more slices of the program. Then a DSE algorithm path coverage algorithm is triggered on the slice to find possible vulnerabilities. The strength of the combination lays in the drastic reduction of possible path to cover by the DSE thanks to the slice computed by static analysis. The combination allowed to find few previously unknown vulnerabilities and especially in JasPer with CVE-2015-5221 [START_REF] Mitre | [END_REF].

• The third combination [START_REF] Bardin | Sound and Quasi-Complete Detection of Infeasible Test Requirements[END_REF] slightly moves appart from binary-level security and finds an application in source-level software testing. To test a software, we usually check its compliance to some requirements, represented by properties to check at some program locations (coverage criteria). These systematic requirements might be unverifiable due to the program structure, which tends to slow down the testing process. By combining abstract interpretation and weakest-precondition calculus, the analysis manages to detect most of these unsatisfiable tests requirements in order to remove them and speed-up the testing process. This combination named VA ⊕ WP was implemented in the C analysis platform Frama-C [START_REF] Cuoq | Frama-C: A Software Analysis Perspective[END_REF]. On the set of benchmarks assessed, the combination managed to detect 98% of infeasible requirements. It significantly improves the accuracy of coverage measurements.

Contribution #4: Experimental Validation

The last contribution is the throughout study of two obfuscation techniques: opaque predicates and call stack tampering in a real-world context. We propose two detection methods based on the previously described techniques (cf.Ctb#1). We first, define and characterize the different kinds of possible opaque predicates and call stack tampering and explain how to address them with bb-dse. We then perform two case-studies to validate the detection algorithms:

First, we perform a study of existing packers. This allowed to validate experimentally the efficiency of our analyses on real obfuscated binaries. It also gives a better understanding of the packers inner working and emphasizes the different tricks used in theirs codes (see Section 10.1).

Second, we perform an in-depth analysis of the X-Tunnel ciphering proxy used by the Sednit/APT28 group as part of their cyber-espionage attacks to exfiltrate data [START_REF] Calvet | Visiting The Bear Den, A Journey in the Land of (Cyber-)Espionage[END_REF]. Later versions of this program are heavily obfuscated with what appeared to be opaque predicates. The analysis formalized and developped in this thesis managed not only to find the obfuscation within the code but also to extract a reduced CFG for every function of X-Tunnel thus greatly simplifying a subsequent reversing of the program.

Conclusion

All these contributions improve the main underlying goal of this work which is to empower the reverse-engineering process by giving the analyst semantic information about the program and especially obfuscation. Subsequently, all the cards are placed in his hands for a better and deeper understanding of the binary being analyzed, with the assistance of different tools provided.

Publications This thesis led to the writing of 5 research papers, among which 4 are already published [Bar+15b; Dav+16a; Dav+16b; Fei+16] and one is still under review [START_REF] David | Backward-Bounded DSE: Targeting Infeasibility Questions on Obfuscated Codes[END_REF]. This work was presented during several talks and seminars, including BlackHat Europe 2016 [START_REF] David | Code Deobfuscation: Intertwining Dynamic, Static and Symbolic Approaches[END_REF].

Thesis outline

The manuscript is split in five parts. Part I provides some background about obfuscation and deobfuscation along with the basics about Dynamic Symbolic Execution. Chapter 2 lays the basic definitions and draws the global landscape of existing obfuscation and deobfuscation techniques used prior to this thesis. Chapter 3 provides all the necessary notations and definitions but also basic reminders about the dynamic symbolic execution inner working. People familiar with these notions can directly jump to the second part. Part II formalizes and describes the two DSE variants aiming at detecting obfuscation and reflect Contribution #1. Chapter 4 formalizes all the contributions brought to the path predicate computation in the DSE algorithm. In the same vein Chapter 5 formalizes and describes the Backward-Bounded DSE algorithm allowing to tune the DSE by performing it in the reverse direction. Part III discusses both the implementation performed as part of this thesis (Chapter 6) and the optimizations developped in the symbolic engine (Chapter 7). This part develops Contribution #2. Then, Part IV puts all these algorithms in action in order to validate the benefits they provide. This part describes and puts in perspective the last two contributions (#3, #4). Chapter 8 shows how they are used to deobfuscate opaque predicates and call stack tampering. Chapter 9 explores the way they can be combined with other existing analyses in order for instance, to leverage the obfuscations data into a disassembly algorithm. As an application, Chapter 10 presents three use-cases taking advantage of all the techniques and analysis defined beforehand. Finally, Part V discuss and puts in perspectives all the other potential applications of this thesis.

Introduction

Over the years, obfuscation has taken a significant place in the software protection field. This term generally embraces any mean aiming at slowing down the analysis of a program for either an analyst or an automated analysis. As such, it has become quite popular for intellectual property protection, like the video-game industry via Digital Right Management (DRM) systems [START_REF] Denuvo | Denuvo Software Solutions[END_REF][START_REF] Mougey | DRM Obfuscation vs Auxiliary Attacks[END_REF]; also it gained popularity in the malware development ecosystem. The only property that should be preserved by obfuscation is the semantic of the program i.e. its behavior. While some obfuscation techniques simply alter the syntactic form of a program, for example by twisting its CFG or adding spurious instructions, obfuscating the real behavior of the program itself is far more complex since the semantic of the program should be preserved after obfuscation. Even though watermarking can be considered as an obfuscation which hides some properties int the program, we focus in this thesis on obfuscation employed in malwares.

Definitions

Let's consider a program P . Barak et al. [START_REF] Barak | On the (Im)possibility of Obfuscating Programs[END_REF] defined an obfuscator O, as a probabilistic compiler transformation of P in O(P ) which satisfies the three following properties:

• Functionality O(P ) computes the same function as P (provide the same observable behavior),

• Polynomial slow-down For all P , O(P ) execution time is at most polynomially slower than P execution time or polynomially bigger than P size,

• Virtual black-box Everything efficiently computable with O(P ) can also be computable with only an oracle access to P .

Under this, definition obfuscation is not possible in all cases in a generic way. However, obfuscation exists in practice and we choose a more pragmatic approach. Collberg provides another definition more practical [START_REF] Collberg | Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection[END_REF]. He first defines an asset as a set of properties on a program P and some inputs I defined by asset(P, I). Then a metric m that characterizes the difficulty to compute the asset is defined by m(P, asset( )) ∈ [0, 1]. O(P ) is an obfuscation transformation if: m(O(P ), asset( )) > m(P, asset( ))

In addition to the semantic preserving property, Collberg's work [START_REF] Collberg | Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection[END_REF] characterizes an obfuscation according to three other characteristics:

• effectivness. reversing the obfuscation process requires more resources than creating it,

• potency. does not weaken other obfuscation,

• stealth. splitted in two: local stealth an adversary cannot find where the transformation was applied and steganographic stealth an adversary can not find out whether a transformation has taken place or not,

• cost. overhead in space or time implied by the transformation.

More recently, some works proposed a theoric definition of obfuscation based on indistinguishability [START_REF] Garg | Candidate Indistinguishability Obfuscation and Functional Encryption for All Circuits[END_REF][START_REF] Sahai | How to Use Indistinguishability Obfuscation: Deniable Encryption, and More[END_REF]. These definitions are very promising in practice but suffer for now of performances issues.

Taxonomy of Obfuscating Transformations

Far from being exhaustive, this section gives a little insight of the different kinds of existing obfuscation along with various examples.

Control & Data

The main distinguishing feature of an obfuscation is whether it targets the CFG whether it targets its data (variables constants, strings, data structures ..).

Common obfuscation aiming at disrupting the CFG intents to make edges implicit or relying on values known at runtime so that a static analyzer will hardly infer them. Among existing techniques we can note opaque predicates and call/stack tampering discussed respectively in Sections 8.1 and 8.2. There is also code diffusion [START_REF]ReMASTering Applications by Obfuscating during Compilation[END_REF] which intends to maximize some gadgets sharing between functions to blur the distinction between them. Signals, and exceptions uses callback handlers to jump at any location of the program without clearly visible edge. Listing 2.1, taken from a dumb virus Win32.Eva uses an invalid address exception to jump at a given location (example on Figure 2 Listing 2.1: Win32.Eva exception triggered

Obfuscation

As a counterpart to control obfuscation, data obfuscation hides the valuable assets of the program potentially giving hints to the reverser such as cryptographic constant values, imported functions and program strings. A common obfuscation is to cipher strings or sensitive information in the program postponing the deciphering at runtime. Another technique consists in altering data-structures by spliting them, merging scalar values or scrumbling them, using Mixed-Boolean Arithmetic (MBA) [START_REF] Zhou | Information Hiding in Software with Mixed Boolean-Arithmetic Transforms[END_REF]. Finally, let us describe an obfuscation used in some malwares to hide library functions used. It first loads the shared library dynamically, then, given a custom hash function h and the hash value of the function to load H f , the obfuscation will iterate all the library functions and apply the hash function on each function name. If a name s matches the hash values such as h(s) = H f then the obfuscator found the right function. If such obfuscation is used, names are never statically present in the code but only a hash values artifacts. Finally, self-modification is potent enough to hide both resources and the CFG of the program.

Static & Dynamic

Another important characteristic of an obfuscation is to know whether it targets the static code and thus the static analysis or whether it targets the dynamic analysis by triggering the obfuscation at runtime. Static analysis, is highly dependent on the accuracy of the disassembly. Unfortunately, it can easily be fooled by obfuscation techniques as the ones presented hereabove. The disassembly can basically be fooled at three levels [START_REF] Meng | Binary Code Is Not Easy[END_REF]:

• Code discovery. Namely decoding instructions. Indeed, as there is no distinction between code and data, the disassembly can wrongly disassemble data or wrongly left undecoded some code. Malwares are taking advantage of this interleaving to break the decoding process. An example is shown on Figure 2.2 label 3 , where due to a spurious data byte 0x2d IDA wrongly disassembled the code sequence at address 0x40101A. Likewise, code-overlapping [START_REF] Bonfante | CoDisasm: Medium Scale Concatic Disassembly of Self-Modifying Binaries with Overlapping Instructions[END_REF] exploits the fact that instruction are not atomic and some bytes of an instruction decoded separately can take another semantic. Figure 2 Conversely, dynamic analysis sidesteps most static analysis issues as it only goes through executed code. Contrariwise, it requires to deal with anti-debug, anti-tampering and potentially one or more process or threads interacting together. In the same way, due to the dynamic aspect of self-modification, it might be tedious to debug and to locate dynamically generated code. To prevent reverse-engineering, some malicious software are using checksum techniques to prevent any tampering of the code or debugging (as usual breakpoints patch the location by 0xCC to add an INT 3 interruption). The listing 2.3 shows how to compute the CRC of a function chunk in order to check its integrity against a pre-computed HASH value. This example uses the GCC label-as-a-value feature allowing to manipulate label addresses as values in C. As an additional protection, most malwares use anti-VM, anti-debug heuristics not to run in virtual-machine, sandboxes or controlled environement. Figures Needless to say that some techniques like self-modification are potent enough to disrupt both static and dynamic analyses. Notably, self-modification engines that perform polymorphism only when functions are called (on-demand) are very difficult to analyse as the whole code is never available in memory at a given time t.

Protection against symbolic reasoning. There has been very little work on obfuscations trying to circumvent symbolic approaches. Mixed-Boolean Arithmetics are crafted to be hardly targetable by symbolic execution. Two other techniques are used to impede symbolic execution, first hashing functions (hardly reversible) [START_REF] Sharif | Impeding Malware Analysis Using Conditional Code Obfuscation[END_REF] and second linear unsolved conjectures [START_REF] Wang | Linear Obfuscation to Combat Symbolic Execution[END_REF]. The later takes advantage of the difficulty for the symbolic execution to reason about loops. Finally, some works proposed to shadow conditional code obfuscation (input dependent condition) in order to create "secure triggers" [START_REF] Futoransky | Foundations and Applications for Secure Triggers[END_REF]. One famous application of secure triggers based on hashing function is the Gauss malware which payload has never been deciphered so far [START_REF] Goodin | Puzzle Box: The Quest to Crack the World's Most Mysterious Malware Warhead[END_REF].

The obfuscation field is a constantly evolving field with more and more evolved obfuscation mechanisms, enumerating all of them is impossible. Among them, TLB Splitting [START_REF] Torrey | Hardened Anti-Reverse Engineering System[END_REF] uses some processor features to decipher on the fly the code at a location where catching the deciphered code is out of reach for classical debugger and dynamic approaches.

Deobfuscation

Introduction

The term deobfuscation groups all techniques aiming at evading protected described hereabove. It can by caracterized as a two step process: (1) detecting the obfuscation, (2) reverting or deleting it. This later step is potentially harder in practice if not impossible for some obfuscations. Once detected, it worths considering three actions:

• reverting the obfuscating transformation (usually impossible)

• gather relevant information in the obfuscated code • simplifying the obfuscated code to facilitate later analyses My thesis focuses on the last option, and tries to provide automated analyses aiming at clarifying the code in order to help the reverse-engineer. Furthermore, narrowing the spectrum of analyses to the ones addressed in this thesis, we solely focus on approaches explicitely targeting obfuscation (not simply disassembly matters) and using formal methods. Far from being exhaustive, this section gives an overview of existing deobfuscation methods available at the time of study.

Static approaches

Multiple data-flow analyses have been proposed to address obfuscation such as gen/kill, data dependency, alias analysis and abstraction interpretation [START_REF] Nielson | Principles of Program Analysis[END_REF]. The last one can be thwarted by obfuscation such as CFG flattening, as the main loop structure will force abstract interpretation to merge its states leading to very unprecise states. To address this problem in virtualization-obfuscated binaries, Kinder proposed to enrich the abstract lattice with a Virtual Private Counter (VPC) to keep memory states splitted and recover precision [START_REF] Kinder | Towards Static Analysis of Virtualization-Obfuscated Binaries[END_REF]. Also, using abstract interpretation, Preda et al, proposed to address opaque predicates with specific abstract domains modeling the attacker [START_REF] Dalla Preda | Opaque Predicates Detection by Abstract Interpretation[END_REF]. The idea was to refine the domain to get the best detection rate. Various researches are also carried to handle self-modification statically and especially metamorphism by abstract intepretation [START_REF] Preda | Unveiling Metamorphism by Abstract Interpretation of Code Properties[END_REF].

Limits. Static approaches usually assume the CFG availability, no multi-threading and most of the time no self-modifying code. Although, polymorphism is a common practice which breaks many assumptions made by static analysis. We will discuss in later sections how our works tries to address these limitations.

Dynamic approaches

The main interest of dynamic analysis is to address self-modification. In this case the goal is to obtain the program after mutation. A generated piece of code can itself be self-modifying creating some nested layers of polymorphism. A program embedding one another is called packer. Various models of self-modification have been proposed named as waves [GMR09; Uga+15] or phases [START_REF] Coogan | Automatic Static Unpacking of Malware Binaries[END_REF]. As an application, various research studies proposed automatic unpacker tools like Eureka [START_REF] Sharif | Eureka: A Framework for Enabling Static Malware Analysis[END_REF], Polyunpack [START_REF] Royal | PolyUnpack: Automating the Hidden-Code Extraction of Unpack-Executing Malware[END_REF] and Renovo [START_REF] Kang | Renovo: A Hidden Code Extractor for Packed Executables[END_REF] which intend to be generic enough to work on unknown packers.

Another problematic, addressed by dynamic analysis, is cryptographic functions identification [START_REF] Calvet | Aligot: Cryptographic Function Identification in Obfuscated Binary Programs[END_REF]. While static approaches can be made using known constants, dynamic analyses can, for instance, compute the entropy of a function output. A regular distribution of output values could indicate some kind of cryptographic functions.

Limits. The main weakpoint of dynamic analysis is code coverage. Unless, doing fuzzing to cover as many paths as possible, the analysis is used to be performed on a single execution trace, which might not be reproducible. Exception is made by the dynamic tracing tool panda that allow full reproducibility of execution traces. Additionally, the analysis has to deal with all the anti-debugging and anti-tampering tricks used by malware which tends to be an endless cat and mouse game. Eventually, it is sometime simply infeasible to execute the software due to hardware constraints or environment constraints (connecting to a remote host etc). An example is given in Section 10.2.

Symbolic approaches

While existing approaches are essentially divided into static methods and dynamic methods, symbolic approaches offer a valuable balance between both. As a semantic approach, Lakhotia has published a technique named binjuice which aims at extracting a semantic summary of code chunks. Any useless instructions from a semantic point of view would be ignored [START_REF] Lakhotia | Fast Location of Similar Code Fragments Using Semantic 'juice[END_REF]. More in the scope of this thesis, Brumley in 2007 proposed techniques based on DSE to automatically analyse malicious binaries [START_REF] Brumley | BitScope: Automatically Dissecting Malicious Binaries[END_REF]. Very recently Ming [START_REF] Ming | LOOP: Logic-Oriented Opaque Predicate Detection in Obfuscated Binary Code[END_REF] proposed an approach to deobfuscate opaque predicates with DSE. That technique suffers some scalability issues. Lately, Yadegary explored ways to deobfuscate various CFG obfuscations, ROP-based obfuscation and packing using the combination of a bit-level taint and a generic DSE analysis [START_REF] Yadegari | A Generic Approach to Automatic Deobfuscation of Executable Code[END_REF][START_REF] Yadegari | Symbolic Execution of Obfuscated Code[END_REF]. This approaches also suffered some scalability issues due to the size of program analyzed.

Limits. Main limitations of existing symbolic execution approaches is the scalability. Indeed, underlying solvers hardly scale to big programs generating numerous constraints. As a consequence, it is thus essential to lighten the computation load of solvers in order to make symbolic execution based deobfuscation.

Chapter 3

Dynamic Symbolic Execution

Introduction

Symbolic Execution (SE) is a popular and fruitful formal approach to automatic (codebased) software testing. Given a path in a program, the key insight of Symbolic Execution (SE) is the possibility in many cases to compute a formula (a path predicate) such that a solution to this formula is a test input exercising the considered path. Then, exploring all the (bounded) paths of the program allows intensive testing.

Basis were laid in the 70's by King [START_REF] King | Symbolic Execution and Program Testing[END_REF], but the technique found a renewal of interest in the mid 2000's [START_REF] Cadar | Symbolic Execution for Software Testing: Three Decades Later[END_REF] when it was mixed with concrete execution [SMA05; Wil+05] and combined with the growing efficiency of Satisfiability Modulo Theories (SMT) solvers. SE has quickly become the most promising technique for code-based automatic test generation, and has led to impressive case studies [Avg+14; Cad+11] and a promise of industrial adoption at large scale [START_REF] Godefroid | SAGE: Whitebox Fuzzing for Security Testing[END_REF]. Its usage for security purposes has also been considered, thanks to its straightforward adaptation to binary-level analysis [START_REF] Bardin | OSMOSE: Automatic Structural Testing of Executables[END_REF][START_REF] Song | BitBlaze: A New Approach to Computer Security via Binary Analysis[END_REF]. SE has successfully been applied in a wide range of security applications such as vulnerability discovery [Avg+11; HG12] and malware analysis [START_REF] Brumley | BitScope: Automatically Dissecting Malicious Binaries[END_REF], the topic of this thesis.

DSE Dynamic Symbolic Execution [SMA05;

Wil+05] also known as concolic execution takes advantage of a concrete execution path to perform the computation. It provides the following advantages:

• the sound execution of the program. The path is sure to be feasible in practice,

• the next instruction executed is always known. This property is particularly helpful at binary-level when dealing with indirect/computed jumps or instructions potentially raising exceptions,

• by design, all the loops are unrolled.

The main drawback is that the trace followed is an under-approximation of the program execution which is inputs dependent. At this point, unless specified otherwise, the term Symbolic Execution will be used for Dynamic Symbolic Execution.

Concolic engines. This study led to the development of Binsec/se [Dav+16b] a full featured DSE engine. Yet, several other initiative already exists at binary-level like Mayhem [START_REF] Cha | Unleashing Mayhem on Binary Code[END_REF] built at the top of the Binary Analysis Platform [START_REF] Brumley | BAP: A Binary Analysis Platform[END_REF]. We can also note S2E [START_REF] Chipounov | The S2E Platform: Design, Implementation, and Applications[END_REF] based on KLEE [START_REF] Cadar | KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs[END_REF], Triton [START_REF] Saudel | Triton: A Dynamic Symbolic Execution Framework[END_REF], Angr [START_REF] Shoshitaishvili | SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis[END_REF] and the closedsource ConcoLynx [START_REF] Yadegari | Symbolic Execution of Obfuscated Code[END_REF].

Binary-level semantic: DBA

At binary level, to avoid dealing with all the instructions set of all the architectures analyses are usually developped on intermediate representation. An intermediate provides a concise set of instructions encoding the semantic of instructions. Thus, an analysis designed on such intermediate representation is meant to work regardless of the backend architecture x86, ARM etc. DBA for Dynamic Bitvector Automata [START_REF] Djoudi | BINSEC: Binary Code Analysis with Low-Level Regions[END_REF] is defined as an intermediate representation of assembly instructions, working on a subset of instructions independents from the architecture. Similar languages provide such functionalities like BIL [START_REF] Brumley | BAP: A Binary Analysis Platform[END_REF], VEX, REIL [START_REF] Dullien | REIL: A Platform-Independent Intermediate Representation of Disassembled Code for Static Code Analysis[END_REF]. Advantages of DBA like most other IR is a side-effect free and bit-precise language. DBA has the advantage of providing higher-level instruction design for program analysis like assert, assume or malloc, f ree. The shortcomings are the lack of floating-point instruction modeling, the lack of thread, exception and the lack of self-modification modeling in the language.

Expressions & Types

All scalar variables are represented as bitvector bv ∈ Bv, a list of bits for which the size is statically known. The memory M em is represented as bitvector addressed with the operator @ which represents both read and write operations depending whether it is used in the left-hand side (lhs) of an assignement instruction or not.

Expressions represent bit-level operations performed on bitvectors. An expression e ∈ Expr can be a bitvector value bv a variable v ∈ V ar typically registers or the composition of operations on these two, like unary and binary operations repespectively ♦ u and ♦ b . At the top of that, two specific values ⊥ and defines respectively an undefined value and a non-deterministic value. ⊥ is used to represent undefined behaviors like some flags on certain operations in x86. represent a non-deterministic value. Table 3.1 gives the grammar of expressions.

Intermediate Langage

A program P, is defined by a map ∆ from location to instructions: ∆ : loc → Instr. The core language is composed of basic instructions like assignement, both static, conditional and dynamic jumps and an ending instruction. We denote Σ a concrete memory state. Σ is a complete function mapping each variable v ∈ V ar to a value bv ∈ Bv and mapping variable M em to an array such as: Bv {addr_size} → Bv {8} . The operational semantic is defined such that an instruction updates the memory state and the current location accordingly.

v ∈ V ar ♦ u ::= -| ¬ ♦ b ::= + | -| × | / u,s | % u,s | | && | ⊕ | u,s | | :: | < u,s | ≤ u,s | = | = | > u,s | ≥ u,s e ::= e ♦ b e | ♦ u e | @[ e ] | v | bv | ⊥ |
At the top of the core language, DBA includes various annotations and utilitarian instructions, aiming at modeling specific behavior and used for analysis specific purposes. For instance, malloc and f ree are used to model an allocation and a "free" in memory. Similarly, assert and assume can be used afterward depending on the analyses.

Assembly instructions are highly likely to be decoded as multiple instructions sharing the same address in the program and forming a DBA block denoted B. Instructions within a block are ordered using an id ∈ N allowing to pinpoint each of them separately. Within a block, an instruction can jump to any instructions, but the language enforces jumps accross instructions to be performed on blocks entrypoint. Thus, any instruction in the program is addressed by l ∈ loc such as loc ∈ (Bv {addr_size} × N). The complete grammar is given in table 3.2. A condition c is defined as an expression that evaluates to a bitvector of size 1 written Bv {1} . Table 3.

Usages

As a starter, Listing 3.1 gives the DBA semantic decoding of the imul eax, dword ptr [esi + 0x14], 7, instruction in x86. As a first advantage, using such modeling allows a more simple syntactic processing. Indeed, it is easier to match for instance an instruction assigning a given register rather than having to deal with the entire instruction set of the architecture with all possible parameters.

In terms, of static analysis DBA is being used as an intermediate representation semantic for abstract interpretation, simulation or high-level predicate recovery [START_REF] Djoudi | Recovering High-Level Conditions from Binary Programs[END_REF] within the Binsec platform and we use it for symbolic execution in this thesis.

res32 := ( @ [( esi (32) + 0 x14 (32) )] × (s) 7 (32) ) temp64 := (( exts @ [( esi (32) + 0 x14 (32) )] 64) × (s) ( exts 7 (32) 64)) OF := ( temp64 (64) = ( exts res32 (32) 64)) SF := ⊥ ZF := ⊥ CF := OF (1) eax := res32 (32)
Listing 3.1: imul eax, dword ptr [esi + 0x14], 7

Definitions

Path predicate

Given a program P over a vector V of input variables taking values in a domain D D 1 × . . . × D m , a test datum t for P is a valuation of V , i.e. t ∈ D. The execution of P over t, denoted P (t), is a path (or run) π (l 1 , Σ 1 ) . . . (l n , Σ n ), where the l i denote control-locations (or simply locations) of P and the Σ i denote the successive internal states of P (i.e valuation of all global and local variables as well as memory-allocated structures) before the execution of each l i .

Definition. ϕ is a path predicate for π if for any input valuation t ∈ D, t satisfies ϕ iff P (t) covers π.

Correctness ϕ is said to be correct if any solution covers the path π. Completness ϕ is complete if any input covering the path π is a solution.

program path predicate ϕ 1 concretization ϕ 2 symbolization ϕ 3 inputs: a, b a = 5 x := a × b x 1 = a × b x 1 = 5 × b x 1 = f resh x := x + 1 ∧ x 2 = x 1 + 1 ∧ x 2 = x 1 + 1 ∧ x 2 = x 1 + 1 //assert x > 10 ∧ x 2 > 10 ∧ x 2 > 10 ∧ x 2 > 10

Definitions

A path predicate is intuitively the logical conjunction of all branching conditions and assignments encountered along that path. Figure 3.1 presents a simple program path (two assignments and a branching condition x > 10 taken to true) together with three possible path predicates for that path. It is straightforward to check that ϕ 1 is correct and complete (a valuation of a and b satisfies ϕ 1 iff their execution satisfies the assertion). ϕ 2 is correct but incomplete due to the additional constraint a = 5 added by the concretization and ϕ 3 is complete but incorrect because of the symbolization that removed the constraint

x 1 = a × b (f resh is a new unconstrained variable) .

Symbolic Execution

Let's consider the set of finite1 paths of a program P denoted Π P . A symbolic algorithm builds iteratively a set of tests by exploring all the feasible paths. The three major components of the SE algorithm are the following:

• Sel, a path selection strategy, aiming at choosing the most appropriate path to explore for the intented analysis. This function is defined by: Sel : Π P → π

• C, the path predicate computation function. It computes the predicate of the path in some predefined theories denoted by T . In our case in the bitvector and array (see. Section 6.4). This function is defined by: C : π → ϕ

• Sol, the satisfiability checking using an automatic solver. This function takes a formula φ ∈ Φ with Φ ⊂ T and returns either sat with a solution t (i.e a test input) or unsat without solution. Formally we note Sol T : Φ → (sat, t) (unsat, ∅) the satisfiability function that checks a formula in the given theory T . Note that most SE tools rely on Off-The-Shelf (OTS) solvers (see. Section 6.4).

Therefore, we can define the symbolic execution algorithm in its entirety.

Definition For a program P and a set of finite paths Π P , the symbolic execution algorithm denoted F DSE is defined by:

F DSE : (Sel • C • Sol)(Π P )
Algorithm 1 shows how the Symbolic Execution algorithm works with its three components, the path selection function (line 4), the path predicate computation (line 3) and the solving function (line 6).

Dynamic Symbolic Execution enhances SE by interleaving concrete and symbolic execution. The dynamically collected information can help the three main DSE operations

Sel, C and Sol by adjusting and choosing the relevant approximations (cf. Figure 3.1 and Chapter 4). Its direct impact is on the sets of paths Π P that is created by concrete execution of the program. The underlying property that appears is that the path predicate is meant to be satisfiable. Otherwisely said ∀ π ∈ Π P , ϕ sat, or more formally:

∀π ∈ Π P , ∃ t ∈ D such that (C • Sol)(π) = SAT, t

Path predicate computation

Intuitively, the path predicate computation is similar to concrete execution, except that the computation is performed on logical formulas rather than on concrete values. We denote by Σ * the symbolic memory state which maps all variables v ∈ V ar to symbolic values ϕ (logical terms on logical variables ranging over Bv) and the distinguished variable M em to a logical array from addresses to bytes. The path predicate ϕ is a first-order logic formula over logical variables and logical arrays. At a given point of execution, the internal state of the algorithm is composed of l, Σ * , ϕ, respectively a location, a symbolic memory state and the current path predicate. The algorithm starts from the initial location l 0 , the initial state Σ * 0 associating a fresh logical variable to each program variable and a fresh logical array to M em, and ϕ 0 true. It then proceeds instruction by instruction along the execution. At the end the computed path predicate ϕ is returned. These notations are summarized in table 3.3.

Recall that the execution trace being fixed, the successor of each branching instruction is known. The operational semantic of the path predicate computation algorithm over DBA is given in Figure 3.2 where represents path predicate computation itself while e represents the symbolic evaluation of a DBA expression. For instance, rule var Σ * ,v eΣ * (v) states that the symbolic evaluation of variable v is the symbolic value stored for v in the current symbolic memory state Σ * , denoted Σ * (v). Rule l -goto e Σ * ,e eϕe ϕ ϕ∧to_addr(le)=ϕe l,Σ * ,ϕ,goto e le,Σ * ,ϕ ,∆(le) allows the symbolic evaluation of a dynamic jump branching to location l e . The rule reads as follows: expression e is symbolically evaluated into the symbolic value ϕ e and location l e which is converted to a concrete The execution environment defined by : l, Σ * , ϕ address with to_addr : loc → Bv. Thus, the constraint to_addr(l e ) = ϕ e is added to the path predicate modeling the fact that the execution flow must jump to l e to ensure soundness. Remaining unexplained symbols are:

• the symbols gathered into ♦ * u and ♦ * b are the logical counterparts of the unary and binary symbols of concrete expressions, e.g "+" is evaluated to the logical operator bvadd of the bitvector theory;

• select/store are the standard logical operators from the theory of arrays, representing the readings and writings to specific array indexes;

• f resh designates a new logical variable in the formula.

Property 1. The path predicate computation algorithm of Figure 3.2 is correct and complete, i.e. it returns a correct and complete path predicate.

This concludes the chapter recalling background notations and definitions about dynamic symbolic execution. This lays the basis for the algorithms improvements formalized in the next Part (II).

Expr : cst Σ * , bv e bv var Σ * , v e Σ * (v) binop Σ * , e 1 e ϕ 1 Σ * , e 2 e ϕ 2 ϕ ϕ 1 * b ϕ 2 Σ * , e 1 b e 2 e ϕ unaryop
Σ * , e e ϕ e ϕ * u ϕ e Σ * , u e e ϕ @ Σ * , e e ϕ Σ * , @ e e select(Σ * (M em), ϕ)

Instr : goto l 1 l, Σ * , ϕ, goto l 1 l 1 , Σ * , ϕ, ∆(l 1 ) l e -goto e Σ * , e e ϕ e ϕ ϕ ∧ to_addr(l e ) = ϕ e l, Σ * , ϕ, goto e l e , Σ * , ϕ , ∆(l e ) T -ite Σ * , e e ϕ e ϕ ϕ ∧ ϕ e = true l, Σ * , ϕ, ite(e) : l 1 ; l 2 l 1 , Σ * , ϕ , ∆(l 1 ) F -ite Σ * , e e ϕ e ϕ ϕ ∧ ϕ e = f alse l, Σ * , ϕ, ite(e) : l 1 ; l 2 l 2 , Σ * , ϕ , ∆(l 2 )
var assign

Σ * , e e ϕ e Σ * new Σ * [v ← f resh] ϕ ϕ ∧ f resh = ϕ e l, Σ * , ϕ, v := e l + 1, Σ * new , ϕ , ∆(l + 1) @ assign Σ * , e e ϕ e Σ * , e e ϕ e Σ * new Σ * [M em ← f resh m ] ϕ ϕ ∧ f resh m = store(Σ * (M em), ϕ e , ϕ e ) l, Σ * , ϕ, @ e := e l + 1, Σ * new , ϕ , ∆(l + 1) stop l, Σ * , ϕ, stop return ϕ

Part II

Dynamic Symbolic Execution Extensions

Chapter 4

Concretization/Symbolization cost modulation

This chapter introduces a new DSE algorithm allowing to modulate in a flexible manner concretizations and symbolizations performed during the symbolic execution. This is made possible via the formalization of C/S policies integrated into a rule-based language CSml and implemented in Binsec/se. Benchmarks performed shows a negligible time overhead while proving the usefulness of such a flexible mechanism.

Introduction

Problem While a purely symbolic approach is worth considering, the strength of modern SE tools is to symbolically evaluate only a (small) trace fragment. Concretization uses run-time values in order to under-approximate the path predicate, while symbolization over-approximate the path predicate by introducing new logical variables. The former allows to handle in a precise but limited way parts of an execution which are either missing (e.g. system calls) or too costly to reason about (e.g. cryptographic functions), while the latter allows to generalize certain program steps, keeping the reasoning exhaustive but less precise.

Actually, choices of concretization and symbolization (C/S) are a crucial part of modern SE tools, together with path predicate computation and path selection. Yet, while the latter are either well-understood (path predicate) or under active research efforts (path selection), C/S policies have been much less studied. Especially, design choices behind implemented C/S policies are often barely explained, and most SE tools either propose only hard-coded C/S policies, or give full control on a line per line manner in the code [START_REF] Chipounov | The S2E Platform: Design, Implementation, and Applications[END_REF].

Goal and contributions

We propose to address these problems through a clear separation of concerns between (1) a specification mechanism for C/S policies in SE, and ( 2) a new SE algorithm parametrized by an arbitrary C/S policy specification as sketched in Figure 4.1.

• We formalize what a C/S policy is and we revisit the standard path predicate computation algorithm taking C/S policy into account (Section 4.2.1). This is the first time such a parametric view of the core algorithm behind SE is provided. We clearly show where the C/S policy matters and we discuss correctness issues.

• We propose CSml, a rule-based specification language for defining C/S policies, together with its semantics (Section 4.3). The language is simple, yet powerful enough to encode standard C/S policies. Again, correctness issues are discussed.

• As a second application, these results have been implemented on top of the Binsec framework [START_REF] David | BINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis[END_REF], yielding the first SE tool with fully customizable C/S policies through high-level specifications (Section 4.4). First experiments demonstrate that the overhead induced by this genericity is very low (Section 4.5).

• Finally, we present the first quantitative comparison of C/S policies (Section 4.5.1), focused on policies dedicated to the handling of memory operations. We compare five policies on 169 programs. We found that, while new policy PP* performs better on most examples, there is still a high variability of results between the policies depending on the considered example. This is a strong a posteriori argument for a generic C/S specification mechanism. (2) the systematic study of concretization and symbolization (including both analytic and quantitative analysis) in order to better understand their impact and to identify interesting trade-offs; and finally (3) the finetuning of dedicated policies tailored to specific programs or needs.

State of the Art

Most SE tools implement a single hard-coded built-in C/S policy, which can favor either scalability (i.e., by considering most values as concrete) or completeness (i.e., by keeping more symbolic values). For instance, the pioneering tools DART [START_REF] Godefroid | DART: Directed Automated Random Testing[END_REF] and CUTE [START_REF] Sen | CUTE: A Concolic Unit Testing Engine for C[END_REF] fall in the former category (memory addresses, results from external library calls and part of non-linear expressions are concretized), while PathCrawler keeps the computation fully symbolic [START_REF] Williams | PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis[END_REF] and EXE [START_REF] Cadar | EXE: Automatically Generating Inputs of Death[END_REF] stands in between. More recent engines can even build on more sophisticated heuristics in the hope of reaching a sweet spot between scalability and completeness, typically based on tainting [HG12; SAB10] or dataflow analysis [START_REF] Cha | Unleashing Mayhem on Binary Code[END_REF]. We showed in Section 4.3.4 how such policies can be specified in CSml.

Definitions

Let's define the three decisions that can be taken on an expression during the path predicate computation.

Concretization (C) uses run-time values in order to

Path predicate correctness

While performing DSE, we might be driven into ignoring some functions not executing them symbolically or to ignore some instructions not decoded in the intermediate representation. While in practice, it helps to narrow the computation to the main code of interest, it might also yield incorrect path predicates. Rarely, it can be due to a bad encoding of the instruction semantic in the given IR. • a sat-decoherence. is a decoherence breaking the execution soundness while keeping a satisfiable path predicate. In the example Figure 4.2, if considering a simple logical propagation (P), it is expected that pop esi will get the value pushed on the stack by push esi. However, in the path predicate we have:

Definition 1. The decoherence or loss of correctness of the path predicate is the phenomenom by which logical values are being made incorrect w.r.t the program execution due to unhandled semantic side-effect of the original program execution.

... inputs:esp0, esi0 @0 push esi @[esp-4] := esi @[esp0 -4] = esi0 esp0 -4 = 0x42 esp := esp -4 ∧ esp1 = esp0 -4 @1 call myfun esp := esp-4 ∧ esp2 = esp1 -4 esp2 = 0x3e @[esp] := @2 ∧ @[esp2] = @2 goto @myfun [FUNCTION CODE EXECUTION SKIPPED] @2 pop esi esi := @[esp] ∧ esi1 = @[esp2] esp2 = 0x42 esp := esp+4 ∧ esp3 = esp2 + 4
@[esp0 -4] = @[esp2] @[esp0 -4] = @[esp1 -4] ⇔ @[esp0 -4] = @[esp0 -8] ⇔ =⇒ sat
The load is performed at the wrong offset. But, as this offset is not constrainted, the path predicate is still sat.

• an unsat-decoherence. is an excecution soundness loss which turn the path predicate to be unsatisfiable. In the example Figure 4.2, if we concretize the load and store addresses we obtain more path constraints (last column). When comparing the logical addresses of the load and store we have:

esp0 -4 = 0x42 ∧ esp2 = 0x42 esp0 = 0x3e ∧ esp1 -4 = 0x42 ⇔ esp0 = 0x3e ∧ esp1 = 0x3e ⇔ esp0 = 0x3e ∧ esp0 -4 = 0x3e ⇔ esp0 = 0x3e ∧ esp0 = 0x3a ⇔ =⇒ unsat
The esp0 cannot hold two different values in the same time, thus the path predicate is unsat. (we also have esp2 = 0x3e ∧ esp2 = 0x42 trivially unsat).

C/S policy introduction

Both concretization and symbolization allow to make SE more robust to real programs, through improving practical solvability. It can also tremendously reduce the decoherence phenomenom described in the previous section. Yet, they come at the price of losing either completeness (concretization) or correctness (symbolization). The decision upon which a value is concretized or symbolized is in general hard-coded inside the path predicate computation of existing tools. Our goal, is precisely designing a flexible and clear specification mechanism for such decisions.

Let's consider the instruction x := @[a×b] for which a and b had respectively values 7 and 3 at runtime. The logical formula associated with that instruction would be x = select(M, a × b) where M is a logical variable representing the memory. Intuitively, a C/S policy defines what actions are to be performed in terms of concretization and symbolization for that instruction. Assuming we want to concretize read operations in memory there is at least three ways to perform it:

• [incorrect] x = select(M, 21) is incorrect as the property a × b = 21 is lost • [minimal] x = select(M, 21) ∧ a × b = 21 • [atomic] x = select(M, 21) ∧ a = 7 ∧ b = 3
While [minimal] and [atomic] seem equivalent, [atomic] forces the values taken by a and b while [minimal] can still choose a and b as long as the product is 21. In addition [minimal] does not get rid of the × operator, which can come at cost for more complex operators or simply if the underlying theory used does not support it. None of these three policies is clearly the best, all depend on the context hence the need for a clear specification is required.

DSE algorithm with C/S modulation 4.2.1 C/S policy enriched DSE algorithm

As recall, the goal of a C/S policy is to decide whether a given expression should be propagated (P) the normal behavior as in the standard algorithm (cf. Figure 3.2), concretized (C) hence replace by its runtime value or whether it should be symbolized (S) hence replaced by a f resh (unconstrainted) symbol. We reuse here, all the notations used in the Chapter 3 about symbolic execution background.

We denote ρ {C, S, P} the set of possible decisions and State the set of concrete memory states. We define a C/S policy csp_expr as a function that takes as input a location l ∈ loc, an instruction i ∈ Instr, a concrete memory state Σ and an expression e ∈ Expr, and returns a decision d ∈ ρ. Formally:

csp_expr : loc × Instr × Expr × State → ρ
Path predicate computation with C/S policy The C/S policy is queried inside the path predicate computation algorithm each time an expression must be evaluated. Intuitively, the standard algorithm given in Figure 3.2 is the case where the decision is always propagate (P), starting from an initial state where all variables are symbolic.

A version of the path predicate computation algorithm revisited for taking C/S policies into account is presented in Figure 4.3. The main difference with the standard approach is that, the symbolic evaluation operator e is slightly modified to cs • to use the policy. This operator now returns a symbolic expression together with a formula to be added to the current path predicate. Thus, before evaluating an expression, csp_expr(l, i, e, Σ) is queried in order to know which action shall be performed on it (lower part of Figure 4.3):

• S: the expression e is replaced by a new symbol;

• P: the expression e is logically evaluated, applying the C/S policy on each sub-terms [with cs • ];

• C: the expression e is logically evaluated [with cs • ], then the resulting logical expression is constrained to be equal to the concrete evaluation eval Σ (e) of e, in order to preserve correctness of concretization.

Note that cs • [and cs • ] return both a symbolic expression and a formula, the latter representing the constraints potentially induced by concretizing some subterms of the expression to evaluate.

The semantic defined in 4.3 yields various interesting properties:

Property 2. An execution with the P policy is strictly equivalent to the standard DSE semantic depicted in Chapter 3.

Property 3. A policy using P and C keeps the correction but loses the completness.

Property 4. A policy using P and S keeps the completness but loses correction.

CSML: C/S Specification Langage

The main goal is to design a high-level specification language for C/S policies able to encode major policies found in the literature (see. Section 4.3.4). Especially we want to distinguish between [incorrect], [minimal] and [atomic]. Besides expressiveness, the following properties are also desirable: (1) a clear semantics; (2) simplicity and concision; (3) independence from the code under analysis or from a particular SE tool; (4) "executability", meaning we want to synthesize the code enforcing a C/S policy from its specification in order to use it in a SE tool.

We achieve these goals through CSml, a high-level rule-based language offering various functionalities like pattern matching or subterm checking on the instruction and expression being processed. That language can be integrated in the modified DSE algorithm formalized in the previous Section 4.2.1.

Expr : cst Σ * , bv cs • bv, true var Σ * , v cs • Σ * (v), true binop Σ * , e 1 cs • φ 1 , ϕ 1 Σ * , e 2 cs • φ 2 , ϕ 2 Σ * , e 1 b e 2 cs • φ 1 * b φ 2 , ϕ 1 ∧ ϕ 2 unaryop Σ * , e cs • φ e , ϕ e φ * u φ e Σ * , u e cs • φ , ϕ e @ Σ * , e cs • φ e , ϕ e φ select(Σ * (M em), φ e ) Σ * , @ e cs • φ, ϕ e Instr : goto l 1 l, Σ * , ϕ, goto l 1 l 1 , Σ * , ϕ, ∆(l 1 ) l e -goto e Σ * , e cs • φ e , ϕ e ϕ (ϕ ∧ ϕ e ∧ to_addr(l e ) = φ e ) l, Σ * , ϕ, goto e l e , Σ * , ϕ , ∆(l e ) T -ite Σ * , e cs • φ e , ϕ e ϕ ϕ ∧ ϕ e ∧ φ e l, Σ * , ϕ, ite(e) : l 1 ; l 2 l 1 , Σ * , ϕ , ∆(l 1 ) F -ite Σ * , e cs • φ e , ϕ e ϕ ϕ ∧ ϕ e ∧ ¬φ e l, Σ * , ϕ, ite(e) : l 1 ; l 2 l 2 , Σ * , ϕ , ∆(l 2 )
var assign

Σ * , e cs • φ e , ϕ e Σ * new Σ * [v ← f resh] ϕ (ϕ ∧ ϕ e ∧ f resh = φ e ) l, Σ * , ϕ, v := e l + 1, Σ * new , ϕ , ∆(l + 1) @ assign Σ * , e cs • φ, ϕ e Σ * , e cs • φ , ϕ e m store(Σ * (M em), φ , φ) ϕ m (ϕ ∧ ϕ e ∧ ϕ e ∧ f resh m = m ) l, Σ * , ϕ, @ e := e l + 1, Σ * [M em ← f resh m ], ϕ m , ∆(l + 1) Σ * , e cs • :      f resh, true if ρ = S φ e , ϕ e if ρ = P, Σ * , e cs • φ e , ϕ e C φ , ϕ e ∧ (C φ = φ e ) if ρ = C, Σ * , e cs • φ e , ϕ e and C φ eval Σ (e)      ρ csp_expr(l, i, e, Σ)
Instruction, location l and concrete state Σ are propagated inside all cs • rules, but we omit it for clarity.

Language specification

We now describe CSml, our rule-based language whose syntax is given in Table 4.1. It allows a scalable level of description from the generic high-level policy to a precise and highly targeted one.

Basic principles A rule is of the form guard ⇒ ρ where the guard allows to check if the rule should be fired (typically using pattern-matching and subterm checks) and ρ is the decision to be returned by the policy. As explained before, rules are queried with the current location, instruction, expression and concrete memory state. Namely, guards are denoted by φ loc :: φ ins :: φ expr :: φ Σ , where:

• φ loc is a predicate on the location,

• φ ins is a predicate on the instruction,

• φ expr is a predicate on the expression,

• φ Σ is a predicate on the concrete memory state.

Rules are tested sequentially, and the first matching rule returns its associated action. If no rule gets triggered, then a default rule is applied. In each rule, guard predicates are also checked sequentially, so that φ loc must be satisfied in order to check φ ins and so on. Note that any of these predicates can be replaced by a wildcard * , which always evaluate to true. Finally, guard predicates may communicate in a limited way through meta-variables and placeholders. . expr + : extended expression, allowing placeholders (!) . pexpr: expr. pattern, allowing placeholders (!) and meta-variables (?) . instr + and pinstr: the same w.r.t. instructions

Matching and meta-variables

Predicates for φ expr and φ ins typically allow to check if the input expression (resp. instruction) matches a given pattern pexpr (resp. pinstr).

A pattern is similar to an expression (resp. instruction), but with two additional kinds of variables.

Meta-variables (prefixed by "?") allow to match any term. Once successfully matched, these terms become available as placeholders in the subsequent guard predicates. When a meta-variable does not need to be reused, one can employ an anonymous meta-variable ? .

Placeholders (prefixed by !) take the value of their corresponding meta-variable (e.g., ?e for !e) once matched. The distinguished placeholder ! contains the current expression being processed. Given a pattern p, we denote the predicate "match p?" by p . As an example, we concretize the expression being added to esp, in any assignment instruction: * :: ? := esp + ?e :: !e :: * ⇒ C Here, ?e is defined in φ ins and then available in φ expr through !e. The rule reads as follows: if the current instruction assigns the sum of esp and some expression e (being captured by the meta-variable ?e) to any lhs (meta-variable ? ), and the current expression matches e, (predicate !e ), then it should be concretized. Or, put another way: if we are evaluating an expression e in the context of an instruction where e is added to esp and assigned to some lhs, then e should be concretized.

Another example, slightly more complex is given in the table 4.2. This policy means: "if we are evaluating an expression e in the context of an assignment where e is used as the write address, then e is concretized, otherwise it is propagated." Subterm This language is already quite expressive, but still does not allow to match a nested sub-expression depending on its context. The typical usage is, when willing to concretize a read address, we want to know if the given expression is in the scope of a read operation. This can be solved by introducing the operator (resp. ≺), allowing to check if an expression is a subterm (resp. strict subterm) of another one. The rule specifying that any read or write expression must be concretized is written: * :: ?i :: (@ ! ) ≺ !i :: * ⇒ C

In this rule ?i matches a whole instruction.

The rule can be read as follows: when evaluating an expression e (given by the special placeholder ! ) such that the expression @e is a subterm of the current instruction (captured by ?i) then e should be concretized. Note that ≺ and can be applied to (extended) terms containing placeholders (expr + and instr + in Table 4.1).

Other predicates φ loc consists in checking that the input location l is either equal to a given location loc or within a range of locations [loc..loc']. φ Σ is a predicate over Expr that can query information from Σ. For example, we can imagine performing some concretization and/or symbolization depending of the runtime value of the expression being evaluated. φ Σ will be lightened in the next section with extended memory states.

CSml properties

CSml ensures interesting properties on the C/S policy being defined. In order to present them, we need a few additional definitions. A CSml rule is said to be welldefined if it is well-typed and if placeholders are used in an appropriate manner. Note that the well-definedness of a rule is automatically checkable. A C/S policy is well-defined if it is a total function (deterministic behavior, defined on any input), and it is correct if it leads to the computation of a correct path predicate (cf. Section 3.4). Then, by construction, we have the good following properties2 : Property 5. A set of well-defined CSml rules defines a well-defined C/S policy. Property 6. A set of well-defined CSml rules employing only C and P defines a correct C/S policy.

Advanced Features

We propose here several useful extensions to the CSml core language.

Richer decisions We enrich the set of possible decisions by allowing a domain restriction on both S and P, now denoted S D and P D , where D is an interval constraint (resp. singleton constraint) of the form [a..b] (resp. [a]) with a and b expressions evaluating to bitvector values. This feature is useful typically for limiting the domain of a fresh logical variable, but it can also be used to encode incorrect concretization or restricted propagation (cf. below). Note that the domain does not need to be defined by constant values, for example its definition can involve runtime evaluation of bitvector expressions, through function eval Σ : Expr → Bv • incorrect concretization of r/w expressions [incorrect] * :: ?i :: (@ ! ) ≺ !i ::

* ⇒ S [eval Σ (! )]
• restriction of r/w expressions [BH11] * :: ?i :: (@ ! ) ≺ !i ::

* ⇒ P [eval Σ (! )-10..eval Σ (! )+10]
Richer subterm constraints We allow chaining of subterm constraints, e.g. e ≺ pe 1 ≺ . . . ≺ pe n ≺ term + , together with the use of anonymous meta-variables inside the pe i . This allows finer subterm relationship, such as checking that an expression is a subterm of an expression pattern, used itself within another expression.

• recursive concretization of r/w expressions: * :: ?i :: ! ≺ (@ ? ) ≺ !i :: * ⇒ C

Compared with [minimal] concretization, this rule enforces the concretization of all subterms of a r/w expression. This policy is also slightly different from atomic concretization CS3 which encoding is shown hereafter.

Richer predicates

We can also allow more predicates in the language. This can be done at two stages: either enriching the four classes of predicates already defined, or adding new classes of predicates. For the first category, it could be useful to have a var predicate indicating if a term is a variable or not. An application is to restrict concretization to atomic variables:

• atomic concretization of r/w expressions [atomic] * :: ?i :: var(! ) ∧ ! ≺ (@ ? ) ≺ !i :: * ⇒ C For the second category, it could be useful to consider a predicate class φ step regarding the step of the execution, allowing for example to define a C/S policy step by step in a trace-oriented manner, which may sometimes come handy.

Extended memory states

In the same vein, it can be interesting to enrich the predicate φ Σ working on a concrete memory state Σ into a predicate φ Σ + working on an extended concrete memory state Σ + . Basically, an extended concrete memory state is a concrete memory state enriched with additional runtime information collected. A typical example of such a predicate is T Σ + (e), indicating whether an expression e is tainted or not in a given extended memory state Σ + , using dynamic taint information [START_REF] Schwartz | All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)[END_REF].

Note that this extension makes the C/S policy dependent on the services provided by the underlying dynamic execution engine. While it is fair to assume that a concrete evaluation function eval Σ is available on any dynamic execution engine, more exotic queries on Σ + may not be available. We assume that C/S policies querying unsupported Σ + -function (or Σ + -predicate) are syntactically rejected.

C/S injection Besides C/S at the level of symbolic evaluation, another common pattern is to enforce concretization and/or symbolization through direct modification of the symbolic memory state. This is particularly useful to handle unknown or hard-to-reasonabout functions (e.g. system calls, cryptographic function) with side-effects or returning complex data structures. Note that this kind of C/S is different from the one we have considered so far, since it modifies permanently the value of a lhs (inside Σ + ), while csp_expr affects a single evaluation of any expression. For example, C/S injection allows to declare that at some location, variable eax receives a fresh value (which will last along the trace until eax is rewritten), while csp_expr allows to declare that at some location, variable eax evaluates as if it were unconstrained (with no impact on the remainder part of the trace). C/S injection can be handled similarly to C/S in expression evaluation. Due to space limitation, we only sketch the idea. Contrarily to csp_expr, concretizations defined by csp_mem are not ensured to be correct, as the symbolic memory state is modified without any additional (correctness) constraint. We thus denote it Sc. We introduce a new function:

csp_inject : loc × Instr × State → (lhs → {Sc, S})
which takes as argument a location, an instruction and a symbolic state, and returns a map from lhs to decisions, which are here limited to C and S. Intuitively, the map represents the modifications which have to be performed on the current symbolic memory state Σ * before the symbolic execution goes on.

Discussion Altogether, these extensions provide a very fine control over the C/S policy, allowing for example to encode the subtle differences between correct concretization, incorrect concretization, recursive concretization and atomic concretization.

Application:Encoding Standard C/S Policies

To illustrate how our language works, we show the encoding of several state-of-the-art policies from the literature, not yet covered in previous sections.

For instance, CUTE and DART [GKS05; SMA05] concretizes both read and write addresses, as well as part of non-linear operations (here: left operand of any × operator). The associated policy is shown in Table 4

:: ¬ T Σ + (! ) ⇒ C default ⇒ P
The approach followed in EXE [START_REF] Cadar | EXE: Automatically Generating Inputs of Death[END_REF] in case of multi-level dereferencement consists in concretizing all r/w expressions but the most nested one. The encoding of such a policy is shown in Table 4.5. Table 4.5: EXE policy * :: ?i :: (@ ! ) ≺ (@ ? ) ≺ !i :: * ⇒ C default ⇒ P

It is important here to use ≺ rather than

Finally, the policy in Mayhem [Avg+16; Cha+12] consists in concretizing all write expressions while keeping read expressions symbolic as long as they cannot take too many values (otherwise, concretizing them). We need here to consider Σ + enriched with an interval analysis. The encoding is then given in Table 4.6, where card I (e) gathers the number of possible values for e from the interval information available in Σ + . 4.7 presents a summary of the kinds of C/S policies CSml can encode, together with the required extension of the language. It is remarkable that CSml can encode all popular C/S policies despite a limited language. Hence, we think that our rule-based language manage to capture the crucial aspects of current C/S policies.

Limits

We do not know of any major existing C/S policy that cannot be encoded into CSml. Yet, the framework has some limitations, coming from both the ordered evaluation of guard predicates and the very restricted communication between those predicates. Here are two such limitations.

• A C/S policy does not depend on the symbolic state we are building, for example we cannot decide to concretize a term if all its leaves (variables) are already concretized.

• A C/S policy does not depend on the formula we are solving. For example, we cannot compute a path predicate, pass it to a solver (or to a simplifier) and then request concretization or symbolization depending on the solver's output.

Note, however, that the extended memory state Σ + does allow to overcome most of the above limitations, assuming one is willing to store (resp. to query) very complex information into (resp. from) Σ + . In our view, Σ + should be used with care, only as a last resort.

Implementation

The C/S policy mechanism presented so far has been integrated into Binsec/se [START_REF] David | BINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis[END_REF]. An overview of the modified architecture is shown in Figure 4.4. The C/S policy is specified in a textual format close to CSml. Subsequently, while the SE engine creates the path predicate, the C/S policy is queried for each encountered expression (Section 4.

Experiments

In this section three experiments are carried out with CSml and Binsec/se. The aim is to evaluate the performance and to compare the benefits brought by different policies. The three different evaluations are the following:

• First, we perform a large scale study on various benchmarks: some from samate [START_REF]SAMATE -Software Assurance Metrics And Tools Evaluation[END_REF], some malwares and all the coreutils. The objective was to study the impact of different policies targeting memory reads and writes. This evaluation aims at answering the following two research questions:

-RQ 1: Do C/S policies have a significant impact on SE in terms of the quality of results?

-RQ 2: Is there a best C/S policy for read/write operations -among standard policies?

• Second, we study the overhead of rule-based C/S specification in comparison to hardcoded ones. This benchmark the following two research questions:

-RQ 3 What is the extra-cost of rule-based C/S specification ?

-RQ 4 Is it affordable, i.e is the extra-cost low w.r.t solving time ?

• Last, we are interested in studying the impact of C/S policies in terms of path predicate solving time. The goal is to study the solving time evolution with regard to the path length and the solver used. The research question addressed is:

-RQ 5 Do all solvers handle all policies equally ?

Policies. For this three experiments we are considering 5 different C/S policies handling diffferently memory reads and writes. Policies are: CC, CP, PC, PP*, PP, where the first letter indicates whether read addresses are concretized (C) or propagated (P). The second letter indicates the same for write addresses in memory. PP* is an original policy where all read/write addresses are kept logic but the base and stack pointer are concretized (i.e on x86 registers esp and ebp are concretized). While CC and PP are standard policies the others are rather new. Reasoning logically about the memory is known to be difficult for DSE engines and SMT solvers. As a consequence these policies are chosen to assess and benchmark the policies on memory operations.

Quantitative Evaluation

This experiment is performed over 167 programs (x86 executable codes) -composed of programs from NIST/SAMATE [START_REF]SAMATE -Software Assurance Metrics And Tools Evaluation[END_REF] (a standard benchmark for program analysis), all Unix coreutils and several Windows malware from VXHeaven [START_REF] Vxheaven | [END_REF], for a total of 45,242 solver queries. Details can be found in Table 4.8. All instructions are traced, except calls to library functions which are stubbed by symbolic values (f resh logical variables). The solver is Z3, with a time-out of 30 seconds. We measure the influence of these policies in the following way: for each benchmark program, we consider an arbitrary (but reproducible) initial concrete execution and we ask the SE engine to iteratively invert every condition along the initial execution, leading to a set of new path predicate computations and solver queries. We record for each policy the number of queries which have been successfully solved (sat), proved infeasible (unsat) or which have triggered a time-out (TO). Note that only the first category leads to new test input and (hopefully) better code coverage. 4.10), the global number of successfully solved instances is quite similar for any policies but PP (Table 4.9). Actually, while a more symbolic policy leads in theory to more satisfiable queries, it may also come at the price of harder-to-solve formulas and time-outs. These results are a strong argument in favor of a generic C/S mechanism.

Results and conclusion

The major threats to validity are the representativeness of the experimental setting (policies, programs) and internal bugs in the SE tool. We mitigate these threats through using standard policies and variants of them as well as a large program set coming from three distinct well-known and publicly-available benchmarks. Moreover, we rely on publicly-available tools (SE, solver) and results have been crosschecked for internal validity.

Rule-Basd Language overhead

We evaluate the overhead of our parametric C/S policy mechanism. We want to answer the two following questions: RQ 3: What is the extra-cost of rule-based C/S specification, especially w.r.t. hard-coded policies (by mean of callback functions) and no C/S policy at all? RQ 4: Is it affordable, i.e. is the extra-cost low w.r.t. solving time?

Protocol We reuse the experimental setting of the previous evaluation. We consider two metrics: the cost of formula creation -which is directly affected by C/S policies, and the ratio between formula creation and formula solving. We record these metrics for the 5 previous policies, implemented either in CSml or through native callbacks, and we consider a baseline consisting of SE without any C/S policy. Ratio between the cost of path predicate computation (impacted by C/S) and the whole cost (i.e. formula creation + formula solving). Note that the time for formula solving does not depend on the way C/S is implemented (rules, hard-coded, no C/S).

Results and conclusion

Computation time benchmark

The first experiments have been carried out on a single program path which length is 377309 instructions long. On this path, we solved the path predicate for path length ranging from 1 to 377309 with the 5 different C/S policies. The goal was to evaluate the impact of the C/S policy on the solving time with regard to the path length. We expect to be able to classify which solver better handle each kind of C/S policies. Note that benchmarks were performed with the highest level of optimization (CRH) as described in Chapter 7.

By solver. The Figure 4.5, shows the results performed on the 5 policies and 5 different solvers using a 2 minutes timeout. As expected CC outperform the other policies as it constraints both read and write addresses in memory. Contrariwise PP barely overcome the 2550 path depth thanks to boolector. PP* provides a good alternative as it concretizes read/writes on the stack. The only solver to solve the whole path is Yices in CC followed by mathsat that succeed in solving a 81,960 instructions long path predicate.

By policies. The Figure 4.6, shows the results by policies and for each solver. As solvers deal differently with the different theories we wanted to check if some policies were better handled by a given solver. Results, speak by themselves while Yices surpass all other solvers for policies reduce memory (array) operation it performs very bad on PP policy. Contrarily, boolector is the worst for CC but outperform all the others solvers for CP,PC and PP. As an outcome, this experiment shows that the solver choice have a strong impact on the policy employed. These two experiments allowed to highlight the solving time disparity between policies, strenghtening the approach of modular policies. It also highlighted a great disparity between solvers which, as we can notice, deal very differently with concrete/symbolic memory accesses. Furthermore, this highlight which solvers best fits each policy and gives a good sampling (truth table) of what solving time is to except depending on the policy and the solver. Table 4.12 gives the overall overview of which solver best and worst handle each policies and gives the trace length expected to be solved with a 2 minutes timeout. Once again being able to adapt the policy appeared to be crucial depending on the solver at hand.

4.6

Toward extending CSml to syscall/libcalls and more

Definitions

As extension of the policy mechanism formalized and developped for expressions, we extended this mechnanism to library calls, syscalls and undecoded instructions. These are the three main vectors of non-determinism inputs in the DSE execution. Extending C/S for this, would allow to decide in a flexible way whether to concretize some parameters/return values whether to symbolize them. Using this method, irrelevant functions calls can simply be ignored or concretized while really interesting functions can be symbolized. Thus we proposed a stub mechanism integrating C/S actions. This mechanism is based on the C/S injection extension described earlier in the Chapter. Intuitively, a stub is defined as a sequence of assignments in which each lhs is assigned a value based on an action ρ * defined by ρ * {Sc, Se, S} selected from a policy. We denote Sc the unsound concretization where the lhs is replaced by an arbitrary constant value. We also denote Se the replacement of a lhs by a logical expression. Let us recall that a lhs is defined by lhs ::= v | v{i, j} | @[ e ]. Thus a stub is a sequence of re-assignement of variables (registers) or memory cells. In addition a stub should be shipped with a policy indicating what action to perform on each lhs and a possibly a function providing a specific propagation expression for that lhs in the case the associated action is Se. We propose a new evaluation operation stub_exec for stub Lhs:

stub_exec(Σ * , ϕ, lhs)      Σ * (lhs) ← f resh, ϕ ∧ lhs = f resh if ρ = S Σ * (lhs) ← ϕ e , ϕ ∧ φ ∧ lhs = ϕ e if ρ = Se, Σ * (lhs) ← ϕ e , e cs • ϕ e , φ Σ * (lhs) ← C, ϕ ∧ lhs = C if ρ = Sc, C eval Σ (lhs)      ρ C St (Σ, lhs) (4.1)
Finally, a stub can be defined as the execution of stub_exec on all the lhs of N St . We thus formalize the whole stub execution as defined below:

stub Σ * n , ϕ n stub_exec(Σ * , ϕ, N 0 ) • ... • stub_exec(Σ * n -1, ϕ n-1 , N n ) l, Σ * , ϕ, stub(N , C, P) l + 1, Σ * n , ϕ n , ∆(l + 1)
Stub kind While doing DSE we need to consider three major kind of stubs. First, external library stubs in the case we do not execute them symbolically, then syscall stubs (dependant of the system and kernel version) and finally not decoded instruction which, even though we can not give them a precise semantic we can approximate their side-effects with stubs. These three kinds of stubs implemented are encompassed by the formalization hereabove.

Library call stubs

Libcalls are any functions (most notably shared library functions) that are intentionally not symbolically executed to lighten the DSE computation. However handling side-effects of this functions is essential to preserve the execution soundness. Thus various stubs are implemented for multiples functions from the libc or from the Windows API.

Call convention Libcalls stubs have to deal with the call convention used by programs. The call convention defines the way parameters are sent to the callee and also defines how the stack should be cleaned-up. There are typically two modes, caller-based and calleebased where the responsability to restore the stack is given respectively to the caller or the callee. Secondarily it also defines parameter order on the stack, in other words either they are pushed left-to-right (LTR) or right-to-left (RTL). Known call conventions are:

• cdecl used in almost all Unix-based systems. All parameters are transmitted through the stack and the caller is responsible for stack restoration.

• stdcall used in Windows. All parameters are sent using the stack, but is calleebased so the function called restore the stack

• fastcall The first two parameters are put respectively in ecx and edx. All the others are pushed onto the stack. This convention is callee-based.

All this convention are RTL conventions. Table 4.13 summaries the properties of the different call conventions. All these considerations have an impact on the way stubs are handled. Formally, let's consider a call convention cvt {cdecl, stdcall, fastcall} and a function get_args(cvt, i th ) → Expr which for a given call convention and parameter number returns the corresponding expression. As a matter of exemple get_args(cdecl, 0) = @[esp -4] or get_args(fastcall, 1) = edx. Similarly, we define epilog functions performed after a stub to perform a gentle clean-up of the stack. For this, we consider a function card(St) → N the function which for a given stub returns its cardinal (i.e its number of parameters). Figures 4.7 gives the semantic of the epilog functions.

stdcall -epilog Σ * new Σ * [esp ← f resh] ϕ new ϕ ∧ f resh = (Σ * (esp) + (card(St) × (addr_size/8))) Σ * , ϕ, stub St Σ * new , ϕ new cdecl -epilog Σ * , ϕ, stub St Σ * , ϕ
N St {@[dst], @[src],
size, eax} with eax the returned value, which according to the specification is equal to dst at return. We want to propagate variables @[dst] and @[src], in addition we also want to concretize size which usually has an undetermined number of iterations. Thus, we have C St {(@[dst] → P), (@[src] → P), (size → C), (eax → P)}. Lastly, we define the propagation function P St given in figure 4.8.

System call stubs

Syscalls, are dependant on the OS Linux,Windows and dependent on the Application Binary Interface (ABI) on Linux. Syscalls are distinguished by the number given in eax. Handling syscall is highly kernel dependent, however, easier than libcalls as there is not calling convention neither the need of epilog. Yet, unless having a dynamic instrumenter working at kernel level, there is no other way than making stubs for syscalls.

P St (e)          dst if e = eax @[src] if e = @[dst] if e = @[src] if e = size

Instruction stubs

The symbolic aspect of DSE allows to emancipate from the strict IR decoding. Indeed, due to the variety of x86 instructions, it is difficult to model all of them precisely. That is why instruction stubs comes handy to give an approximated modeling of an instruction, either over-approximated by symbolizing either under-approximated by concretizing. The purpose is to keep the soundness of execution. Let us take the example of rdtsc.

RDTSC is an instruction returning in both edx and eax the numbers of tick since the last reset of the CPU read in the TSC register. Modeling precisely the content of the TSC content is not simple (and thus not decoded in DBA). Hence, we have N St {edx, eax}, and the propagation function can be modelled either by calling the real rdtsc and putting the result in the two registers or more lazily by symbolizing the content edx,eax. The second approach consists in choosing S and a relative fair approach to over-approximating the execution while keeping a satisfiable path predicate.

Implementation

The formalization hereabove, and the implementation made in Binsec/se only allows one stub per function or syscall. As a consequence, it forbids to select a different stub for the same function depending on the context.

Each new stub should be implemented at three levels:

• making the policy specification with parameters and returned values;

• implementing the data gathering in Pinsec (used by eval Σ (e));

• implementing in Binsec/se the propagation function P St modeling the behavior for each parameters or returned values.

Backward-Bounded DSE

This chapter presents a scalable and robust method for solving infeasibility queries, a standard problem encountered in reverse-engineering. bb-dse does not supersede existing DSE algorithm but rather complement them by addressing infeasibility queries in a precise manner.

Problem Dynamic methods only address reachability issues, namely feasibility questions, i.e. verifiying that certain events or setting can occur, e.g. that an instruction in the code is indeed reachable. Contrariwise, many questions encountered during reversing tasks are infeasibility questions, i.e. checking that certain events or settings cannot occur. It can be used either for detecting obfuscation schemes, e.g. detecting that a branch is dead (i.e. it cannot be taken) or to prove their absence, e.g. proving that a computed jump cannot lead to an improper address.

These infeasibility issues are currently a blind spot of both standard and advanced disassembly methods. Dynamic analysis and DSE do not answer the question because they only consider a finite number of paths while infeasibility is about considering all paths. Also, (standard) syntactic static analysis is too easily fooled by unknown patterns. Finally, while recent semantic static analysis approaches [BHV11; BR10; KV10; SMS11] can in principle address infeasibility questions, they are currently neither scalable nor robust enough.

At first sight infeasibility is a simple mirror of feasibility, however from an algorithmic point of view they are not the same problem. Indeed, since solving feasibility questions on general programs is undecidable, practical approaches have to be one-sided, favoring either feasibility (i.e. answering "feasible" or "I don't know") or infeasibility (i.e. answering "I don't know" or "infeasible"). While there currently exist robust methods for answering feasibility questions on heavily obfuscated codes, no such method exist for infeasibility questions.

Motivation Let us consider the obfuscated pseudo-code given in Figure 5.1. The function <main> contains an opaque predicate in 1 and a call stack tampering in 2 (cf. 8.1 and 8.2).

Getting the information related to the opaque predicate and the call stack tampering would allow to: • 2 to know that the ret of <fun1> is tampered and never return to the caller.

As a consequence a and c are dead instructions. Such trick would also allow to hide the real payload located at <X>.

Hence the main motivation is not to be fooled by such infeasibility-based tricks that slow-down the program reverse-engineering and its global understanding.

Goal and challenges

In this chapter, we are interested in solving automatically infeasibility questions occurring during the reversing of (heavily) obfuscated programs. The intended approach must be precise (low rates of false positives and false negatives) and able to scale on realistic codes both in terms of size (efficient) and protection -including self-modification (robustness), and generic enough for addressing a large panel of infeasibility issues. Achieving all these goals at the same time is particularly challenging.

Proposition We present Backward-Bounded Dynamic Symbolic Execution (bb-dse), the first precise, efficient, robust and generic method for solving infeasibility questions. To obtain such a result, we have combined in an original and fruitful way, several stateof-the-art key features of formal software verification methods, such as deductive verification [START_REF] Leino | Efficient Weakest Preconditions[END_REF], bounded model checking [START_REF] Biere | Symbolic Model Checking without BDDs[END_REF] or DSE. Especially, the technique is goal-oriented for precision, bounded for efficiency and combines dynamic information and formal reasoning for robustness.

Impact Backward-Bounded DSE does not supersede existing DSE approaches, it complements them by addressing infeasibility questions. Altogether, this work paves the way for robust, precise and efficient disassembly tools for obfuscated binaries, through the careful combination of static/dynamic and forward/backward approaches. ( †): follow only a few traces ( † †): very limited reasoning abilities ( ‡): can have false positive and false negative, yet very low in practice

Formalization

Preliminaries We consider a binary-level program P with a given initial code address a 0 . A state s (a, σ) of the program is defined by a code address a and a memory state σ, which is a mapping from registers and memory to actual values (bitvectors, typically of size 8, 32 or 64). By convention, s 0 represents an initial state, i.e. s 0 is of the form (a 0 , σ). The transition from one state to another is performed by the post function that executes the current instruction. An execution π is a sequence π (s 0 • s 1 • ... • s n ), where s j+1 is obtained by applying the post function to s j (s j+1 is the successor of s j ). Similarly, we call s j the predecessor of s j+1 if s j+1 is obtainted by application of the post function on s j .

Let us consider a predicate ϕ over memory states. We call reachability condition a pair c (a, ϕ), with a a code address. Such a condition c is feasible if there exists a state s (a, σ) and an execution π s (s 0 • s 1 • ... • s) such that σ satisfies ϕ, denoted σ |= ϕ. It is said infeasible otherwise. An feasibility (resp. infeasibility) question consists precisely in trying to solve the feasibility (resp. infeasibility) of such a reachability condition.

These definitions do not take self-modification into account. They can be extended to such a setting by considering code addresses plus waves or phases [START_REF] Bonfante | CoDisasm: Medium Scale Concatic Disassembly of Self-Modifying Binaries with Overlapping Instructions[END_REF].

Principles We build on and combine 3 key ingredients from popular software verification methods:

• backward reasoning from deductive verification, for precise goal-oriented reasoning;

• combination of dynamic analysis and formal methods (from DSE), for robustness;

• bounded reasoning from bounded model checking, for scalability and the ability to perform infeasibility proofs.

The initial idea of bb-dse is to perform a backward reasoning, similar to the one of DSE but going from successors to predecessors (instead of the other way). Formally, DSE is based on the post operation while bb-dse is based on its inverse pre. Perfect backward reasoning pre * (i.e. fixpoint iterations of relation pre, collecting all predecessors of a given state or predicate) can be used to check feasibility and infeasibility questions. But this relation is not computable.

Hence, we rely on computable bounded reasoning, namely pre k , i.e. collecting all the "predecessors in k steps" (k-predecessors) of a given state (or predicate). Now symmetry does not hold anymore: while pre k can answer positively to infeasibility queries (if a predicate has no k-predecessor, it has no k -predecessor for any k > k and cannot be reached), but cannot falsify them (because it could happen that a predicate is infeasible, for a reason beyond the bound k). Moreover, it is efficient as the computation does not depend on the program size or trace length, but on the user-chosen bound k.

In practice, checking whether pre k = ∅ can be done in a symbolic way, like it is done in DSE: the set pre k is computed implicitly as a logical formula (typically, a quantifier-free first-order formula over bitvectors and arrays), which is unsatisfiable iff the set if empty. This formula is then passed to an automatic solver, typically a SMT solver [12] such as Z3.

Yet, backward reasoning is still very fragile at binary-level, since computing pre in a perfect way may be highly complex because of dynamic jumps or self-modification. The last trick is to combine this pre k reasoning with dynamic traces, so that the whole approach benefits from the robustness of dynamic analysis. Actually, the pre k is now computed w.r.t. the control-flow graph induced by a given trace π -in a dynamic disassembly manner. We denote this sliced pre k by pre k π . Hence we get robustness, yet since some real parts of pre k may be missing from pre k π , we now lose correctness: we may have false positive FP (because pre k π will be incomplete w.r.t pre k ), additionally to the false negative FN due to "boundedness" (because of too small k). A picture of the approach is given in Figure 5.2.

Algorithm Considering a reachability condition (a, ϕ), bb-dse starts with a dynamic execution π and iterates it in order to solve ϕ at the given location. The algorithm is given in 2.

As a summary, this algorithm enjoys the following good properties: it is efficient (depends on k, not on the trace or program length) and as robust as dynamic analysis. On the other hand, the technique may report both false negative (bound k too short) and false positive (dynamic CFG recovery not complete enough). Yet, in practice, our experiments demonstrate that the approach performs very well, with very low rates of FP and FN. Experiments are presented in Sections 8.1.4, 8.2.4, 10.1 and 10.2.

By convenience, we will not distinguish anymore between the predicate ϕ and the reachability condition (a, ϕ) if a is clear from context.

Solving Infeasibility Questions with bb-dse

We show in this section how several natural problems encountered during deobfuscation and disassembly can be thought of as infeasibility questions, and solved with bb-dse.

Opaque predicates (OP) is a predicate always evaluating to the same value. Intuitively, to detect an opaque predicate the idea is to backtrack all its data dependencies and gather enough constraints to conclude to the infeasibility of the predicate. Considering p = (a, ϕ) the pair address-predicate for which we want to check for opacity and π the execution trace under attention we have:

• if p is dynamically covered by π, then returns FEASIBLE;

• otherwise, returns bb-dse (p), where INFEASIBLE is interpreted as "opaque". This obfuscation is addressed in detail in Chapter 8.

Call stack tampering

Call stack tampering consists in altering the standard compilation scheme switching from function to function by associating a call and a ret and making the ret to return to the call next instruction. The ret is tampered (a.k.a violated) if it does not return to the expected return site pushed on the stack at the call. This infeasibility problem can be addressed with the predicate @[esp {call} ] = @[esp {ret} ]. It compare the content of the value pushed at call @[esp {call} ] with the one used to return @[esp {ret} ]. If it evaluates to UNSAT, a violation necessarily occurs. A complete taxonomy and detection algorithm is discussed in Chapter 8.

Opaque constant Similar to opaque predicates, opaque constants are expressions always evaluating to a single value. Let us consider the expression e and a value v observed at runtime for e. Then, the opaqueness of e reduces to the infeasibility of e = v. Dynamic jump closure When dealing with dynamic jumps, switch, etc., we might be interested in knowing if all the targets have been found. Let us consider a dynamic jump jump eax for which 3 values v 1 , v 2 , v 3 have been observed so far. Checking the jump closure can be done through checking the infeasibility of eax

= v 1 ∧ eax = v 2 ∧ eax = v 3 .

Virtual Machine & CFG flattening

Both VM obfuscation and CFG flattening usually use a custom instruction pointer aiming at preserving the flow of the program after obfuscation. In the case of CFG flattening, after execution of a basic block the virtual instruction pointer will be updated so that the dispatcher will know where to jump next. As such, we can check that all observed values for the virtual instruction pointer have been found for each flattened basic block. Thus, if for each basic block we know the possible value for the virtual instruction pointer and have proved it cannot take other values, we can ultimately get rid of the dispatcher.

A glimpse of conditional self-modification Self-modification is a killer technique for blurring static analysis, since the real code is only revealed at execution time. The method is commonly found in malware and packers, either in simple forms (unpack the whole payload at once) or more advanced ones (unpack on-demand, shifting-decode schemes [START_REF] Ugarte-Pedrero | SoK: Deep Packer Inspection: A Longitudinal Study of the Complexity of Run-Time Packers[END_REF]).

The example in Figure 8.1 (page 106) taken from ASPack combines an opaque predicate together with a self-modification trick turning the predicate to true in order to fool the reverser. Other examples from existing malwares have been detailed in previous studies (NetSky.aa [START_REF] Yadegari | Symbolic Execution of Obfuscated Code[END_REF]).

Dynamic analysis allows to overcome the self-modification as the new modified code will be executed as such. Yet, bb-dse can be used as well, to prove interesting facts about self-modification schemes. For example, given an instruction known to perform a self-modification, we can take advantage of bb-dse to know whether another kind of modification by the same instruction is possible or not (conditional self-modification). Let us consider an instruction mov [addr], eax identified by dynamic analysis to generate some new code with value eax = v. Checking whether the self modification is conditional reduces to the infeasibility of predicate eax = v.

Benchmark against forward DSE

We compare bb-dse with standard forward DSE, as well as with (unbounded) backward DSE. We are interested in comparing their efficiencies and their adequacy to infeasibility questions -through the distribution of their results, between SAT, UNSAT and timeout. The experiment is performed on a trace of 115000 instructions and we check at each conditional jump if the branch not taken is infeasible (UNSAT) or not (SAT), which is equal to checking if the branch is dead. For bb-dse, we take the algorithm for opaque predicate detection described in Section 5.2, with bound values k = 100 and k = 20. We argue in latter experiments (Section 8.1) that k = 20 is a reasonable bound. We use the forward DSE of Binsec/se, and backward DSE is obtained from bb-dse with a bound set to ∞.

Results are presented in Table 5.2. While forward and backward DSE provide similar results, bb-dse clearly surpasses them in terms of efficiency, spending less than a second for every predicate without any timeout (≥ 2000 with DSE). From a result point of view, bb-dse with k=16 returns very few UNSAT answers compared to the other methods (54 vs ≥ 7000). Actually, this was expected since DSE takes the whole path into account, and while dead branches are rare in normal code, dead paths are very common.

Conclusion

This preliminary experiment gives a clear demonstration on the advantages of bb-dse over DSE on infeasibility questions. Indeed, besides the dramatic gap in efficiency (which was of course expected since DSE depends on the whole size trace), DSE reports far more infeasible branches -which would lead in practice to too many false positives. These results were expected, as they are direct consequences of the design choices behind DSE and bb-dse. On the opposite, bb-dse is not suitable for feasibility questions. As such, we provide throughout benchmarks of bb-dse in Chapter 8 and real world application in Chapter 10. The DSE is usually performed by three components described in Figure 6.2. First, the Dynamic Binary Instrumentation (DBI) generates an execution trace transmitted to the symbolic execution engine which computes the path predicate and generates a formula sent to an automatic solver. As a response, the solver returns a status and a model which can optionally be used to generate new inputs. These inputs can subsequently be sent back to the DBI to generate a new trace.

Part III Implementation & Optimizations

Dynamic Instrumentation

Introduction

Several different instrumentation systems are being used for DSE. Probably the most famous is Pin [START_REF] Luk | Pin: Building Customized Program Analysis Tools with Dynamic Instrumentation[END_REF] developped by Intel. It allows to instrument x86 programs both 32 and 64 bits by embedding at runtime a shared library that will hijack the normal control flow of the program to instrument it. No debug feature is used by Pin which helps bypassing basic anti-debugging tricks. In the same vein, DynamoRIO provides similar functionalities [START_REF] Bruening | Transparent Dynamic Instrumentation[END_REF]. A possible alternative is the use of the virtualization engine Qemu [START_REF] Bellard | Open Source Processor Emulator[END_REF] (developped by the awesome Fabrice Bellard). Last, the promising Panda engine [START_REF] Dolan-Gavitt | Repeatable Reverse Engineering with PANDA[END_REF] based on TCG, LLVM and Qemu which unlike other DBI allows repeatable instrumentation and backward execution.

Pinsec

Pinsec is the instrumenter developped for this thesis. Based on Pin, and developped in C++ it accounts for approximately 2000 loc and is able to instrument both Linux and Windows binaries. Execution traces are generated in protobuf3 to be parsable and used in any language. Among advanced functionalities, it allows to gather function parameters for some libc, and Windows API functions; it also allows to retrieve arbitrary values in memory and registers. It eventually provides a mechanism for on-the-fly value patching (mostly used to force a given path). Finally, via a messaging API, it allows some remote

Dynamic Instrumentation

control actions for dynamic interaction with the symbolic execution engine (see Section 6.6).

Configuration. Basic parameters given to the pintool are, -start-entrypoint to start at the entry point of the program or more generically -start to begin at a specific address. That is especially useful if we want to skip all the initializations performed at the begining of the program. As a remplacement -function allows to provides a function name to instrument which requires symbols to be present. The -out option is used to specify the output trace file. To limitate the trace length or the instrumentation time -maxlength or -timeout are available. Lastly, it is possible to activate the tracing of self-modification layers with -trace-waves that will tag all addresses written in memory. If at some point of the execution the program jumps on a tagged address a new wave information is recorded in the trace.

In addition to parameters given via the command line, an instrumentation can be configured via a JSON file, providing more advanced features (-config command line argument). The configuration permits to define in a granular manner which function to trace and which function to "skip". It also allows to define the policy to adopt for all library calls or syscalls, namely either to trace it or not, or to retrieve theirs values etc.

Input injection

A key feature, for path selection and iterating paths is the ability to inject inputs, or values during the execution, forcing the value of a certain register or memory cell at some point of the execution. We define T {R, M, I} the kind of inputs with R a register, M a memory address, I an indirect pointer. The idea is to alterate the dynamic execution of the program to patch values or to gather some value for later usage (concretization etc). Indeed, these values can be later used for C/S injection in the dynamic symbolic engine. We define A {S, C, (Pt × Bv)} the set of possible actions to perform for that input with S the pintool ignores it, C the value is retrieved and Pt the value is patched with the given value. An input is as a rule of the form guard ⇒ A of which guard defines the predicate where to apply the input action. This predicate is defined by an adress, an occurence and W {Be, Af} defining respectively before and after the given address. An input rule is defined by: type :: address :: when :: iter ⇒ action T ::

Bv :: W :: N ⇒ A ⇔
As a matter of example eax :: 0x801040 :: Be :: 0 ⇒ (Pt, 0x0) indicates to patch eax with value 0x0 at the first occurence of location 0x801040 before the instruction is being executed.

Performances. This pintool was not especially design to run fast and not especially designed to be compact (because of protobuf). For instance, at load-time all instructions are cached for a quick posterior access. Yet, performing this task slow-down the effective starting of the program. Additionally, we need to instrument the program at the instruction level while Pin also allows to instrument at the basic-block or function level which is far more efficient. As a matter of appreciation the table 6.1 shows empirical statistics about instrumentation performances. The table shows the trace length, native execution time compared to instrumentation time and the average execution time per instruction. The benchmark was performed on a Windows virtual machine so all the results are relative to the performances of the VM. The initialization phase is quite slow, as consequence longer trace have a better ratio of instruction/sec. The benchmark is composed of 6 packers later used for large scale benchmarks. It should be taken into account that a pintool by design usually induces a slow-down from 7.8x to 20x [START_REF] Luk | Pin: Building Customized Program Analysis Tools with Dynamic Instrumentation[END_REF] compared to native execution when instrumenting at basic-block level. Thus, a significant time is spent in the DBI itself independently from the pintool implemented. In addition, we perform analysis at the instruction level which is very costly in terms of time. All the packers executions take less than 3 minutes which is efficient-enough for automated analysis of large binaries data-set.

Symbolic Execution Engine

Introduction

As mentioned earlier, the symbolic execution engine is supposed to perform both the path selection (Sel) and path predicate computation (C). Among existing DSE working at binary level, we can notice Mayhem [START_REF] Cha | Unleashing Mayhem on Binary Code[END_REF], Fuzzball [START_REF] Caselden | HI-CFG: Construction by Binary Analysis and Application to Attack Polymorphism[END_REF], S2E [START_REF] Chipounov | The S2E Platform: Design, Implementation, and Applications[END_REF], Angr [START_REF] Shoshitaishvili | SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis[END_REF] and the promising recent Triton [START_REF] Saudel | Triton: A Dynamic Symbolic Execution Framework[END_REF]. What differentiates them, is mostly architectures supported, theories used for formulas, solvers supported, path covering strategies and additional analyses like abstract interpretation, tainting or data dependencies.

Binsec/SE

Binsec/se is the symbolic engine developped in the Binsec platform. As the DBI engine it is parameterized with JSON configuration files. At the time of writing it represents more than 10K OCaml lines of code. Like most engines an analysis can be implemented using a callback mechanism (see Figure 6.3). It supports Z3, boolector, CVC4 and Yices.

Nonetheless, what differentiates it from the existing DSE engines are the modular path predicate computation (i.e concretization/symbolization), all the optimizations implemented at the formula level and the different stub mechanisms for library and system calls. All these differences are elaborated in Part II and Chapter 7.

Path predicate computation

Path predicate computation is the cornerstone of computation. It is in charge to evaluate the semantic of each instruction and update the path predicate accordingly. The computation in Binsec/se also integrates the C/S policy mechanism. The path predicate computation time is generally negligible compared to solving time [START_REF] David | Specification of Concretization and Symbolization Policies in Symbolic Execution[END_REF]. Meanwhile for the sake of evaluation we measured the path predicate computation time for different C/S policies (cf. 4). The benchmark given in table 6.2 aims at evaluating the impact of C/S policies on the path predicate computation. We compute both the execution time and the number of instructions processed per seconds. The idea is to have a rough apreciation of the throughput. For that, we selected few random binaries and performed the computation on them. This includes the parsing of instructions in the protobuf trace, which represents a significant amount of time. PP correspond roughly to the case where no C/S policies is applied as everything is propagated like in standard DSE. The difference with CC is only 4044 instructions per seconds which represent a gain of 19%. Considering CC to be an heavy policy we can conclude that the C/S policies computation takes at most 20% of the path predicate computation (still negligible compared to solving time).

Path selection

Beside a fine-grained control of a single execution trace, automatic multiple paths exploration is also a desired feature of a DSE tool. Ideally, the path exploration engine should allow either to fulfill some standard coverage requirements, or to focus on specific parts of the code through dedicated (user-defined) search heuristics. It relies on a simple API allowing to easily implement various exploration strategies. In particular, this API offers a function select(S) returning the "best" trace from a set of traces S, w.r.t. a user-defined score function. Scores are built from several (predefined or dynamically computed) traces characteristics, such as length, last instruction call-depth, distance to a given target, etc. This approach allows to precisely define a wide-range of exploration strategies. Several strategies are already implemented such as DFS, BFS, random path, MinCall-DFS and MinCall-BFS [START_REF] Bardin | Binary-Level Testing of Embedded Programs[END_REF]. The Depth-First-Search (DFS) strategy might get stuck in narrow parts of the code and Breath-First-Search might get stuck in loops. Thus, it is worth considering alternate strategies. For instance MinCall-DFS selects the longest path having the lowest call depth. This strategy ensure to hit all the functions while keeping the longest path possible to have a maximum coverage. MinCall-BFS works similarly but consider the shortest path and the lowest call depth.

Analysis development

Internally, an analysis is represented as an OCaml class, which each analysis should inherit from. This class provides appropriate callbacks and data structures for implementing any DSE-based analysis. Main callbacks are:

• pre_execution, post_execution triggered respectively once at the begining and once at the end of the analysis;

• visit_instr_before, visit_instr_after triggered before (resp. after) every assembly instruction of the trace;

• visit_dbainstr_before, visit_dbainstr_after triggered before (resp. after) every DBA instructions of an x86 instruction; Figure 6.3: BINSEC/SE analysis callbacks A summary of all callback location calls is given in Figure 6.3. These callbacks allow to apply specific actions at a specific step and/or location along the execution in a highly configurable manner. They help developing new analyses without a deep understanding of the whole inner-working of the DSE.

Memory Management & Initial State

In standard DSE we usually assume argv and the environment variable env to be inputs in the program memory. Later in the execution, allocated memory can also become inputs. In practice, all the other memory addresses in memory are either not mapped, or not accessible for writing due to theirs belonging to the kernel. This differs from the closed quantifier-free array theory over the bitvectors used QF_ABV. Indeed, by default an array is totally unconstrainted and the bounds are limited to the size of bitvector indexes. Then, the solver is free to give a valuation for any unconstrainted memory cells which can lead to meaningless results. To address this issue the main solutions remaining to be implemented are:

• constraining the load operations by enforcing possible addresses,

• dumping the initial state,

• potentially using, taint analysis to force load operation to be performed at tainted addresses (also called "controlable").

Automatic Solving

Introduction

There are two kinds of automatic solvers used. First constraint-programming based solvers like or-tools [START_REF]Google Optimization Tools[END_REF] from Google or also Colibri [START_REF] Chebaro | Behind the Scenes in SANTE: A Combination of Static and Dynamic Analyses[END_REF]. Second, Satisfiability Modulo Theories(SMT) solvers based on DPLL. Binary-level DSE requires bitvectors theory and, in most cases, the array theory. Known solvers supporting these two theories are Z3 [MB08], CVC4 [START_REF] Deters | A Tour of CVC4: How It Works, and How to Use It[END_REF], boolector [START_REF] Niemetz | Boolector 2.0 System Description[END_REF] and Yices [START_REF] Dutertre | Yices 2.2[END_REF].

Nevertheless, their difference tends to be very negligible as most of them now handle the smtlib2 format [START_REF] Barrett | The Satisfiability Modulo Theories Library (SMT-LIB)[END_REF]. What differenciate solvers are the theories supported and the usability features included like interactive or incremental modes.

Solving in Binsec/se

Binsec/se embeds an internal representation of formulas, subset of the SMTLIB2 acting only on bitvectors and arrays. This representation can be exported to SMTLIB2 as a common format with external solvers. Binsec/se does not provide direct binding with solvers. The two ways to solve formulas are:

• files in SMTLIB2 format,

• interactive mode, for solvers supporting this functionality. This allows to use the two commands push and pop to remove a posteriori, some terms of the formula.

Although we use a common format, some solvers may require specific processing. For instance, some of them do not support timeout as command line argument or generated models are not necessarily in the same format. Main differences lay in the support of arrays as function parameters. Indeed, Binsec/se uses two functions as syntactic sugar for reading, or writing 32 bits values in an array. One of them is the load32_at function given in listing 6.1. It is invoked the same way as select but returns a 32bits value. This greatly improves the formula readability. Unfortunately, boolector does not support arrays as function parameters, as a consequence it should be inlined. Listing 6.1: load32_at SMT function

IDASec: DSE analysis vizualisation

As fullfilment of one of the contributions aiming at lifting analysis results to make them usable for the reverse-engineer. I developed an IDA plugin called Idasec facilitating the triggering of an analysis and the exploitation of results. This plugin represents more than Python 7000 lines of code. Basic features allow to request the DBA semantic for an instruction in order to understand its side-effect, as shown in Figure 6.4a. But the main purpose of Idasec is to manipulate dynamic traces. Apart from being able to load a trace and vizualize it (as shown in Figure 6.4b) it allows to highlight instructions executed, creates heatmap of instructions and some dynamic disassembly features. In the later case, the idea is to follow the trace and disassemble instruction that would have been missed or wrongly disassembled by IDA.

Components Interaction

Thank's to an internal DBA representation and a tiny SMTLIB2 representation it can perform some computation on data and values in order to generate reports or charts. From an analysis perspective, some obfuscation specific features are implemented to highlight dead code, annotate code or compute various statistics. Global aim is to integrate DSE analysis in the main tool which is used in reverse-engineering so as to facilitate data exploitation in an user-friendly manner.

Components Interaction

The communication between the three entities is being made using a message queueing protocol base on ZeroMQ4 . This framework has been chosen as it provides great bindings in the three languages involved C++, Python and OCaml. In this context, Binsec/se works as a server handling analysis requests over the network. A request is formed by a configuration file serialized in protobuf, followed by the execution trace splitted in chunks. A chunk is a buffer of instructions, transmitted when filled. The size of a chunk can be parametrized with the argument -chunk-size in Pinsec. This changes from the classical workflow where arguments are sent on the command line and the trace read from a file. When running as a server Binsec runs multiple worker to receives different requests simultaneously. The architecture is modular, thus various configurations are possible:

• Pinsec ↔ Binsec for direct streaming, of the execution trace to Binsec (see Section 6.7 for a concrete application),

• Idasec ↔ Binsec for static symbolic execution. Paths can easily be created using IDA. (see Section 10.2 for an application),

• Pinsec ↔ Idasec ↔ Binsec for a complete interaction between the three entities. This configuration allows a dynamic and simultaneous interaction with the program instrumented and the lifting of resulting informations in IDA, all in the same time.

All messages transmitted over the three entities are of the form COMMAND, DATA where COMMAND indicates the DATA kind or a control message. From the Binsec/se side, at the time of writing three commands are supported:

1. DECODE_INSTR: to decode the semantic of an instruction into DBA, 2. REQUEST_INFOS: to have analysis available, solver available etc, 3. START_ANALYSIS: that takes a configuration as DATA and triggers the appropriate analysis accordingly.

Pinsec, support few commands to interact with the instrumentation 5 . Supported commands are:

• RESUME resuming the instrumentation after a breakpoint hit. When a breakpoint is triggered Pinsec send a BP_REACHED to the symbolic executor,

• PATCH_ZF allowing to patch ZF forcing a specific value. This is being used to force a program to take certain branches.

API.

Within an analysis in Binsec/se two additional callbacks are available to interact with the different entities:

• send_message sending a command, to any of the other components. Note, that by default when running a remote symbolic execution, all log messages are sent to the remote entity,

• input_message_received triggered when a message is received from an external component

In practice: A crackme example

A crackme is a challenge simulating a real world situation where binary programs are designed to make the analysis difficult. The goal is usually to find a string key (the flag) allowing to validate the challenge.

Flare-On is a reverse engineering challenge organized since 2014 by the FLARE team of FireEye Security6 . This section analyses the first challenge of 2015 since it is straightforward enough to be discussed in detail and will put in action all features described hereabove. This crackme is a 32 bits Windows program which asks for a password and prints "You are success" or "You are failure" depending on the keyboard input. Each byte of the input (input_buffer) is xored with 0x7d, the result is then checked against a key stored in the data section (data_str), cf. Figure 6.5.

Solving the crackme by symbolic execution aims at checking that the predicate ZF=1 is true at location 0x40105b; and this, for every character of the key. If the generated formula is satisfiable, then the right character can simply be retrieved in the formula solution at input_buffer[ecx]. One last remaining problem is the initial state. If none is specified, the solver is allowed to give any valuation to the content of data_str, while it is read-only data. Hence, an initial state constraining the value of the data_str bytes is required in order to get meaningful results for input_buffer (cf. Section 6.3.3). Finally, iterating over input_buffer can be done in two ways: a manual offline way, and a fully automated way (more complex).

The simple (painful) way From a trace taking the fail branch, we should solve ZF=1 at 0x40105b to get the right char and inject it back as input via the configuration file (cf: 6.2.2) for generating a new trace that will go for a second loop iteration, repeating until the whole key is found. The automated way Configures a breakpoint at 0x40105b (the address of jnz), compute the right character value, send a command to patch the ZF flag when the command BP_REACHED is received and resumes instrumentation to force the tracer to take the right branch and to loop again. This fully automatic method makes usage of both the remote control features and the incremental solving (cf. Section 6.4.2). This method allows to solve all the character values in O(n) w.r.t trace length. Finally, we obtain the right key solving the challenge, bunny_sl0pe@flare-on.com7 .

Chapter 7

Path predicate optimizations

Optimizing the path predicate at the formula level is a crucial task as solving it is the most costly part of DSE. Furthermore, prior knowledge of the analysis and program allows to perform some relevant context-sensitive pre-processing optimizations. As an example, some optimizations will greatly take advantage of the way memory accesses are performed. First, pre-processing optimizations implemented are aiming at reducing the complexity in space/time, but also provide normalized representation of formulas. This normalized representation is used for optimizations to benefit from one another. Second we propose array optimizations aiming at reducing constraints on the array representing the memory. Benchmarks preformed shows in best cases, a tremedous speed-up in solving time.

Pre-processing optimisations

This section describes four different pre-processing optimizations: (1) backward pruning aiming at removing all unused terms in the formula, (2) constant propagation which performs several syntactic simplification, (3) rebase, an original optimization normalizing some expression and (4) high-level predicate aiming at lifting low-level x86 comparison operations into natural conditions. Table 7.1 summarizes the optimizations and which solver benefits from each of them.

Backward-pruning

The main pre-processing operation performed by most DSE engines is the backwardpruning phase. The objective is to remove all unused or irrelevant terms in the formula by doing a backward pass starting from the assert property to check. All variable terms used in any assert of the formula are then kept. The listing 7.1 gives an example where the value of esp3 is checked. Recursively, eax, esp1 and esp0 are then used. Experiments Regarding benefits measurement, we compare the number of terms in formulas with and without pruning. Table 7.2 provides the formulas statistics with and without the pruning phase. This benchmark has been performed on a 377300 instructions path predicate. The gain in space is significant, it varies from a 129Mo formula file with more than 1M terms to a 22Mo formula file with 239916 terms. The gain in solving time is mitigated. For example, as shown in Figure 7.1 mathsat can solve a 72k not-pruned trace, it can solve a 82k pruned trace with a 2min timeout. Solving times, appeared not to be significantly better if not worse for some solvers (Z3, CVC4). Thus this optimisation is more valuable for formula compactness and readability rather than any solving time improvements. As of now, unless explicitely mentioned all the other optimizations and benchmarks use this generic post-processing pass on the formula.

Constant propagation & Local Rewriting

Constant propagation is also a common optimization in DSE engine solvers or compilers. While it is usually performed by the solver, it is interesting to make it during the path predicate computation as it simplifies data structures hold internally and also unleash the power of others optimizations that require a canonical representation of terms. Figure 7.2 shows a trivial example of constant folding on the expression esp2. Propagation is being performed by classic rewriting rules which the more important are given in Figure 7.3. We define by ⇓ the concrete evaluation operator, that simulate an expression according to its semantic or fail otherwise. Thus, this operator works only on constant variables.

Rebase

The rebase optimization is a new auxiliary optimization aiming at reducing the number of variable definitions in the path predicate so as to improve the efficiency of both the backward-pruning pass, and the read-over-write optimization described in Section 7.2 by providing a common basis of logical comparison. This optimization works by replacing a new variable definition with an older definition by commiting all the arithmetic changes performed on it. It works for basic arithmetic operators {+, -}. Example in figure 7. 4 shows the two advantages of applying such transformation combined with the backward-pruning pass. In the example esp3 can be rebased on esp1 which makes the esp2 definition useless. Then the backward-pruning pass remove the term from the formula. Impact In addition to reducing the number of terms in the formula, this optimization also lays some basis for making logical comparisons more easier. For instance, in the example it is clear that esp2 and esp3 are not aliased (strictly disjoint) because they are both based on esp1 but with different offsets. This property will be of a great help for the next section.

High level predicate encoding

The semantic of assembly instructions tends to be modeled with low level operations using for instance bit-masks, xor or extract. This is especially the case for conditions. At the source level the condition if (x = 0), while certainly be assembled with both a cmp and a jz instruction that will communicate with flags update. Table 7.3 shows an example of binary semantic for the simple ecx < 24 predicate.

OF := (ecx {31} = 24 {31} )&&(ecx {31} = res32 {31} ) SF := res32 < s 0 [...] jl 0xffffffec if (SF = OF ) goto 0xffffffec else [...] ((ecx -24) < s 0) = (ecx {31} = 24 {31} )&&(ecx {31} = res32 {31} )
Based on some recent researches [START_REF] Djoudi | Recovering High-Level Conditions from Binary Programs[END_REF], the idea is to lift low-level operators to higherlevel operators that once symbolically executed will be hopefully simpler to solve. Indeed, it depends on the inner working of the solver, some might be more efficient on low-level encoding while some others might be better on higher-level operators. Based on Table 7.4 we perform a syntactic processing on instructions to transform low-level predicates to their natural condition equivalent. Then the symbolic execution is performed as usual. This optimization is highly pervasive as it will modify all the path constraints in the formula. The transformation is sound as it only replaces a cmp, sub, test immediatly followed by conditional instruction based on pattern matching rules. Doing a generic transformation would require more in-depth and expensive formal analysis [START_REF] Djoudi | Recovering High-Level Conditions from Binary Programs[END_REF]. Also, this optimizations is pattern-matching based so it works solely on x86 and would require different rules to be adapted to other architecures.

Experiments Using the same execution trace (377000 instrs), the benchmark highlight the computation time with and without the high-level predicate optimization. Experiments carried put in evidence a small gain for certain solvers. Figure 7.6 shows the results for Yices. While it fluctuates the high-level predicate encoding is on average more efficient than without optimization (58% of the time). As a conclusion, the gain is rather small but such pre-processing worth being activated if the solver used takes advantage of higher-level predicates encoding.

Array optimizations (load/store)

The theory of arrays is used in DSE to represent the memory. Therefore, it is important to handle it carefuly and to optimize operations performed on it, they are used to be highly constrainted. We consider three types: arrays A, index I and elements E in any theory (in our case bitvectors). As a recall, the array theory [START_REF] Mccarthy | Towards a Mathematical Science of Computation[END_REF] T A provides two • read :

A × I → E • store : A × I × E → A
So, while read(A, x) returns the logical value at index x in the array A, write(A, x, v) returns a new array updated with the value v stored at x. The first property of array is the functionality (cf. FC) which states that given an array a, if two indexes i, j are equals the read operation on whichever index are equals. Given the signature of the store, a memory is either an empty memory or the outcome of a sequence of store. The read-over-write (RoW) is instinctively knowing whether a read index has previously been written or not. For a given memory, this can be done by iterating all its store operations. The Read-over-Write axiom consider two cases:

FC : if i = j, read(a, i) = read(a, j) (7.1) RW1 : if i = j, read(write(a, i, v), j) = v (7.2) RW2 : if i = j, read(write(a, i, v), j) = read(a, j) (7.3)
Intuitively, the two cases can be described as:

• RW1 we can replace a read operation by the value written on the previous write if it is performed on the same logical indexes,

• RW2 if both indexes are different, we can replace the read in the result of the store by a read in a (directly).

Backwarding simplification These two properties can be applied in order to perform simplification on arrays. The idea is to perform such simplification on every load of the execution to either substitute it by the written value (Figure 7.7) or to "rebase" it to an older memory (Figure 7.8). The later case works similarly to the rebase optimization. For a given load the simplification algorithm needs to work recursively as long as it can compare the load and store indices.

Before Read-over-Write →

After Read-over-Write memory1 := write(memory0, 0xffc351fc, 0x04) memory1 := write(memory0, 0xffc351fcn 0x04) eax := read(memory1, 0xffc351fc) eax := 0x04 Before Read-over-Write

→

After Read-over-Write memory1 := write(memory0, 0xffc351fc, 0x04) memory1 := write(memory0, 0xffc351fc, 0x04) memory2 := write(memory1, 0x80105200, 0xfc) memory2 := write(memory1, 0x80105200, 0xfc) eax := read(memory2, 0x7f000080) eax := read(memory0, 0x7f000080)

Standard Read-over-Write pre-processing

To simplify a load operation a backtracking step on the whole store chain must be performed. The "standard" Read-over-Write is a linear approach where the RoW complexity for a single load is linear O(n) with n the number of store operations in the path predicate. Depending on the number of load the worst case complexity of the whole simplification process is roughly quadratic. Hence the backtracking phase along the storechain is usually bounded by a constant k to ensure only a linear overhead.

     true if comparable(x, y) ∧ x = y f alse if comparable(x, y) ∧ x = y ? if ¬comparable(x, y)
Implementation 3-cmp comparable returns true only if both expression use the same logic variables (in this case the bitvector theory T Bv ). As an example 3 -cmp(esp 1 -4, esp 1 -4) = true, 3 -cmp(esp 1 -4, esp 1 -8) = f alse and 3 -cmp(esp 1 , eax 0 ) =? as esp 1 and eax 0 cannot be syntactically compared. We consider by convenience that memories (aka array) are named strictely incrementally, thus M x+1 is the memory created after a store in M x .

Backtracking algorithm

We can now formalize the RoW backtracking algorithm as a recursive function iterating the store-chain bounded by k. We denote by STC-RoW the unbounded algorithm and kSTC-RoW the algorithm bounded by k. The overall kSTC-RoW complexity is O(#load × k) thus bounded by O(n 2 ) and the algorithm is defined by: kSTC-RoW(load(M n , e ld ), k)

     v if C = true ∧ k = 0 kSTC-RoW(load(M n-1 , e ld ), k -1) if C = f alse ∧ k = 0 load(M n , e ld ) if C =? ∨ k = 0 with: M n-1 , e st , v

Read-over-Write "Concrete map"

In the case of constant indexes (eg. policy CC) we can in principle remove all load. Yet, kSTC-RoW cannot achieve it. A common solution is using a map of all indices written, then we can perform in O(ln(n)) the backtracking step of RoW. This provides the best complexity possible for the RoW simplification. We denote CM-RoW this algorithm. Under these settings, all load can either be replaced by the value previously written either being rebased on the initial memory. As a consequence, the chain of stores is not used and can be pruned. Unfortunately, having constant values for indices is a really specific situation and in DSE, indices are more often arbitrary logical expression on bitevctors.

Read-over-Write "Store-Map Chain"

The main issues of the previous approaches are:

• STC-RoW does not scale on huge path length we have to deal with,

• kSTC-RoW is not optimal,

• CM-RoW only applies under very specific settings.

We propose a more scalable and optimal algorithm which complexity is oscillating between O(ln(n)) and O(n 2 ) depending on the settings and environment. We can use a different internal data-structure to improve the complexity of the RoW. The idea behind this encoding is that multiple stores having the same base will update the same map thus reducing the cost of lookup when performing the RoW on a load. If a new store is performed but with a different base, a new map (with its base) is appended to the chain. Figure 7.10 shows the same store chain as the standard approach (see Fig. 7.9) but using our data-structure. For one load, the STC-RoW complexity is O(n) while it is y × log(x) for the STMC-RoW where y is the number of store-groups and x the size of the maps. In the worst case scenario we have y = n and thus x = 1 bringing us back to the same complexity as STC-RoW. Such a construction enhances significantly the complexity of the RoW algorithm. Table 7.5 summarizes the complexity gain between the different alternatives. The best construct is to keep a concrete mapping from constant addresses to theirs value but it only works if all read/write are performed to constant addresses. So, while with constant indices STMC-RoW have the best complexity (the same as a direct mapping CM), it also gain on more symbolic modes knowing that in the worst case it provides the same complexity as kSTC-RoW. As a consequence this algorithm adapts and scales to depending on the sort of loads and store performed and provides the optimal complexity in all cases. We denote respectively perfect techniques that perform the optimal substitution and we denote them partial instead.

M₀

update -store(M n+1 , e st , v) map n [off st ] := v if ¬(3-cmp(b n , b st ) ?) Sts :: (M n+1 , b st , (off st → v)) if 3-cmp(b n , b st ) ?
This algorithm works especially well on C/S policies that keep concrete memory addresses (cf. Table 7.5) in that it will always be possible to backtrack to the first memory thus opening the way to syntactical optimizations as the memory flattening presented hereafter.

Write-over-Write

The WoW is the property indicating that two consecutive store, at the same logical index are equivalent to the second store in the array of the first. Formally:

store(store(A n , i, v 1 ), j, v 2 ) ∧ i = j =⇒ store(A n , j, v 2 )
Performing a WoW simplification implies to backtrack on every store in memory which is very costly. Moreover, such simplifications should also handle potential load operation performed on the memory of a store before simplifying it. As such, STMC-RoW with its map-based chain provides the Write-over-Write (WoW) for free. Indeed, two store using the same base, and writing at the same address will update the same value in the map (overwriting the previous one).

Benchmarks

The following two benchmarks emphasize the difference and the effect of the kSTC-RoW and STMC-RoW techniques on a generated formula w.r.t compactness and efficiency of the optimization. For that a 370000 instructions long trace was used. For the kSTC a bound of k = 150 was arbitrarily used. The first benchmarks shows formula simplification statistics by in applying kSTC-RoW or STMC-RoW. The second benchmark, provides some insight on the internal statistics of optimizations themselves like the chain lengths, map sizes etc.

Benchmark #1 This benchmark provides formula statistics namely number of inputs, variables, load and store in memory and the number of constraints. These attributes are compared without RoW and with kSTC-RoW or STMC-RoW under different levels of concretization on the memory. The idea is to assess the potency of optimizations on formulas addressing the memory accesses differently. For that, we re-use policies throughoutly discussed in Chapter 4, namely CC, PC, PP* and PP. For clarity in the results the policy CP is not shown as results are very close from PP* and PP. Results are given in Table 7.6. Results for CC are outstanding. While kSTC-RoW removes half of loads, STMC-RoW substitute all of them. The 3381 remaining are loads on the initial memory and thus allow to prune the whole store chain. This shows that kSTC-RoW is not optimal and could have replaced 48972 more loads. On more symbolic modes and especially SS kSTC-RoW managed to replace 2632 loads by their value while STMC-RoW managed to replace 6618 of them, thus more than twice more. It worths noting that these statistics does shows load which where rebased to preceding memories. These data are shown in the next benchmark. Timing benchmarks are given in Table 7.8 and also validates the gain of STMC over the STC approach.

Benchmark #2

The goal of this benchmark is to highlight the inner efficiency of kSTC and STMC optimizations. It shows the number of load fully replaced (ROW 1), the number of load rebased (ROW 2) on a prior memory and the number of load where nothing could have been performed (∅). It also shows for kSTC the min, max, moy of the backtracking k (so bounded by 150). For STMC-RoW it takes another meaning, it represents min, max, mean the size of the different maps in the store chain. Finally it also shows for STMC-RoW the y value representing the size of the custom store chain. The benchmark re-use the same settings as the first benchmark and results are given in Table 7.7. Results are insightful to understand the potency of algorithms. In STMC-RoW in CC load but two are replaced by theirs value. The two remaining have been rebase on the initial memory while the others were already load on initial memory. On average kSTC backtrack on five store to perform the replacement which means many of RoW are rather local. As expected in CC the store-chain length is 1 so all the RoW simplification where performed in ln(x). For more symbolic modes, optimizations are still working despite the reasoning difficulty. For instance, in PP, STMC manages to replace 8959 load and to rebase 1105 of them but more surprinsingly the maximum size of the map is 264 with an average of 12. This results shows that storing multiple store with the same base is working and efficient in practice even one more symbolic modes. This benchmark highlight another takeway on PP. In STMC, the store-chain is reduced to 24770 while the whole store chain is still 58005 and kSTC have to backtrack on such size.

Conclusion

Results are clear, while kSTC slightly reduce the number of load and the number of variables compared to no optimization, STMC significantly peforms better and especially on CC (as expected). Indeed, for STMC in CC the store chain is only one map containing all the element. Notably, PC is particulary weak as only 28 load were replaced. This indicates that keeping either load or store symbolic tends to weaken the optimization. Further, solving time benchmarks are performed in the next section. As a conclusion, STMC performance in CC are optimal as expected. Yet, in more symbolic modes the STMC-RoW is still potent as it managed to replace 8959 load and to rebase 1105 of them which is twice better than a standard RoW. It is worth noting that in this mode the average map was 12 with a maximum value of 264. These results validates the potency of the optimization at any level of "symbolicness".

Memory flattening

This syntactical optimization is complementary with the RoW and aims at removing the memory array when all the load and store are performed at concrete indexes. This is made possible by the RoW that will either replace a load by its value either rebase it in the initial memory denoted M 0 . Then, all load replaced by a f resh bitvector representing the memory cell. Removing all the load operations turn a Qantifier-Free Array and Bitvectors (QF_ABV) formula into Qantifier-Free Bitvectors (QF_BV). In this way, the formula can be solved by solvers not supporting the array theory T A . Jointly, it helps solvers like Z3 which are more efficient on bitvector-only formulas. For this optimization, we consider M 0 the initial memory, and map ∈ (Bv → ϕ) the map from constant addresses to theirs symbolic value. The optimization algorithm is formalized as:

mem_flat(map, M i , e)      map, map(e) if e ∈ dom(map) ∧ M i = M 0 ∧ e ∈ Bv map[e ← f resh], f resh if e / ∈ dom(map) ∧ M i = M 0 ∧ e ∈ Bv map, load(M i , e) otherwise
The first output is the map (update or not), that will be held during the whole symbolic execution. The second output is the expression simplified (or not). Let us detail the three cases: (1) the index is already in the map so we substitute the expression by the content of the map, (2) the index is not in the map so return a fresh symbol and update accordingly and (3) the memory where the load is performed is not the initial memory so nothing is performed.

Experiments To evaluate the gain we solve the previously used path predicate of 377300 instructions containing 3381 read in memory. We performed the experiments in CC-CRH so that the optimization will remove all the memory array. Figure 7.11 shows the solving time results for Z3 that really benefits from the flattening. While the solving time did not appeared to change significantly on other solvers, it was never worse. Thus, it is worth activating this optimization that will opportunistically remove the array theory on concrete modes like CC-CRH.

Experiments: Optimization combination

All experiments are complementary one another. This section evaluates the gain of the different RoW modes on the criteria of formula size and solving time. All that is made in different environment of execution namely different concretization and symbolization settings. Benchmarks are performed on a 377300 instructions long trace. Three benchmarks will be performed. Bck#1 evaluates the computation time impact of the optimisations on the path predicate. Bck#2 evaluates the impact of optimizations w.r.t C/S policies and the impact on the path predicate. Bck#3 evaluates the different solvers w.r.t optimizations given a fixed C/S policy).We notate "C" the constant propagation, "R" the rebase, "W" the kSTC-RoW and "H" the STMC-RoW. Thus, the code CRH, indicates the combination of constant propagation, rebase and STMC performed in this order. As expected, basic pre-processing depends on the efficiency of the solver, while array optimizations demonstrate a huge speed-up for all solvers.

Benchmark #1: Impact on path predicate computation

Table 7.8 shows the benchmark results for five different C/S policies (see. Chapter 4) and five different levels of optimizations. Results show that not performing optimization increases the instruction throughput which tends to discourage using these optimizations. However, they drastically decreases the solving time as shown in Bck#3. As a conclusion, we might be interested in finding the right balance in selecting the optimizations although it will everytime be in favor of using all optimizations.

Benchmark #2: Optimizations

This benchmark assesses the potency of optimizations on different C/S policies in terms of formula size and statistics. Table 7.9 shows the statistics for each level of optimizations.

Unsurprisingly, the CRH optim in CC manages to remove all the store operations and drastically reduce the load operations to the ones reading in the initial memory. The gain for loads is x31. The STMC is by design less potent on more symbolic policies. However optimisations provide good constraints reduction, for instance in PP* constraints are reduced from 150928 to 108126 between no optimisations and CRH, thus providing a gain of 28%. As conclusion, from the statistical point of view, the combination CC-CRH removes all stores, and almost all load but more symbolic modes also provides significant improvments on the solving time as shown in Bck#3.

Benchmark #3: Solving time

With a fixed, policy CC this benchmark evaluates the solving time of a path predicate under different level of optimisations. As performed in previous Chapter 4 we evaluate the solving time of different path predicate lengths. We evaluate 5 solvers under these settings with a 2 minutes timeout (TO=120s). Figure 7.12 shows the solving time results obtained and the gain provided in terms of performences. Results shows, that without optimisations none of the solvers succeed in solving the whole execution trace. In CRH Yices manages to solve the whole predicate. The difference between no optimisation, just constant propagation and rebase is rather low as they are more pre-processing tasks aiming at improving the RoW. Results put in evidence the gap between CRW and CRH. CVC4, mathsat and Yices are the best examples.

While the performances of solvers are very disparate, optimizations provide better results than no optimizations and most notably with the CRH. Results show that CRW misses lots of cases and is as consequence not optimal.

Part IV Experimental Validation

Chapter 8

Deobfuscation

This chapter presents two case-study obfuscations that were used as applications of our algorithms in order to detect and thwart them. We considered opaque predicates and call/stack tampering that can be encoded as infeasibility queries. Moreover, these two obfuscations are rather resilient to static approaches which justifies focusing on them as they are commonly encountered. Other obfuscations, like self-modification, are indirectly handled by the dynamic aspect of our DSE approach. On opaque predicates, experiments will be performed on the whole coreutils obfuscated using O-LLVM. For call/stack tampering, experiments are performed on samples programs obfuscated with Tigress along with some packers. This Chapter lays the basic taxonomy and detection methodology used in Chapter 10 for real-world case-studies.

Opaque predicates detection

Definitions

An opaque predicate is a predicate always evaluating to true (resp. false) for which this property is ideally difficult to deduce. The infeasible branch will typically lead the reverser (or disassembler) to large and complex portions of useless junk code. The next section shows various concrete examples of such predicates. The first definition was given by Collberg[CTL98]: Definition 2. A variable V is opaque at point p in a program, if V has a property q at p which is known at obfuscation time written V q p . A predicate P is opaque at p if its outcome is known at obfuscation time. We write P F p /P T p if P always evaluates to False respectively True at p, and P ? p if P may sometimes evaluate to True and sometimes to False.

Taxonomy & Example

From now we denotes opaque predicates by Opaque Predicates (OP) for concision. Collberg first proposed a taxonomy and classification of opaque predicates [CTL97] using either arithmetic or data structure invariant properties to build opaque predicates. The different kinds of opaque predicates:

Arithmetic invariant aims at encoding invariants into arithmetic properties on numbers. An efficient method is to use modulo arithmetic. Further distinction between arithmetic opaque predicates is given below. As an example Figure 8.1 shows the x86 encoding of the 7y 2 -1 = x 2 predicate (as generated by O-LLVM [START_REF] Junod | Obfuscator-LLVM: Software Protection for the Masses[END_REF]). This condition is always false for any values of ds:x, ds:y, so the conditional jump jz <addr_trap> is never going to be taken. Data-structure invariant such category aims at hiding invariant into data-structure, crafted on purpose which have specific opaque properties. Collberg proposed the example of an array given in listing 8.2 which hold the following properties: (1) all cells at indexes modulo 3 starting from 0 are 1 mod 5, (2) from index 1 all cells at indexes modulo 3 are 2 mod 7, (2) cells at indexes 2,5,8,11 are respectively 1,5, 2 and 7. Then g[3] % g [5] == g [2] is always true because g [3] holds the property 1 mod 5 and g [5],g [2] are statically 5 and 1.

∀x, y ∈ I 7y 2 -1 = x 2 ∀x ∈ I 2|(x + x 2 ) ∀x ∈ I 2|x(x + 1) ∀x ∈ I 3|(x 3 -x) ∀x ∈ I x 2 ≥ 0 ∀n ∈ I + , x, y ∈ I (x -y)|(x n -y n ) ∀n ∈ I + , x, y ∈ I 2|n ∨ (x + y)|(x n + y n ) ∀n ∈ I + , x, y ∈ I 2 |n ∨ (x + y)|(x n -y n ) ∀x ∈ I + 9|(10 x + 3 • 4 x+2 + 5) ∀x ∈ I 3|(7x -5) ⇒ 9|(28x 2 -13x -5) ∀x ∈ I 5|(2x -1) ⇒ 25|(14x 2 -19x -19) ∀x, y, z ∈ I (2 |x ∧ 2 |y) ⇒ x 2 + y 2 = z 2 ∀x ∈ I + 14|(3 • 7 4x+2 + 5 • 4 2x-1 -5) ∀x ∈ I 2|x ∨ 8|(x 2 -1) ∀x ∈ I + 64|(7 2x + 16x -1) ∀x ∈ I + 24|(2 • 7 x + 3 • 4 x -5) ∀x ∈ I 2x+1 i=1,2| i i = x 2 ∀x ∈ I + 8|(7 2x+1 + 17 x ) ∀x ∈ I + 2| x 2 2 ∀x ∈ I + 3|x(x + 1)(x + 2) ∀x ∈ I + 7 |x 2 + 1 ∀x ∈ I + 81 |x 2 + x + 7 ∀x ∈ I + 19 |4x 2 + 4 ∀x ∈ I + 4|x 2 (x + 1)(x + 1)
the example given in listing 8.3, create_circular_list creates a list of a random size and returns a pointer to it. Then move shifts the current pointer of a given number of items and insert add a new item in the list and returns a pointer to it. As a consequence g cannot alias with h. By moving both pointers in the data structure with the same value we ensure they cannot alias. This property si then used to create opaque predicates. This is an example but any other data-structure embedding such invariant are good candidates to create such predicates.

void main () { item * g = c re a te _c i rc ul a r_ li s t ( rand () ) ; g = move (g , rand () ) ; item * h = insert ( g ) ; int x = rand () ; g = move (g , x ) ; h = move (h , x ) ;

if ( h == g ) { // never taken } } Listing 8.3: Pointer aliasing invariant data-structure

Concurrence based invariant

The idea is to encode invariant in race condition properties. Both static and dynamic analyses are known to be difficult and unreliable for proving properties on such concurrent codes. Thus, using such kind of OP is particularly efficient although difficult to craft reliably. Collberg proposed an example where two threads update global variables intentionally delayed the threads to encore opaque predicates. Listing 8.4 shows in example where two threads computes the variables x and y of an opaque predicates. The trick is that x is either R*R if threadS come seconds, either R*R * R*R threadT come second. In both cases the OP invariant will hold.

Detecting opaque predicates

Intuitively, to detect an opaque predicate, the idea is to get back on all its data dependencies. If the predicate is local, the distance from the predicate and its inputs instanciation will be short and the predicate will be relatively easy to break. Otherwise the distance is at most linear with the trace length which hardly scales in forward DSE. Interestingly, for invariant opaque predicates, it is not required to get back on all its input definition to break it, constraints on them might be enough. Consequently, a bb-dse with a pre ≤k approach might be very handy.

Furthermore, it allows to bypass some dynamic tricks that would mislead a reverser into flagging a predicate as opaque. A good example is a predicate found in the packer ASPack. The predicate seemingly opaque, is not to be opaque due to self-modifications (Figure . 8.1). Statically, the predicate is opaque since bl is necessarily 0 but it turns out that the second bytes of the instruction mov bl, 0x0 is being patched to 1 during the execution in order to take the other branch when looping back later on. The key element of the approach is the aggregation of paths for a given bound k and a given predicate ϕ p at the specified location l p . Hence, the pre ≤k is computed for every new k-path to that predicate found in the trace. If all of the formulas generated evaluate to unsat the predicate is flagged opaque, unknown otherwise. If both branches of a predicate are covered by the trace the predicate is flagged not opaque. Table 8.2 summarizes the different possible status for a predicate.

Evaluation

Goal We are interested in the following two questions: Q1: what is the detection capacity of our approach, and are the ratio of false positive, false negative acceptable? The second question is Q2: is our approach efficient and scalable?

Benchmark and protocol In benchmarks, we have chosen the O-LLVM [START_REF] Junod | Obfuscator-LLVM: Software Protection for the Masses[END_REF] in which we implemented various opaque predicates (cf. Table 8.3). O-LLVM has been selected because its core engine is open-source and it already implemented a mechanism for opaque predicates. Other obfuscation engines were not open-source [START_REF] Collberg | Distributed Application Tamper Detection via Continuous Software Updates[END_REF] or outdated.

In order to evaluate the bb-dse, two sets of benchmarks were selected:

• 5 simple programs taken from the State-of-the-Art in DSE for obfuscation [START_REF] Yadegari | Symbolic Execution of Obfuscated Code[END_REF]. Each of the sample was obfuscated 20 times (to obtain the same number of samples than coreutils). Programs are: simple-if, bin-search, bubble-sort, huffman and matrix-multiply.

• all 100 coreutils as a genuine dataset reference

Table 8.3: OP implemented in O-LLVM Formulas Comment ∀x, y ∈ Z y < 10||2|(x × (x -1)) (provided with O-LLVM) ∀x, y ∈ Z 7y 2 -1 = x 2 ∀x ∈ Z 2|(x + x 2 ) ∀x ∈ Z 2| x 2 2
(2 nd bit of square always 0)

∀x ∈ Z 4|(x 2 + (x + 1) 2 ) ∀x ∈ Z 2|(x × (x + 1))
In total 200 binary programs were used. For each of them a dynamic execution trace was generated with a maximum length of 20.000 instructions. By tracking where opaque predicates were added in the obfuscated files we are able a priori to know if a given predicate is opaque or not giving in consequence a set of ground truth values. Note that all predicates in coreutils are considered to be genuine (and then false positive if flagged as opaque). This large but controlled experiment allowed to test the accuracy of results. The 200 samples sums up a total of 1,091,986 instructions trace length and 11,725 conditionnal jumps with 6,170 genuine predicates and 5,556 opaques among them. Experiments were carried using different values for the bound k in order to find which one fits best at finding all opaque predicates without yielding too much false positives. As a matter of estimation a predicate marked opaque with k = 2 is more likely to be opaque than a predicate marked opaque with k = 30 since the path constraint might make the predicate unsatisfiable. Benchmarks were carried with a 5 second timeout per queries (k-path + predicate).

Results Table 8.4 and Figure 8.2 show respectively the graph and the table of the relations between the number of opaque (OP), genuine (OK), false positive (FP)/negative (FN) depending of the bound value k. The two last columns show the percentage of false positive among the number of all predicates and the number of false postives opaque predicates. These results represent predicates that only had one branch covered. Among the 11,725 predicates, 987 were fully covered by the trace and were excluded from these results, keeping 10,739 predicates (and 5,183 genuine predicates). The experiment shows a tremendous peak of opaque detection with an approximate k = 10. Alongside, the number steadily decreases as the number of false positive grows. All opaque predicates are rightly flagged opaque for k = 16 and luckily no predicate raised any TIMEOUT. The number of false positive 293 represent 6.28% of all predicates marked opaque and only 3.17% of all predicates for approximately 1.46 false positive per sample on average.

Note, that the path aggregation discussed in Section 8.1.3 provides a substantial gain since it reduces of 4.62% the number of false positive for k 16 (see Table 8.5).

Resolution time

We have performed another experiment about computation time of predicates solving to check if it scales on a large number of predicate (here more than 10000) with a 2.7GHz Core i7 and 16Go of RAM. Each predicate formula was solved using Z3 with a 5 second timeout. Table 8.6 gives for each k-bound value the total time taken for solving and the average per query. For k 16 the average time per query is 0.018s which tends to prove that this technique scales. Previous work aiming at solving invariant opaque predicates [START_REF] Ming | LOOP: Logic-Oriented Opaque Predicate Detection in Obfuscated Binary Code[END_REF] obtained on average, 0.49s per queries (min:0.09, max:0.79). For this kind of opaque predicates this approach delivers a tremedous speed up (more than x27). These results validates the bb-dse advantages compared to strictly forward DSE. The analysis is also efficient and scales thanks to its independence from the trace length which address Q2. As shown by Table 8.6 for k=16 the average time solving per query is 0.014s which is acceptable even with a large number of predicates to check.

Call/Stack tampering 8.2.1 Definition

A call stack tampering is the mean to alter the classical compilation scheme switching from a function to another using the call and ret instruction, where ret jumps on the address pushed on the stack by the call. The ret is tampered (a.k.a violated) if it does not return to the expected returnsite pushed on the stack by the call. This thesis proposes a more precise characterization and taxonomy of a call stack tampering.

A trivial example is given in Figure 8.3. From an attacker perspectives benefits are twofold:

• the reverser might be lured into exploring useless code starting from the returnsite,

• the real target of the ret instruction is hidden from the static analysis stand point. In this later case the call has been compiled so that the function _mbrtwoc will perform the ret of sub_8053AB0. This can happen to be an issue in DSE if the function tail called (here _mbrtwoc) is not symbolically executed because its ret will not be visible.

Taxonomy & Examples

From a semantic point of view, a ret is just an indirect jump to the first value on the stack which can lead to various different scenarios of violation:

• ret performed with a dynamic jump • no call but a ret (orphan ret)

• call, tampering of the return value and then ret

In this work we strengthen the violation definition to better characterize it. For reverse-engineering purposes it is important to distinguish if a ret does not return well, if the value has been overwritten or if the stack pointer (esp) has been tampered. This approach identifies the following ret properties:

Tampering detection

This study uses the bb-dse algorithm to detect the tampering. Of the author's knowledge DSE have never been used to detect such obfuscation. The purpose is to check the infeasibility of the tampering by checking the validity of some predicates. As a recall, a predicate φ is VALID iff: unsat(¬φ). To characterize the violation, the following queries are performed: Table 8.7 summarizes all the possible states and attached tags. This stack tampering analysis uses the same bb-dse as opaque predicates but with slightly differents settings. In this case, the k value will be different for every call, ret pair. The trace is analysed in a forward manner each call encountered is pushed to a call stack. Upon ret encounter, the first call on the stack is poped and a pre ≤k is performed where k is the distance between the call and the ret. The different queries are then solved on this bounded path slice. Two problems might corrupt the call stack breaking the synchronicity of call,ret pairs:

• integrity: @[esp {call} ] = @[
• Tail call [START_REF] Meng | Binary Code Is Not Easy[END_REF] to non-traced function: As shown above tail calls are the mean of calling functions using a jump instruction instead of call to avoid stack tear-down.

Similarly to the previous case, a tail call in a non-traced instruction will hide the ret instruction, so the current call stack head should be poped to keep synchronicity.

• ret performed with dynamic jumps. As our analysis is ret centric any obfuscation replacing all rets by dynamic jumps would make the analysis inefficient

Evaluation

Two benchmarks are performed to assess the analysis effectiveness. First, a controlled benchmark is performed on samples, obfuscated on purpose. Second, a benchmark of various packers is performed to ensure the scalability on real-world obfuscated programs. The first benchmark is on the same 5 samples as opaque predicates, but obfuscated with the source-to-source obfuscator Tigress [START_REF] Collberg | Distributed Application Tamper Detection via Continuous Software Updates[END_REF]. Files have been obfuscated with the AntiBranchAnalysis transformation that replace all conditionnal branches with calls and rets. The two schemes used here are:

• push; call; ret; ret (the second ret will jump on pushed value)

• push; ret (similar to previous)

The second experiment is a free wheel experiment on few packers to find if violations were employed. Packed binaries are chosen as they are more likely to contain such protections. Indeed, they are usually the first line of protection to be broken in order to reach a malware payload. In this experiment, the payload was a legitimate program (hostname on Windows).

Analysis combination

This chapter present three different kind of analyses combinations based on the algorithms and methods described previously in this thesis. The first combination is a disassembly algorithm taking advantage off both dynamic and symbolic approaches limitating the weaknesses of the purely static approaches. The second combination is a static and symbolic combination based on abstract interpretation and DSE geared for vulnerability discovery. The last combination is a forward and backward static analysis combination aiming at detecting infeasible test requirements for software testing. Based on abstract interpretation and weakest-precondition calculus, it differs from the other combination by working at the source level.

Combination principles

In general, combining different approaches is a strength from the program analysis perspective, especially when dealing with obfuscation as one might target a specific kind of analysis. As an example, Marion et al proposed a mixed static and dynamic approach for disassembly purposes [START_REF] Bonfante | CoDisasm: Medium Scale Concatic Disassembly of Self-Modifying Binaries with Overlapping Instructions[END_REF] called concatic disassembly. The idea is to enrich static disassembly with dynamic analysis allowing to handle both self-modification and codeoverlapping, which techniques are hindering static analysis. The disassembly obtained is more precise and efficient than a pure static disassembly. The key point of this approach is to obtain a proper segmentation of the different self-modification layers.

Forward/Backward combination Let's take the formal approach; some properties are to be checked on a given program. Various semantic analyses techniques like abstract interpretation, weakest-precondition calculus or symbolic execution exist to address this problem but each of them have theirs particularities. The two main characteristics are whether the analysis works forward or backward and whether the analysis is under or over-approximated. Table 9.1 shows the characteristics of different analyses and their abilities to detect some properties. For instance abstract interpretation computes an over-approximated invariant of the whole program, while symbolic execution computes under-approximated but more precise values for a given path. Similarly, forward DSE is able to generate new inputs to cover a given path, while backward-DSE cannot. But it • Dynamic disassembly retrieves only instructions and branches observed at runtime on one or several executions. That technique is safe, but possibly very incomplete. Yet, it recovers instructions masked by self-modification, code overlapping, which are out of reach for static disassembler.

For example, objdump is based on linear sweep, while IDA performs a combination of linear sweep and recursive disassembly (enhanced with severals heuristics).

Static/Dynamic combination

As mentioned in previous Section (9.1), various approaches mix both static and dynamic analyses. Doing so helps to bypass the dynamic jumps, self-modification and code-overlapping issues. Nonetheless, it cannot address dead code and opaque predicates which will still be disassembled. Similarly, dead returnsite (never executed) due to call/stack tampering will still be disassembled. While such combination is better than static or dynamic alone, it can still be improved to circumvent aforementioned obfuscations.

Principles

As already explained above, standard disassembly approaches are not satisfactory. Hence, we propose a sparse disasembly, an algorithm based on dynamic disasssembly reinforced with a static disassembly guided with complementary information about obfuscation (computed by backward-bounded DSE). The goal is to provide a more accurate and sound disassembly. The approach takes advantage of the two analyses presented in Sections 8.1 and 8.2 in the following way:

• use dynamic values found in the trace to keep disassembling after indirect jumps instructions and disassemble the "self-modified" code;

• use a static recusive disassembly algorithm to enlarge the dynamic disassembly but the disassembly is guided by the symbolic execution. Thus it takes into account the following properties:

use opaque predicates found by bb-dse to avoid disassembling dead branches (thus limiting the number of recovered non legit instructions);

use call/stack tampering information found by bb-DSE to disassemble ret targets in case of violation, as well as not to disassemble the returnsite of the call in this case.

Implementation This algorithm has been integrated in the existing recursive traversal disassembly algorithm implemented in Binsec. The bb-dse procedure sends OP and ret information to the modified disassembler which takes them into account when recursively disassembling the program.

Evaluation

Opaque predicates The first benchmark aims at testing the disassembly of O-LLVM obfuscated samples using the sparse disasembly approach. In this benchmark, IDA and Objdump perform well thanks to their linear-sweep. Binsec in recursive traversal performs badly with rets and some jump eax added by the obfuscator. Nevertheless, the sparse disassembly performs very well with an instruction differential ranging from 12 to 63. A manual verification showed that this difference was an over-disassembly of returnsite that is never executed due to the stack tampering. Once again, the sparse disasembly provided a better and sound disassembly of the program.

Coreutils

The last benchmark aims at proof-testing the sparse disasembly on larger obfuscated binary samples to test its efficiency. Thus, we have obfuscated the coreutils using O-LLVM in order to insert opaque predicates into them. Unfortunately, it was not possible to mix it with Tigress that uses some inline assembly constructs not supported by Clang (and required by O-LLVM). Table 9.4 shows the results on 5 coreutils selected randomly. While the samples are significantly bigger, the ratio between Objdump/IDA and Binsec rec/sparse remains roughly similar. Obviously, the coverage of both Objdump and IDA is larger since it takes advantage of the linear sweep not to miss any function. Yet, they also disassemble lots of junk code.

These experiments have demonstrated that sparse disasembly is an effective way to enlarge a dynamic disassembly, in a both significant and safe manner. Indeed, sparse disassembly recovers between 6x and 16x more instructions than dynamic disassembly, yet it still recovers slightly less instructions than recursive disassembly (including less junk), and much less than linear sweep -partly due to the focused approach of dynamic disassembly. Hence, sparse disassembly stays close to the original trace.

Conclusion

The carried experiments brought very good and accurate results about controlled samples, achieving perfect disassembly. From this stand-point, sparse disasembly performs better than the combination of both recursive and linear like in IDA, including up to 30% less recovered instructions than IDA. The coreutils experiments showed that sparse disassembly is also an effective way to enlarge a dynamic disassembly in a both significant and safe manner. Yet, our sparse disasembly algorithm is currently limited by the inherent weaknesses of recursive disassembly for example the handling of all the computed jumps targets would require advanced pattern techniques.

Thus, sparse disasembly performs better on obfuscated samples than recursive disassembly alone and limitate the over-disassembly shortcoming of linear-sweep based approaches.

Use-After-Free detection: Use-case binary exploitation 9.3.1 Introduction

This works has been performed in collaboration with Verimag Grenoble and especially Josselin Feist to detect and exploit Use-After-Free (UaF) vulnerabilities. The technique is based on static analysis and Dynamic Symbolic Execution(DSE) and led to the discovery of various vulnerabilities and most notably CVE-2015-5221 [START_REF] Mitre | [END_REF]. An UaF appears when a heap pointer is used after having been freed. Such memory corruptions can in some cases be leveraged by an attacker to execute arbitrary code and consequently to craft an exploit. Finding an UaF is particularly difficult as it is only triggerable after the sequence of events malloc, free and use for a given resource. While these three events can be located at distant area of the code. Finding such sequences requires some path coverage algorithm, which are non-linear in the general case. Moreover, it requires, at some extend, alias analysis to compare pointers on the heap. It also requires alias analysis which is known to be hard for static analyzer.

Combination

The combination first performs a static analysis of the code and extract a weighted slice containing relevant events (malloc,free,use). This is later used by a guided dynamic symbolic execution to trigger the bug and to generate appropriate inputs. Static analysis phase aims at reducing the coverage surface for the DSE in order to improve its efficiency. The DSE algorithm is also empowered with specific heuristics guiding the path selection and enumeration so as to maximize the chance to find a solution quickly.

• Static Analysis is performed by a tool GUEB [START_REF] Feist | GUEB Static Analyzer for Detecting Use-After-Free on Binary[END_REF] which performs a value analysis based on abstract interpretation keeping as abstract states the set of allocated and freed memory chunks. Within the same chunk, if the sequence malloc, free, use is found, a slice containing all paths to the three events is extracted from the CFG. This slice is then transmitted to the DSE for UaF vulnerability discovery.

• Guided DSE performs a path exploration of each slice provided by the static analysis, to validate or invalidate each candidates. For a given slice, the DSE explores all the possible paths until finding one satisfying the conditions to trigger the UaF.

Enumerating paths can lead to the so called path explosion problem. Even though the analysis is performed on a slice it also uses its guidance heuristics to return the best candidate (path) based on a score. The score is based on the distance between the three points of interest (malloc, free, use).

Evaluation

Experiments are peformed on several versions of the DSE namely with and without guiding heuristics. Results are compared against the standard fuzzers AFL [lca16] and radamsa [START_REF] Archer | Radamsa[END_REF]. The experimentation is performed on JasPer8 , an image conversion library. The analysis has found an UaF in the mif_process_cmpt function which subsequently led to the CVE-2015-5221 identifier [START_REF] Mitre | [END_REF]. From the performance perspectives, without the guiding heuristics Binsec/se is unable to generate a PoC to trigger the vulnerability while with the heuristics a PoC is generated in 20 minutes.

Conclusion

This combination approach designed for UaF detection relies on the use of a weighted slice computed by abstract interpretation and path coverage with symbolic execution. It proved to be efficient on real-world applications. In addition, guiding heuristics proved to be useful and further work are ongoing to make them more generic. Indeed, they are for now driven by examples encountered.

[Bonus] Infeasible tests requirements: Use-case source-level

This section shows a use-case where the forward/backward combination approach has successfully been applied to a slightly different domain, namely software testing at source level. As the language and tools change, the approach remains similar. It emphasizes the portability of such approach accross languages and an example of the variety of domain where it can be applied. This work has been published in [START_REF] Bardin | Sound and Quasi-Complete Detection of Infeasible Test Requirements[END_REF].

Software Testing: Introduction

In software testing, a coverage criteria specify the requirements to be covered by a test case. These coverage criteria are normative test requirements that the tester must satisfy before delivering the software under test. Among existing coverage we have: decision coverage (DC), condition coverage (CC), multiple condition coverage (MCC), function coverage or weak mutations (WM). Figure 9.1 illustrates possible encodings for selected critera. ] as a convenient formalism to specify and to encode several structural testing criterias into a unified solution making use of existing verification tools. Given a program P , a label l is a pair loc, ϕ where loc is a location in P and ϕ is a predicate over the internal state at loc. We say that a test datum t covers a label l = loc, ϕ if there is a state s such that t reaches loc, s and s satisfies ϕ. An annotated program is a pair P, L where P is a program and L is a set of labels in P . The main benefit of labels is to unify the treatment of test requirements belonging to different classes of coverage criteria. While Bardin et al explored the question of automatic test generation with labels [START_REF] Bardin | Efficient Leveraging of Symbolic Execution to Advanced Coverage Criteria[END_REF], we focus in this section on the problem of infeasibility test requirement detection.

Problematic

In practice, such test criterias are limited by the infeasibility problem [Wey93; WHH80; YM89], where a requirement cannot be covered by any test case due to inherent program structure. In addition to yield a worse code coverage, automated testing tools might waste time trying to cover the criteria. Identifying them is an undecidable problem [START_REF] Goldberg | Applications of Feasible Path Analysis to Program Testing[END_REF], so it affects the decision to stop testing as it requires the knowledge of what remains to be covered. As consequence, it is difficult to accurately measure the coverage of the test suite which is usually used to stop the testing process (usually 80% to 100%).

Combination

The motivation of the combination is based on the fact that infeasible requirements can be transformed into assertion validity problem verifiable with various analyses. This study considers two analyses Value Analysis (forward) and Weakest Precondition calculus (backward) as basis of the combination. The idea is to compute an over-approximation of all reachable program states with Value Analysis(VA). Then with the Weakest Precondition(WP) and an assertion to check, the goal is to compute a proof obligation equivalent to the validity of the assertion. The combination improvement is to extract relevant information from the state approximation of VA for the property to check, and to submit them as assume to WP to enforce and improve its decision power. This communication is performed in a Grey-box manner, by inserting assume annotations in the common annotation language used (see the next Section 9.4.4). Let P , be a program, and A a set of assertions in P which we want to check the validity.

The combination VA ⊕ WP depicted hereabove is divided in different steps: (1) VA analysis computes once for all a state approximation S of the program. (2) For each a ∈ A, if a is valid the method terminates. Otherwise, the greybox part starts by extracting the set R a of variables and locations relevant to a. Next, the set R a and the previously computed approximation S are used to deduce properties of relevant variables that will be submitted as hypotheses to the last step. (3) a WP analysis step checks if the assertion a can be proven valid using the additional hypotheses in H.

Advantages

The proposed combined approach takes benefit both from the global precision of the approximation computed by VA for the whole program and the local precision of analysis for a given assertion ensured by WP. Therefore, this technique is likely to provide a better precision than the two methods used separately. Careful selection of information transferred from VA to WP tries to minimize information exchange: the amount of useless (irrelevant or redundant) data is reduced, thanks to the greybox combination. On the other hand, even if not being purely black-box, the grey-box approach remains lightweight and non-invasive: only basic knowledge of the WP technique is required to implement the validation step, and only basic knowledge of datastructures and contents of approximations computed by VA is necessary to query them and to produce hypotheses at the H V A P step. Neither VA nor WP requires any modification of the underlying algorithms. Moreover, the approximation S is computed only once, and then used for all assertions. These elements are the foundation of the two methods combination.

Implementation

This combination was developped within the LTest testing toolkit [Bardin2014TAP] into a component called LUncov dedicated to the detection of infeasible test requirements. This toolkit uses the DSE engine PathCrawler [START_REF] Williams | PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis[END_REF] itself included as a plugin into Frama-C [START_REF] Cuoq | Frama-C: A Software Analysis Perspective[END_REF]. Thus, this combination takes advantage of both Abstract Interpretation (Value Analysis) and Weakest Precondition analysis provided with Frama-C. Also, Frama-C provides a common Abstract Syntax Tree (AST) and a ANSI/ISO C Specification Language (ACSL) [START_REF] Cuoq | Frama-C: A Software Analysis Perspective[END_REF] to express annotations used by LTest to generate test requirements. Thus, hypotheses H are implemented as ACSL annotations assumed to be true.

Example

The use case presented in Figure 9.1 aims at emphasis benefits of combining both Value Analysis and Weakest Precondition to prove properties that would not be possible otherwise. Note that Frama_C_interval is a built-in Frama-C function that return a non-deterministic value into the given range and used by the different Frama-C analyses.

int main () { int a = Frama_C_interval (0 ,20) ; int x = Frama_C_interval ( -1000 ,1000) ; return g (x , a ) ;

We then compared the percentage of infeasible requirements detected per program and per criterion with 3 methods. (1) abstract interpretation alone with VA, (2) weakest precondition alone with WP and (3) VA ⊕ WP the combination of the two. Table 9.5 gives the results in terms of detection for each pair program/criterions.

From these results it becomes evident that all the studied methods detect numerous infeasible requirements. VA detects 84 infeasibles requirements, WP 73 and the combination of the two 118. Out of the three methods, our combined method VA ⊕ WP performs best as it detects 98% of all the infeasible requirements. The VA and WP methods detect 69% and 60% respectively. Interestingly, VA and WP do not always detect the same infeasible labels. For instance, WP identifies all the 11 requirements in fourballs-WM while VA finds none. Regarding the utf8-3-WM, VA identifies all the 29 labels while WP finds only two. This is an indication that a possible combination of these techniques, such as the VA ⊕ WP method, is fruitful. Thus, VA ⊕ WP finds at least as much as VA and WP methods on all the cases, while in some, i.e., replace-WM and full_bad-WM, it performs even better.

These results have shown that the combination VA ⊕ WP performs better than VA or WP alone, and achieve a 98% rate of detection on our benchmarks. Thus, the combination of forward/backward analyses sketched at the begining of the chapter shows that it finds application beyond binary analysis.

Real-World case studies

This chapter discusses two case studies aiming at emphasizing the efficency of detection methods designed in the previous Chapter 8. The first case study examined is a free evaluation of the detection algorithms on packers. The second, one is more targeted to a single piece of malware which particularity is to be heavily obfuscated and to have been used in severe targeted attacks.

Large scale evaluation of packers 10.1.1 Context & Dataset

Packers Packers are programs embedding another program. This can be done for compression purposes but its more usually done for protecting the embedded software of the reverse-engineering. While they can be used for legitimate purposes lots of malware are using either commercial or custom packers to hide their code. Because packers are usually the first layer of protection to be broken before any in-depth malware analysis, performing a large scale analysis on them is worthy. In addition, experience shows that packers are more likely to use obfuscation than malware payload that usually relies on such overlay of protection. We want to see if our techniques are able to detect OPs or CS tampering on real packers.

Targeted obfuscation

The two obfuscations directly targeted are opaque predicates and call/stack tampering thouroughtly discussed in Section 8.1 and 8.2. Hence, performing these two analyses in a black-box manner, without prior knowledge of the code is a great way to validate at a larger scale the efficiency of the two detection analyses.

Dataset

The packer set originates from previous studies performed on standard packers, especially concatic disassembly benchmarks [START_REF] Bonfante | CoDisasm: Medium Scale Concatic Disassembly of Self-Modifying Binaries with Overlapping Instructions[END_REF]. All packers are Windows binaries used to pack the hostname utility. Choosing hostname as stub binary is totally arbitrary but has the advantage to be small and to provide a good oracle to know whether or not the packing succeed and whether the binary kept the same observable behavior or not. The list of packers is not exhaustive as newcomers appear regularly but still provide a large representative panel (33). A priori, we do not know if there is any opaque predicates or call/stack tampering. The only obfuscation surely present is the self-modification.

Evaluation Settings

The instrumentation was limited to 10M instructions. All samples reaching this limit were not analysed because yielding a partial trace. The dynamic instrumentation appeared not to be perfect, due to the number of process, threads created and all the counter-measures used within the packers. As a sanity check, we ensure that the execution trace was successfully created without unexpected termination (tr.ok) and if the hostname of the machine appeared at the end of the execution (host) in order to analyse the trace. Also as a comparison with the previous study, the number of waves detected is put in perspective between Codiasm and Binsec. The modeling varies and thus impact the number of waves yielded. The difference lays in the way to propagate the marking of memory while doing the dynamic instrumention and is discussed in Annex B.

Analyses

The bound used for the opaque predicates detection is 16 as it emerged as the best value from the benchmarks performed in Section 8.1.3. We note, OK, OP, To and Covered, the predicates which are respectively not opaque, opaque, unknown (because of timeout) and fully covered (both branches) by the dynamic instrumentation. The call/stack tampering is run without specific parameters.

Results

Some results of the previous study are given like the number of processes (#proc) and the number of threads(#th) spawned. Table 10.1 gives the complete results of the two analyses. Interestingly, some packers do not make use of obfuscation while others seems to use it heavily e.g Crypter. Discriminating true positive from false positive would require to check all of them individually. It is worth noting that we only detect OPs and CSTs and it is very likely that packers are using way more tricks. The first constatation is that both algorithms scale well on most samples and succeed in finding both OPs and CSTs. Anomalies Among the 33 packers, three of them (Enigma, svk, Themida) reached the 10M instructions and were consequently not analysed. Similarly, Molebox, Mystic and Setisoft led the analysis to fail by filling the memory. Another anomaly is raised by ACProtect and Crypter. The trace was successfully retrieved but the machine hostname did not appear on the terminal during instrumentation which might indicate that the binary was not well packed. Finally, the last anomally is due to the trace size of certain packed malware which are suspiciously small like JD Pack(42), Obsidium(21) or Yoda's Protector(17). The two explanations for that are either the instrumentation got detected and the process stopped, either the packers kept working in a different process/thread that the instrumentation did not managed to catch up.

Detection results

Except for Molebox, Mystic and Setisoft the analysis succeed on all packers. Thus, it scales well on few millions instructions traces. It managed to find 149 call/stack tampering and 420 opaque predicates. Quantifying the number of false positive would require an exhaustive verification but manual checking revealed that most of them are true positive.

Closer look at the results

Given the amount programs and the amount of predicate tested, it is not possible to check manually all the results, but some manual inspection yield interesting scheme and patterns described below.

Opaque predicates While some packers do not seem to really use OP with a very few OP detected (probably false positive) other packers are using it heavily like ACProtect, Molebox or PE Lock. Most predicates found are strictly exclusive conditions as shown in listing 10.1.

f7a js 0 x1018f92 f7c jns 0 x1018f92

Listing 10.1: Sample of opaque predicate ACProtect Every pair of conditions were found js/jns, ja/jbe, jp/jnp, jo/jno etc. This example shows that our approach successfully detect both invariant and contextual opaque predicates. Funnily Armadillo uses the classic xor, jnz pattern as shown in listing 10.2. Call/Stack tampering Only ACProtect and Crypter are heavily using call stack tampering. ASPack also do but at a lower scale. Meanwhile, patterns used are rather trivial. The most common is push; ret. ACProtect is brutal in its approach as the first 4 instructions executed are two violations (see listing 10.3). It also uses slightly more evolved patterns with in-place violation as given in listing 10.4. Last, packers seemingly using call/stack tampering are using the ret instruction to perform the transition to the last self-modification layer. Packers using a tampered ret to perform the transition to the payload are: ACProtect, ASPack, Crypter, Mew, nPack, PE Lock, TELock, Upack, WinUpack and Yoda's Crypter. since the stack pointer read the ret address at the wrong offset. In the second example (Figure 10.1), the return value is modified in place. The tampering is detected with the [violated], [aligned], [single] tags as it jumps to the return site with an offset of +1. The last example (Figure 10.3), takes place between the transition of two selfmodification layers and the ret is used to do the tail transition with the payload of the packer. This violation is detected with [violated], [disaligned], [single] since the analysis matches an unrelated call far upper in the trace with a different return site. Note that the instruction push 0x10011d7 at 10043ba is originally push 0 but is patched by the instruction at 10043a9 triggering the entrance in a new auto-modification layer when executing it. Nevertheless, this experiment highlighted the fact that multiple packers are using ret as tail transition to enter the original entrypoint. Thus, call/stack tampering is a really good candidate to detect the transition to the payload. This detection is the key-point of generic unpacker algorithm, thus using call/stack tampering analysis can be of a great help for such task as the last violation will probably be the transition to the payload.

X-Tunnel: Sednit/APT28 proxy deobfuscation 10.2.1 Context & Samples

The use-case X-Tunnel is a ciphering proxy component aiming at exfiltrating data from a machine not directly reachable from internet. This malware was used as part of various targeted attack campains (APT). The group behind these attacks is named Sednit [START_REF] Calvet | Visiting The Bear Den, A Journey in the Land of (Cyber-)Espionage[END_REF] but also APT28, Fancy Bear, Sofacy or Pawn Storm group. This group is active since 2006 and mainly targets geopolitical entities. Among attacks alleged to this group we can mention NATO [START_REF] Micro | Operation Pawn Storm, Using Decoys to Evade Detection[END_REF], EU institutions [START_REF]Sednit APT Group Meets Hacking Team[END_REF], the White House [START_REF]Trend Micro. Operation Pawn Storm Ramps Up Its Activities; Targets NATO, White House[END_REF], the dutch team in charge of the MH17 crash investigations [START_REF]Pawn Storm Targets MH17 Investigation Team[END_REF], the german parliaments [von15], the french TV channel TV5 Monde [START_REF] Paquette | Piratage de TV5 Monde: L'enquête S'oriente Vers La Piste Russe[END_REF] and more recently the American Democratic National Committee (DNC) [START_REF] Alperovitch | Bears in the Midst: Intrusion into the Democratic National Committee[END_REF]. As an appreciation of the group sophistication, for the single 2015 year 6 zero-days (0-days) where used, 2 in Flash, 1 in Office (RCE), 2 in Java and 1 in Windows LPE. This group also uses advanced malware tools like Rootkits, USB Command-and-Control (C&C), bootkits dropped by their custom exploit-kit and recently highly pervasive Mac OS X malware named Komplex [START_REF] Creus | Sofacy's 'Komplex' OS X Trojan[END_REF]. Answering this question requires to be able to analyse the obfuscated binaries. Table 10.2 gives the basic information about the samples. As suggested by the results, the number of instructions in obfuscated samples is almost twice as big as the original sample while the number of imported functions remains almost constant.

Analysis context A quick code gazing reveals the presence of opaque predicates in the code. Unlike previous case-studies, the analysis have to be performed statically for the following reasons:

• as the malware is a network component, it requires to connect to the C&C server (which we are definitely not eager to, with such attackers);

• as it listens on the network, all branching conditions to cover the program would be network-event based thus unreliable and more hardly reproducible (which would also require infected client to connect to xtunnel);

• X-Tunnel does not look to use any self-modification obfuscation or neaty tricks to hamper the disassembly. Thus the whole disassembled code is available.

For these reasons running the analysis statically will be easier and will provide a full coverage of the program. In addition, the opaque predicate is performed fully symbolically (does not use runtime values) thus running the analysis statically does not change the inner working of the analyse.

Goal

The goal of this analysis is to detect and remove all opaque predicates along with their dead-code in order to find the potential new functionality afterward. This is a two step process (1) identifying the obfuscated code and pruning it, (2) finding the potential functionalities. We focus in this analysis on the first step which is a prerequisite for the second. Thus, we need to find a way to simplify the CFG in order to make the second step possible.

Approach & Analysis setup

Analysis setup This analysis will be static SE but working like a DSE analysis as opaque predicates analysis is fully symbolic. As described hereafter, all the process will be driven by Idasec that will submit all sub-traces to Binsec running in server mode.

The obfuscation seems to have been done on a per function basis so the analysis will also be performed on a per function basis. Taking advantage of benchmarks previously done, we will use k 16 as the bound value for the bb-dse. The solver used is Z3 with a 6s timeout.

Binsec From the Binsec perspective, the analysis is slightly different. Indeed in DSE when reaching a conditional branches, one of the two branches is necessarily taken. Thus solely the other branch need to be checked. In static SE both branches need to be checked to find out if the predicate is opaque. Also, different from DSE, if both branch are unsat we mark the predicate as likely-opaque since the unsatisfiability is necessarily due to path constraints not satisfiable which mean the predicate is unreachable.

Idasec Most of the computation tasks will be driven by Idasec as it has the complete view of the program and its CFG. The first thing performed is the enumeration of paths leading to every conditional jump of the program. For a conditional jump to check, the choice has been made to compute the shortest path from the function entry point as a reference path. This path is then used to create an artificial execution trace sent to Binsec for solving. The shortest path computation is performed by a classic dijkstra algorithm performed on basic blocks. This allows to know for any instructions its depth in the function. Idasec also performs a basic predicate synthesis to identify the predicate used and also an unobfuscated reduced CFG extraction based functionality. The two are described below. For convenience, the analysis in Idasec allows to perform the analysis with different levels of granularity:

• on a predicate

• on a function

• one the whole program

Exploiting results Results are processed by Idasec which performs further computation to extract relevant information. These computations require the two following components developped for that purpose:

• Internal SMT representation A tiny SMT representation is embedded allowing to perform computation on the generated formula. As the formula represents the logic relation of a predicate it allows to perform semantic manipulation. It is used to perform the dependancy analysis and to retrieve all the spurious instructions involved in the predicate computation. The predicate synthesis also makes use of this functionality.

• Internal CFG representation The CFG given by IDA is superficial and not extendable. Thus, Idasec holds an internal representation providing all the information about paths to a specific address. It also can provide a safe path to a specific address ensuring no possible back edges within that path. Lastly, this CFG allows to tag basic blocks and instructions if user defined information.

Post-analysis processing Idasec performs three post-analysis computations on results, (1) liveness propagation, (2) reduced CFG extraction and (3) predicate synthesis.

Here are some insight on the inner working of the different algorithms:

• Predicate "synthesis" This algorithm allows to retrieve the instructions involved in the computation of a predicate and gives an higher level view of the predicate used which allows to quickly identify OPs. We call spurious instructions all instructions involved in the computation of an opaque predicate. Synthesis is improperly used here as it does not use formal synthesis algorithm usually denoted by this term. This algorithm works on the SMT representation of the predicate. For a conditional jump it looks for the two parameters used in the comparison associated and recursively replace them by their definition. Some normalization is also performed for instance x × x is replace by x 2 . At the end of the recursion all register or memory cells are replaced by placeholders (x, y, z etc) to obtain the generic predicate;

• Liveness propagation This analysis is used to mark basic blocks and instructions with annotations namely alive, dead and spurious. This analysis uses OP results to propagate from the entry point the liveness of basic blocks, marking them with theirs status. For each function, it starts from the entry point and follows the CFG. When reaching a good condition, it follows both branches, otherwise it follows only the alive branch and remove the dead edge in the CFG. All unmarked blocks are consequently tagged dead. Finally, all alive instructions in basic blocks are marked alive except for spurious instructions which are marked spurious;

• Reduced CFG extraction This analysis aims at recovering a readable and unobfuscated CFG of a function. Using information computed by the liveness propagation, the CFG extraction algorithm remove all dead basic blocks of the CFG and all edges pointing to them. After this operation, it remains only basic blocks containing legitimiate and spurious instructions. Then, the algorithm will strip spurious instructions and concatenate within the same basic block all instructions having a single predecessor. This operation is performed while not encountering an instruction with multiple successors. This works well as the liveness propagation will have removed dead edges.

Results

Execution time

The analyses were performed on the whole program of the two obfuscated samples. Table 10.3 reports the execution time. Less than two hour is clearly acceptable for samples of this size. The predicate synthesis takes a non-negligible amount of time but it was not especially designed to be efficient. The 10 predicates per second should be put in perspective as it includes sub-path creation, solving for both left and right branches and also network communications. OP diversity Each sample presents a very low diversity of predicates used. Indeed solely 7x 2 -1 = x 2 and 2 x 2 +1 = y 2 + 3 where found to be opaques. It is worth noting that the later was new to our knowledge and has never been seen elsewhere. Table 10.4 sums up the distribution of the different predicates. The amount of predicates and their distribution supports the idea that they were inserted automatically and chosen randomly.

Detection results

As the diversity of opaques predicates is very low, we are able to determine, with quite a good precision, the amount of false negatives and false positives based on the predicate synthesized. If a predicate matches one of the two OP and was detected OK, then we considered it false negative (respectively false positive). Results are given in Table 10.5. From one sample to the other results are similar except that one of them yielded a timeout. The detection rate is satisfactory as false negatives only represent 2.4% of all predicates but conversely 9.7 to 10.5% of false positive are wrongly tagged opaque. We only test on path (the shortest) for each predicates. As consequence, most false positives are due to wrong path the selection. An exemple is shown in Figure 10.4a where the shortest-path selected going through the xor ebx, ebx which makes the predicate cmp ebx, 0x7f to be always false. Also, we marked likely-opaque, predicates for which both branch conditions evaluate to unsat. This is due to the high density of opaque predicates and are mostly occuring when another OP is in the path predicate. Indeed, even though the backward bound is only 16 it is frequent that the path to a legitimate predicate goes through another opaque predicates that makes the path predicate unsat. Figure 10.4b illustrates this issue where the jz is flagged opaque because the shortest-path has select the green edge which is the dead branch of another opaque predicate.

Dependency evaluation

As seen above, a large k bound can lead to false positive due to nested opaque predicates while in the meantime a low bound miss some predicates.

An example is given in Figure 10.5 where a bound of 24 would have been required to include all predicate dependencies. With k=16 we miss the imul ebx,ebx that would have enforced enough the constraints to detect the predicate. Finding the right balance is still an important issue, but results with 11311 OP detected against 808 false negative tend to confirm that such low bound is enough. Across the two samples, the maximum distance between a predicate and its variable definition where 230 for C637 and 148 for 99B4. Annexe C shows an example of predicates with a distance of 43 between variables declaration and their usage. Still, the average computed on all the OPs yield an average of 8.7. The results obtained are satisfactory in the way that they open the way to further manual triage on doubtful predicates. Difference with O-LLVM The two obfuscated program structures present great similarities with O-LLVM and it has undoubtedly been obfuscated using similar technologies. Yet, interesting differences are to be emphasized. Firstly, there is more interleaving between the payload and the OPs computation. What appeared to be meaningful instruction is often encountered within the predicate computation. Secondly, while O-LLVM opaque predicates are really local to the basic blocks there are here some code sharing between predicates as shown in Figure 10.5 where ebx is used in two opaque predicates. As a consequence, predicates are not fully independent from one another. In the same vein, this obfuscator uses local function variables to store temporary results at the begining of the function for later usage in opaque predicates. This has in consequence to increase the depth of the dependance chain and to complexify the detection.

Obfuscation distribution Surprisingly, not all functions are obfuscated. Conversely, only few functions appeared to be obfuscated. Figure 10.6 shows the distribution of functions considering their level of obfuscation. For each function the level of obfuscation is the percentage of opaque predicates among all conditional jumps. Considering that the obfuscation is generally used to hide the critical parts of the program it can be helpful to focus on these functions. X-Tunnel include various libraries statically linked and most notably OpenSSL. Code simplification After detecting OPs, the next step is to simplify the code by removing dead basic blocks and spurious instructions. Table 10.6 shows the number of instructions classified based on their status. Dead code alone, represents 1/4 of all the program instructions. Computing the difference with the original non-obfuscated program shows a very low difference. Therefore, the simplification pass allowed to retrieve a program which is roughly the size of the original one. The difference is highly likely to be due to the false negatives or missed spurious instructions.

Reduced CFG Extraction

The extraction of the reduced CFG can be made on purpose for a chosen function. It uses the liveness data to extract the unobfuscated CFG.

Conclusion & Futur improvment

Results conclusion This obfuscation is relatively sophisticated compared with existing opaque predicates found ever since. It successfully manages to spread the data dependency accross a function so that some predicates cannot be solved locally at the basic block level. Hopefully, this is not a general practice across predicates so that the bb-dse works very well in the general case. The main issue of the obfuscation is the low diversity of opaque predicates in the way that some pattern matching can come in relay of symbolic approaches to classify a posteriori false positives and false negatives. Finally, this use-case emphasizes the complexity of choosing the appropriate k bound to maximize the detection and to limitate the false positives/negatives rates.

Possible improvements

Various improvements are possible in order to reduce false positives and false negatives. The first, is for a given predicate to compute the opacity with more k-paths which would reduce the risk of having selected the wrong one. The second, would be to compute on the fly the CFG simplification to remove dead edges and basic blocks as soon as possible. This would have in effect to improve the shortest path computation for a more accurate one. Last, an idea is to compute a safe path ensuring it does not go through an already detected opaque predicate or function call. Last, performing a taint on data would enable to detect missing data dependencies while keeping the scalability of the backward-bounded approach without being hampered by path constraints making formulas unsat for both branches.

Towarding finding new functionalities This case-study, showed how to locate highly obfuscated functions (more likely of interest) and how to extract a readable CFG version of them. In order to answer the initial question, some similarity algorithms should be computed between the non-obfuscated and the extracted version. This would help to find the differences and potential new functionalities. The initial question is "is there new functionalities in obfuscated samples ?". We do not give a final answer but the low difference of instructions between the non-obfuscated and the extracted versions supports the idea that it is very unlikely that new functionalities would have been added in the obfuscated samples.

Part V Conclusion

Chapter 11

Conclusion

We have studied in this thesis the application of different formal methods to address obfuscation problematics. The focus has been given to dynamic symbolic execution applied to two unfeasibility based obfuscation, namely opaque predicates and call/stack tampering. In the scope of this study we formalized and developped two DSE variants aiming to scale on obfuscated codes. In support we designed different optimisations. This work has been validated on two significant case studies especially packers and the X-Tunnel malware.

Contributions summary

Flexible Dynamic Symbolic Execution The main contribution of this thesis is the formalization, implementation and testing of an enhanced path predicate computation algorithm integrating concretization and symbolization in a flexible way. All that was facilitated by the conception of a meta-language CSml allowing to specify a wide range of different policies and thus behavior for concrete data. This modularity did permit to benchmark various behaviors highlighting the difference between them and emphasizing the impact of concretization and symbolization on the solving time of the path predicate. To further reduce the solving time different formula optimizations were formalized and developped of which the most notable is the STMC-RoW. Various experiments and benchmarks showed the usefulness of these optimizations to scale on larger formulas. bb-dse Another contribution to the dynamic symbolic execution field of research is the backward-bounded DSE algorithm. This algorithm is scalable, robust and precise for solving infeasibility questions brought by obfuscation. This thesis has demonstrated the benefit of the method for several realistic kinds of obfuscations, such as opaque predicates and call stack tampering. While this algorithm does not supersede existing forward DSE approaches, it complements them by addressing infeasibility questions.

These two algorithms are the answer to "How to make analysis algorithms scaling on real-world obfuscated malwares" stated in the introduction.

Obfuscation detection Deobfuscation is the cornerstone of my thesis subject and was addressed by focusing on two obfuscations, opaque predicates and call/stack tampering. We proposed for each one, a complete taxonomy along with a detection method based on our DSE algorithms. This study provides a throughout study of opaque predicates and call/stack tampering and shows how the bb-dse algorithm has successfully been used on packers and on the real-world malware X-Tunnel. It is worth nothin that call/stack tampering obfuscation have rarely been addressed in state-of-the art research. Such analyses, also unveiled interested properties. For instance it showed that call/stack tampering was able to detect the tail transition from the packer to the payload for packers using ret for making this jump.

Sparse disassembly Beyond simple detection, as one of the main contribution, my thesis formalizes a new disassembly algorithm sparse disasembly lifting obfuscation information computed by DSE in the disassembly process. It empower a dynamic disassembly with a static disassembly guided and improved with obfuscation related data. The few benchmarks performed, yielded promising results. This work paves the way for robust, correct and almost complete semantic-aware disassembly tools for obfuscated binaries.

Experimental Validation

The scalability and the robustness of these algorithms and methods have been validated on commercial packers. Moreover, these techniques found some application beyond the reverse-engineering and the binary analysis field. Indeed, a forward/backward combination approach detailed in 9.4 was successfully used for detecting infeasible test requirements at source-level for software testing purposes. The last validation of my thesis work was performed on the X-Tunnel malware. It showed a concrete example replying to the initial question: "How to locate obfuscation, and how to take it off to make the code more readable and malleable for the reverse-engineer ?". From the localization to the CFG extraction, all steps were performed to remove the obfuscation and to make the CFG usable for the reverse-engineer. Besides that, it showed that algorithms theorized in Part II are applicable and successful on governement-grade malware.

Community contributions

A key idea of this thesis, was to make the algorithm and detection method usable in practice for the reverse-engineering community in order to bridge the gap between academic research and industrial problems. For that, all algorithms were implemented in open-source software namely Pinsec, Binsec/se and Idasec. These three tools provide respectively a dynamic instrumentation tool to gather concrete behaviors of malware, a tool to perform symbolic execution and an IDA plugin allowing to use all these algorithms in a user-friendly manner.

These work and implementation were presented in non-acadamic conferences especially RMLL/Sec [START_REF] Bardin | Binsec: Binary-Level Semantic Analysis to the Rescue[END_REF] and BlackHat Europe 2016 in London [START_REF] David | Code Deobfuscation: Intertwining Dynamic, Static and Symbolic Approaches[END_REF]. The aim of such 11.3. Perspectives initiatives was to fill in the gap between academic research and the reverse-engineering community by providing them both practical approaches and functional tools.

Perspectives

This thesis opens the way to many applications and further improvements. From a purely technical point of view we can improve dynamic analysis by adding more antidebug or addressing more obfuscation schemes but the next step of the work made in this thesis would be to integrate the results of analyses with morphological analysis algorithms developped at the LORIA aiming at providing better and more accurate signatures for malwares.

Formal methods and more especially symbolic approaches provided very good results with dynamic symbolic execution, but another promising usage of symbolic approaches for software deobfuscation is instruction synthesis. This technique showed very good results for optimization matters and very few works have focused on using such approach for deobfuscation.

Over the past few years, the interest in automated binary analysis grew tremendously with the appearance of challenges like the Cyber Grand Challenge [START_REF]DARPA | Cyber Grand Challenge[END_REF] (CGC) and consequently some baseline benchmarks for binary analysis tools [START_REF] Guido | Your Tool Works Better than Mine ? Prove It[END_REF]. The CGC financed by the DARPA greatly intensified the research on various aspect of binary analysis like dynamic instrumentation, binary translation, abstract interpretation and symbolic execution. My thesis humbly contributes on several of these aspects and showed that formal methods can successfully be used for obfuscation related problematics. Especially it tries to bring semantic-aware analyses to the field of malware analysis. Hopefully, this thesis will guide and incitate futur researches aiming at building more accurate malware detection algorithms.

Acronyms

Résumé

L'analyse de codes malveillants est un domaine de recherche en pleine expansion de par la criticité des infrastructures touchées et les coûts impliqués de plus en plus élevés. Ces logiciels utilisent fréquemment différentes techniques d'évasion visant à limiter la détection et ralentir les analyses. Parmi celles-ci, l'obfuscation permet de cacher le comportement réel d'un programme. Cette thèse étudie l'utilité de l'Exécution Symbolique Dynamique (DSE) pour la rétro-ingénierie. Tout d'abord, nous proposons deux variantes du DSE plus adaptées aux codes protégés. La première est une redéfinition générique de la phase de calcul de prédicat de chemin basée sur une manipulation flexible des concrétisations et symbolisations tandis que la deuxième se base sur un algorithme d'exécution symbolique arrière borné. Ensuite, nous proposons différentes combinaisons avec d'autres techniques d'analyse statique afin de tirer le meilleur profit de ces algorithmes. Enfin tout ces algorithmes ont été implémentés dans différents outils, Binsec/se, Pinsec et Idasec, puis testés sur différents codes malveillants et packers. Ils ont permis de détecter et contourner avec succès les obfuscations ciblées dans des cas d'utilisations réels tel que X-Tunnel du groupe APT28/Sednit.

Mots-clés:

Code malveillants, Désobfuscation, Méthodes formelles, Exécution Symbolique, Rétro-ingénierie.

Abstract

Malware analysis is a growing research field due to the criticity and variety of assets targeted as well as the increasing implied costs. These softwares frequently use evasion tricks aiming at hindering detection and analysis techniques. Among these, obfuscation intent to hide the program behavior. This thesis studies the potential of Dynamic Symbolic Execution (DSE) for reverse-engineering. First, we propose two variants of DSE algorithms adapted and designed to fit on protected codes. The first is a flexible definition of the DSE path predicate computation based on concretization and symbolization. The second is based on the definition of a backward-bounded symbolic execution algorithm. Then, we show how to combine these techniques with static analysis in order to get the best of them. Finally, these algorithms have been implemented in different tools Binsec/se, Pinsec and Idasec interacting alltogether and tested on several malicious codes and commercial packers. Especially, they have been successfully used to circumvent and remove the obfuscation targeted in real-world malwares like X-Tunnel from the famous APT28/Sednit group. Keywords: Malware, Deobfuscation, Formal Methods, Symbolic Execution, Reverse-Engineering.

programme prédicat chemin ϕ 1 10 ∧ x 2 > 10 Figure 1 :Contribution # 1 :

 1101011 Figure 1: Prédicat de chemin, concrétisation et symbolisation

Figure 2 :Figure 3 :

 23 Figure 2: schéma pre k

  (a) CFG original (b) CFG marqué (c) CFG extrait

Figure 4 :

 4 Figure 4: Exemples de CFG avant et après réduction

3 Figure 2 . 2 :

 322 Figure 2.2: Win32.Eva Obfuscation tricks

  2: DBA instructions l ∈ loc, loc ∈ (Bv {addr_size} × N) lhs ::= v | v{i, j} | @[ e ] inst ::= lhs := e | goto e | goto l | ite(c)? goto l ; goto l | assert c | assume c | malloc e | f ree e | stop stmt ::= < l, inst > program ::= ε | stmt | stmt ; stmt Some other extensions have been added to DBA, allowing to segment memory in region along with some permissions [DB15]. -

Figure 3 . 1 :

 31 Figure 3.1: Path predicate, concretization and symbolization

Algorithm 1 :

 1 Symbolic Execution algorithm Input: a program P with finite set of paths Π(P ) Output: T S a set of pairs (t, π) such that P (t) covers π T S := ∅; S paths := Π(P ); while S paths = ∅ do π := Sel(S paths ); S paths := S paths \{π} ; ϕ π := C(π) ; switch Sol(ϕ π ) do case sat(t): do T S := T S ∪ {(t, π)}; case unsat: do skip ; end end return T S;

Figure 3 . 2 :

 32 Figure 3.2: Path predicate computation.

Figure 4 . 1 :

 41 Figure 4.1: DSE engine with C/S overview

Figure 4 .

 4 Figure 4.2 gives an exemple of decoherence that might occur when purposely not tracing a given function here myfun. If not handling properly registers or memory that might have been modified by symbolizing them, we can provoke such decoherence. In this example, the stack pointer esp has not properly been updated after the function return because the stdcall except the callee to clean-up its stack. Therefore, two kinds of decoherence may happened:

Figure 4 . 2 :

 42 Figure 4.2: Decoherence exemple by skipping function execution

Figure 4 . 3 :

 43 Figure 4.3: Path predicate computation with C/S policy

Table 4 . 1 :

 41 Policy language policy ::= rules default | default rules ::= rule | rule rules rule ::= guard ⇒ ρ default ::= default ⇒ ρ guard ::= φ loc :: φ ins :: φ expr :: φ Σ φ loc ::= loc | [loc..loc] | * φ ins ::= pinstr | * φ expr ::= pexpr | expr + ≺ term + | expr + term + | * term + ::= expr + | instr + φ Σ ::= P (expr)

Figure 4 . 4 :

 44 Figure 4.4: CSml support in Binsec/se

  Part of results are summarized in Tables 4.9 and 4.10. Firstly, [RQ 1] the choice of C/S policy may greatly affect the outcome of SE: there are ≥5x more sat results on 20/167 examples, and up to 286x more sat results on one program. Secondly, [RQ 2] there is no clear hierarchy between the considered policies. Indeed, even if PP* performs very well on many examples -PP* is the best policy on 41/167 examples, and it is optimal on 117/167 examples (Table

Formally.

  A stub St, is defined by a tuple St (N St , C St , P St ) where N St {Lhs} defines the set of lhs modified by the stub, C St Lhs × Σ * → ρ * defines the actions to perform on a given lhs (as lhs ⊂ Expr). Finally, P StExpr × Σ * → Expr defines the function that performs the propagation for the given lhs and return an expression Expr.

Figure 4 . 7 :

 47 Figure 4.7: Epilog function semantic

(4. 2 )Figure 4 . 8 :

 248 Figure 4.8: memcpy(dst, src, size) propagation function stub

Figure 4 .Figure 4 . 9 :

 449 Figure 4.9 provides an overview of the global integration of the stub mechanism in the DSE engine.

Figure 5 . 1 :

 51 Figure 5.1: Motivating example

  Our DSE algorithm has been implemented in the multipurpose Binsec framework[START_REF] Djoudi | BINSEC: Binary Code Analysis with Low-Level Regions[END_REF]. Far from being DSE centric, Binsec provides low-level API to decode and manipulate instructions in DBA. At the top of it, static analyses, simulation features have been implemented with some interaction in between them.

Figure 6 .

 6 [START_REF]Désassemblage "sparse" de prédicats opaques[END_REF] shows the overall landscape of functionalities.

Figure 6 . 1 :Figure 6 . 2 :

 6162 Figure 6.1: Binsec features overview

(

  define -fun load32_at (( memory ( Array ( _ BitVec 32) ( _ BitVec 8))) ; arg1 ( addr ( _ BitVec 32))); arg2 ( _ BitVec 32); return ( concat ( concat ( concat ( select memory ( bvadd # x00000003 addr )) ( select memory ( bvadd # x00000002 addr ))) ( select memory ( bvadd # x00000001 addr ))) ( select memory addr )) )

Figure 6 . 4 :

 64 Figure 6.4: IDASec main UIs

6. 7 .Figure 6 . 5 :

 765 Figure 6.5: Flare-On #1 CFG decoding loop

Figure 7 . 1 :Figure 7 . 2 :

 7172 Figure 7.1: Solving time mathsat with/without pruning

Figure 7 . 3 :

 73 Figure 7.3: Some propagation rules & rewriting

Figure 7 . 4 :Figure 7 . 5 Figure 7 . 5 :

 747575 Figure 7.4: Constant propagation example

Figure 7 . 6 :

 76 Figure 7.6: Yices solving time w.r.t trace length

Figure 7 . 7 :

 77 Figure 7.7: RoW case #1

Figure 7 . 8 :

 78 Figure 7.8: RoW case #2

Figure 7 . 9 :

 79 Figure 7.9: Example STC-RoW

  Figure 7.9 shows an example of such chain of store. The first load M 5 [100] can be fully substituted with a RoW backtracking 2 times. The second load M 5 [47] can be rebased on M 2 by backtracking 3 times. It cannot be backtracked further as 47 and esp + 4 cannot be logically compared. Formally, we denote St(m, i, x) a store operation in the memory m at index i and the store-chain -→ St < St 0 , St 1 . . . St n >. Then we consider 3 -cmp a three-way comparison function allowing to compare expressions. This function should return true and respectively f alse if both expressions are comparable and respectively equal or not. If two expressions are not comparable the function should return ?. More formally we have: 3-cmp(x, y)

  with: b n , map n Sts .(n) and b st , off st b_of_expr(e st ) ST M C-RoW (load(M n , e ld ) N .(off ld ) if 3-cmp(b ld , b n ) true ∧ off ld ∈ dom(map n ) load(M n-1 , e ld ) if 3-cmp(b ld , b n ) f alse load(M n , e ld ) otherwise with : b ld , off ld = b_of_expr(e ld ) and M n , b n , map n = Sts .(n)

Figure 7 .

 7 Figure 7.11: Z3 solving time w.r.t trace length

  int X , Y , C ; void * threadS ( void * name ) { int R = rand () % C ; sleep ( rand () %10) ; X = R * R ; } void * threadT ( void * name ) { int R = rand () % C ; Y = 7* R * R ; sleep ( rand () %10) ; X *= X ; } int main ( void ) { pthread_t S , T ; C = sqrt ( INT_MAX ) /10;

Figure 8 . 1 :

 81 Figure 8.1: ASPack opaque predicate decoy

Figure 8 . 2 :

 82 Figure 8.2: Opaque predicate detection results

Figure 8 . 3 :

 83 Figure 8.3: Standard stack tampering

Figure 8 . 4 :

 84 Figure 8.4: Tail call to _mbrtwoc

Figure 9 . 1 :

 91 Figure 9.1: Standard coverage criterias

Listing 10 . 2 :

 102 Sample of opaque predicate Armadillo

  Listing 10.3: First instructions of ACProtect 1004328 call 0 x1004318 1004318 add [ esp ] , 9 100431 c ret Listing 10.4: Sample call/stack tampering ACProtect The taxonomy defined in Chapter 8 helped discriminating different kinds of violations found for instance in the ASPack packer.

  Figure 10.2, 10.1 and 10.3 show the exemple of three different kinds of call stack tampering found in the ASPack packer. In the first exemple (Figure 10.2), the tampering is detected with labels [violated], [disaligned]

Figure 10 . 4 :

 104 Figure 10.4: Samples of false positives / Likely predicates

Figure 10 . 5 :

 105 Figure 10.5: False negative in 99B4

( a )

 a Figure 10.6: Fonction obfuscation

Figure 10 .

 10 7 shows different original CFG, with their tagged version (red:dead, orange:spurious) and extracted version. The extracted versions are not executable and still contain noise and thus some oddities in the flow of the CFG. Although, it makes possible reading the CFG while it was simply not possible on the obfuscated version.

  extracted (j) Function #4 CFG (k) CFG tagged (l) CFG extracted

Figure 10 . 7 :

 107 Figure 10.7: Examples of CFG extraction performed on 4 functions 142

Table 1 :

 1 • utilisation des informations de corruption de pile d'appel pour désassembler les cibles de saut d'un ret corrompu et ne pas désassembler le returnsite d'un call dans lequel on ne retourne jamais. Désassemblage "sparse" de prédicats opaques

		pas parfait IDA Objdump	Binsec	gain vs IDA
		obf.				rec. sparse	(sparse)
	simple-if	37	185	240	244	240	185	23,23%
	huffman	558 3226	3594	3602	3594 3226	10,26%
	matrix_multiply 249	854	1075	1080	1075	854	20,67%
	bin_search	105	833	1110	1115	1110	833	24,95%
	bubble_sort	121 1026	1531	1537	1531 1026	32,98%

Evaluation Les benchmarks effectués visent à évaluer la précision du désassemblage de la combinaison par rapport aux algorithmes classiques dans les outils dits grand public. La comparaison est faite avec Objdump fonctionnant en balayage linéaire, IDA mélangeant désassemblage linéaire et récursif et Binsec en mode récursif. Le tableau 1 montre les résultats sur cinq binaires obscurcis avec des prédicats opaques. Les résultats montrent que IDA, Objdump et Binsec (récursif) désassemblent les branches mortes alors que la combinaison dite minutieuse ne désassemble que les instructions réellement exécutables et offrant un gain maximum de 32%.

Détection de vulnérabilité de Use-After-Free

  Ensuite, une couverture des chemins est effectuée en DSE sur ces slice afin de détecter la présence d'une vulnérabilité. En complément différentes heuristiques dédiées ont été implémentées afin de guider l'exploration des chemins de manière plus efficace dans le contexte de la détection d'UaF. L'analyse statique effectuant l'extraction du slice et les heuristiques de choix de chemins ont pour but commun de contourner le problème de l'explosion combinatoire des chemins inhérent à l'exploration des chemins en DSE.Validation expérimentaleCette combinaison a permis la détection de plusieurs vulnérabilités. La plus notable est une vulnérabilité dans la librairie de traitement d'image JasPer ayant menée à la CVE-2015-5221 [Mit15]. Cette vulnérabilité a mis en évidence l'utilité de la combinaison dans la mesure où des outils de fuzzing échouent à détecter la vulnérabilité. Par ailleurs, les heuristiques de guidage pour le DSE réduisent significativement le temps d'énumération des chemins menant à la détection de la vulnérabilité. Cette analyse est développée dans la plateforme Frama-C qui intègre deux greffons, Value et WP, permettant respectivement le raisonnement avant et arrière. La campagne de test est effectuée avec LTest [Bar+14] et Pathcrawler [Wil+05], eux aussi deux greffons de Frama-C. Expérimentations Des benchmarks ont été effectués sur 12 fichiers issus de la suite Siemens et de la suite Verisec. Des critères de couverture usuels tels que la couverture de branches ou encore la couverture de conditions ont été étudiés et encodés sous forme de labels. Sur un total de 1270 critères de tests, 121 se sont révélés infaisables avec une vérification manuelle. En sus, 84 ont été détectés par VA et 73 par WP tandis que la combinaison des deux a permis d'en détecter 118 soit 98%. De façon intéressante, la combinaison permet de détecter certains critères que ni VA ni WP ne sont capables de détecter seuls. 'efficacité des différents algorithmes de DSE développés a été validée expérimentalement sur deux obfuscations différentes et appliquées à deux cas d'utilisation. Les deux obfuscations traitées sont les prédicats opaques et les corruptions de pile d'appel pour lesquels deux méthodologies de détection sont formalisées et implémentées. Ces deux algorithmes ont ensuite été évalués expérimentalement sur un large ensemble de packers et sur le malware X-Tunnel.

	Introduction Ces travaux ont été effectués en collaboration avec le laboratoire Vérimag
	et plus particulièrement Josselin Feist. Cette combinaison a pour but d'étendre les ana-
	lyses symboliques développées au niveau binaire mais appliquées à de la détection de
	vulnérabilité et plus particulièrement des Use-After-Free (UaF). Cette vulnérabilité per-

met si elle est exploitée, l'exécution arbitraire de code grâce à la réutilisation impropre de pointeurs préalablement libérés. Cette combinaison s'articule autour d'une analyse statique par interprétation abstraite visant à extraire un ou plusieurs slice de programmes contenant les évenements clés d'un UaF c-a-d malloc,f ree et use.

Détection de critères de couverture infaisables [code source]

Introduction Ces travaux de thèse et en particulier les différentes méthodes de combinaisons étudiées ont donné lieu à une application dans le domaine du test logiciel au niveau source. Pour une campagne de test, certains critères de couverture doivent être satisfaits afin de considérer le logiciel comme testé. Les critères connus sont : la couverture de décision (DC), la couverture de condition (CC) ou encore les conditions de couverture multiples(MCC). Afin de tester ces critères nous utilisons les labels

[START_REF] Bardin | An All-in-One Toolkit for Automated White-Box Testing[END_REF]

comme formalisme pour encoder ces différents critères de manière générique. Concrètement, au niveau C, un label est une annotation de code traitée ensuite par le moteur de test afin d'en vérifier la validité.

Problématique Ajoutés automatiquement dans tout le code, certains de ces critères se trouvent être infaisables de par la structure du programme. Outre la réduction du taux effectif de couverture, beaucoup de temps est perdu afin d'essayer de couvrir ce critère. Il est donc important de pouvoir détecter en amont ces différents critères infaisables.

Combinaison Inspiré des combinaisons et techniques précédentes, mes travaux proposent une combinaison avant/arrière permettant la détection des critères de couverture infaisables. Cette combinaison se base sur une analyse de valeurs (VA) par interprétation abstraite pour l'analyse en avant et sur du calcul de plus faible précondition (WP) pour l'analyse en arrière. Le but est de calculer une sur-approximation du programme par VA afin d'inclure certains des ces invariants comme hypothèse (donc considéré valide) sous forme de prédicat ACSL

[START_REF] Cuoq | Frama-C: A Software Analysis Perspective[END_REF]

. Le but est d'améliorer le pouvoir de décision du WP, et ce, sans aucune annotation supplémentaire. Cette combinaison VA ⊕ WP est donc effectuée en boîte grise grâce à cette communication d'invariants entre VA et WP. Cette analyse s'effectue en trois étapes: (1) le calcul (une seule fois) de la sur-approximation des états avec VA, (2) pour tous les prédicats non-valides, l'extraction et ajout comme hypothèses des invariants relatifs aux variables du prédicat. (3) analyse WP pour vérifier la validité du prédicat. xxviii Implémentation Contribution #4: Évalution expérimentale L

  Taxonomie La première taxonomie des PO fut proposée par Collberg[START_REF] Collberg | A Taxonomy of Obfuscating Transformations[END_REF] et présente différentes manières d'encoder des invariants dans les programmes servant ensuite à la création de PO. Les différents type d'invariants proposés sont :• Invariants arithmétiques qui utilisent généralement des propriétés d'arithmétique modulaire pour créer des équations sans solution ou bien toujours vraies. Par exemple, 7y 2 -1 = x 2 est toujours vrai quelques soient les valeurs de x ou y et ce même avec les overflow possibles sur des entiers machine; Invariants sur les pointeurs qui se basent sur la difficulté de faire des analyses d'alias et donc savoir si deux pointeurs sont équivalents. Toutes les manières sont bonnes et ce genre d'invariant est facile à créer au niveau source;• Invariants de concurrence qui se basent sur des invariants créés avec des "race condition" entre différents threads temporisés de manière adaptée;• Invariants d'environement qui correspondent à tout invariant lié au système, typiquement en x86 la pile est alignée donc esp mod 4 = 0 est toujours vrai.Détection Dans ma thèse, la détection se focalise sur les PO arithmétiques plus largement répandus. Le but est de détecter l'infaisabilité d'une des deux branches d'un prédicat. Le bb-dse est particulièrent adapté à ce genre de problème. Toute la difficulté

• Invariants de structure de données qui utilisent certaines propriétés des structures de données pour encoder les prédicats. Par exemple on peut créer un tableau dont toutes les cases paires sont divisibles par 2 (x mod 2 = 0) ou encore sur une liste triée où x < x + 1 est toujours vrai;

xxix

Résumé long

• consiste à choisir la borne k adaptée pour englober toutes les dépendances du calcul du prédicat. De par l'aspect dynamique du DSE, une des branches a nécessairement été prise, il ne reste plus qu'à tester la "prenabilité" de l'autre branche par bb-dse. À noter que le pre ≤k sur une trace teste uniquement un sous-chemin. L'algorithme va donc tester tout nouveau sous-chemin candidat pour essayer de déterminer l'opacité du prédicat. Si le chemin est insatisfiable alors le prédicat est opaque; si le chemin est satisfiable alors il n'est pas possible de statuer dans la mesure où un sous-chemin n'a peut-être pas été testé. Dans ce contexte, un faux positif est un prédicat faussement identifié comme opaque et un faux négatif un prédicat opaque non identifié comme tel. A noter que le pre ≤k est incomplet et peut rater des chemins. L'analyse peut donc déclencher des faux positifs et des faux negatifs (prédicats opaques ratés).

Benchmarks Plusieurs benchmarks ont été effectués. Les benchmarks se basent sur O-LLVM

[START_REF] Junod | Obfuscator-LLVM: Software Protection for the Masses[END_REF]

fournissant des passes d'obfuscation dans LLVM et visent à tester l'efficacité de l'analyse en environement contrôlé sur des binaires connus. Pour cela, tous les coreutils Linux ainsi que 5 binaires de test ont été obfusqués puis analysés. L'obfuscation intégrant de l'aléa, il fut possible de dériver plusieurs versions obfusquées d'un même binaire et ce, afin d'obtenir 200 binaires obscurcis. Les benchmarks ont été effectués avec différentes valeurs de k afin d'évaluer la valeur la plus adaptée. Les résultats ont mis en évidence la valeur k=16 comme étant la valeur optimale, maximisant la détection des PO tout en limitant les faux positifs (3.17%) et les faux négatifs (0%).

  Taxonomie Peu de travaux ayant été réalisés à ce sujet, cette thèse propose une taxonomie des différents types des violations/corruptions possibles caractérisées par l'alignement, l'intégrité et la multiplicité. Cette caractérisation permet d'obtenir des indices quant à la nature de la violation, à savoir, un bug ou une action intentionnelle. Les trois caractéristiques sont:

Définition La corruption de pile d'appel désigne l'action de violer l'assertion selon laquelle une instruction ret retourne à l'instruction suivant le précédant call (appelé returnsite). Dans ce cas le ret est dit violé/falsifié. Au niveau machine, un ret est un saut dynamique sur l'adresse en haut de pile. Cette adresse est donc facilement modifiable afin de brouiller le flot de contrôle et brouiller la détection des bornes de fonction. L'exemple de violation le plus simple est le pattern push xx; ret qui écrit une valeur sur la pile puis saute à cette adresse avec le ret.

• l'intégrité, c-à-d la valeur de retour a-t-elle été modifiée? Autrement dit : y-a-t'il eu une corruption ? Les statuts sont désignés par [genuine] ou [violated],

• l'alignement, c-à-d le ret retourne-t-il au même offset sur la pile ? Autrement dit retourne-t-il avec la même valeur pour esp. Les deux statuts possibles sont

[aligned], [disaligned],

• la multiplicité de corruption, plusieurs valeurs de sauts sont-elles possibles ? Les statuts sont [single] ou [multiple]. Détection La détection se base sur le bb-dse. La différence se situe dans le choix de la borne k, qui sera ici adapté à la distance entre le ret et le call afin de pouvoir déterminer si le retour s'effectue à la bonne adresse. Afin de caractériser la corruption trois requêtes SMT sont effectuées : (1) test de la valeur pushé au call et lue au ret pour détecter la corruption, (2) comparaison des valeurs de esp pour caractériser l'alignement et (3), test d'une nouvelle valeur de saut en cas de corruption. Benchmarks Afin de valider l'approche, un benchmark a été effectué avec Tigress [Col+12] permettant l'ajout de corruption de pile d'appel avec les patterns push; call; ret; ret et push; ret. Différents programmes ont été obscurcis de cette manière. Sur 218 ret, 77 étaient légitimes et 141 corrompus. L'analyse a obtenu un taux de détection de 100% sans aucun faux positifs ni faux négatifs (à relativiser dû à la faible diversité des patterns inserés).

  Les packers dont la trace atteignait cette limite n'ont pas été analysés car ils n'ont pas atteint le payload. L'analyse de prédicats opaques a été effectuée avec k = 16, et ce choix se base sur les résultats des précédents benchmarks sur O-LLVM.

Un ensemble de 33 packers open-source et commerciaux sur Windows sont évalués sur un binaire inoffensif (hostname) agissant néanmoins comme témoin du bon fonctionnement du packer. Ce benchmark est issu d'une précédente évaluation effectuée dans la litterature [Bon+15].

Critères d'évaluations

Les packers sont évalués sur la base des analyses de prédicats opaques et de corruptions de pile d'appel. Effectuer l'analyse en boîte noire sans connaissance préalable des codes analysés est une manière pertinente de tester l'éfficacité des analyses sur de véritables programmes obscurcis. À des fins d'évaluation, le nombre de couches d'auto-modification est aussi enregistré. La trace dynamique générée est limitée xxxi à dix millions d'instructions.

Table 2 :

 2 Expérimentation sur packers

						Obfuscation detectée
	Packers	#Tr.len	Prédicats opaques (k 16 )	Corruption de pile
			OK PO To Couvert OK(a/d)	Viol(a/d/s)
	ACPacker	1.802.554 73 209 0	9	0 (0/0)	45 (42/1/42)
	ACProtect v2.0	1.813.598 74 159 0	9	0 (0/0)	48 (45/1/45)
	Aspack v2.12	377.349 32	24	0	136	11 (7/0)	6 (1/4/1)
	BoxedApp v3.2	/	-	-	-	-	-	-
	Crypter v1.12	1.170.108 263 24	0	136	125 (94/0) 78 (0/30/32)
	EP Protector v0.3	250 10	1	0	2	4 (2/0)	0 (0/0/0)
	Expressor	635.356 42	8	0	39	14 (10/0)	0 (0/0/0)
	Petite v2.2	260.025 60	19	0	45	4 (1/0)	0 (0/0/0)
	Yoda's Crypter v1.3	240.900 38	1	0	16	4 (3/0)	9 (0/1/0)

Résultats Le tableau 2 donne les résultats pour quelques-uns des packers analysés. (a/d/s) signifie aligné, désaligné et single pour la caractérisation des corruptions. Les résultats montrent que les deux analyses sont robustes et efficaces sur des traces de plusieurs millions d'instructions. Aussi bien des prédicats opaques que des corruptions de pile d'appel ont été détectés. Ainsi, plus de 150 prédicats opaques et près de 50 corruptions de pile d'appel ont été détectées dans ACProtect.

1.3.2 Contribution #2: Implementation & Optimizations

	• As standard DSE algorithms are performed in a forward manner, we propose a
	new algorithm to modulate the symbolic execution by performing it backwardly in
	a bounded manner. This backward-bounded DSE(bb-dse) formalized in Chapter
	5 allows to address specific problems i.e. infeasibility queries, while forward DSE
	handles feasibility queries. An infeasibility query intents to check infeasibility of
	some events or some configurations in a given environement. The main strength
	of bb-dse is its scalability on any program regardless of the trace length. Exper-
	iments performed showed the effectivness of the algorithm to detect infeasibility
	based problems and more especially obfuscation problems.
	Implementation To validate these algorithms, all of them have been implemented
	and validated on real life examples, thanks to the implementation from scratch of a fully
	featured DSE engine based on Guillaume Jeanne's early work. As a matter of transparency
	and reproducibility, the whole toolkit is available in open-source [ANR16; Dav16]. This
	platform is formed by a dynamic instrumentation engine based on Pin [Luk+05] (∼5000loc
	C++) allowing to generate execution traces and basic debugging interaction. Working on
	both Linux and Windows, it also provides interesting features like function parameters
	retrieval or self-modification layers tracking. Secondly Binsec/se, the main DSE engine
	(∼7000loc OCaml) integrated in the Binsec platform (see Section 6.3.2) managing the
	path selection, the path predicate computation and the interaction with external solvers.
	This engine supports the two DSE algorithms highlighted above but also the different
	formula optimizations described hereafter. Last, Idasec is an IDA plugin allowing to lift
	and process data computed by the DSE engine, for post-analysis data exploitation. It
	provides many features among which it allows to highlight a dynamic trace in the Control
	Flow Graph (CFG) or to trigger an analyse in Binsec/se directly from Idasec.

  2.2 in2 shows a manner to check if the program is being debugged without direct call to isDebuggerPresent. It uses GetProcAddress to retrieve the address of the function which is then called by call ecx. Conveniently,

	}	32	e l s e
	return sum == HASH;	33	p r i n t f ( " F a i l hash \n " ) ;
	}	34 }
	void main ( ) { t e s t ( 0 , 0 , 1 ) ;	Listing 2.3: anti-tampering checksuming
	i f ( hash_fun ( ) )
	p r i n t f ( " Hash OK ! \ n " ) ;
	IsDebuggerPresent is then removed from imports. Finally, listings A.1, A.2 and A.3
	given in annexes, shows respectively: (1) how to check if a certain key is present in the
	Windows registry, (2 )if a given process is running and (3) if the program runs suspi-
	ciously slower than native performance. In the later case it could indicate a debugged or
	instrumented process. These tricks are commonly used to evade dynamic analysis. All
	these examples are very basics but many other advanced techniques are playing with the
	peculiarities of sandboxes and virtual machines to avoid detection.
	1 void * b e g i n , * end ;	12 13	f o r ( i =0; i <nb ; i ++)// a r e a r = r * x ; // checksumed
	2 3 i n t t e s t ( i n t x , i n t nb , i n t dummy) { 4 i f (dummy) { 5 b e g i n = &&b e g i n ; 6 end = &&end ; 7 return 0 ; 8 } 9 i n t r =1; 10 i n t i ; 11 b e g i n :	14 15 16 } 17 18 i n t hash_fun ( ) { end : return r ; 19 const i n t HASH = 3 8 0 1 ; 20 i n t sum = 0 ; 21 char * p=b e g i n ; 22 while ( p<(char * ) end ) { 23 sum += ( unsigned char ) * p++;

Table 2 .

 2

	1: Obfuscation target & Potency summary
		Target	Against
		Control Data Static Dynamic Symbolic
	Conditional Code/Secure Triggers
	Mixed-Boolean Arithmetic	∼
	Opaque predicates
	Call/Stack tampering
	Code diffusion
	Signal/Exceptions
	Virtual marchine (VM)
	Polymorphism (ciphering, packing..)	∼
	Resources ciphering
	Checksuming (code, data)
	anti-debug (VM, debug..)
	Code-overlapping
	Aggregation/Encoding
	(variables split, merge, reordering..)
	Aggregation/Encoding
	(functions split, merge, reordering..)
	Code parallelization
	CFG flattening
	jump encoding (indirect, calculated)
	Variable aliasing

Table 3 .

 3

1: DBA Expressions grammar bv ∈ Bv ({0, 1} n with n size of the bitvector)

Table 3 .

 3 3: Notation : forward symbolic execution

	Symbol Meaning
	Φ	Set of all first-order logic formulas
	Σ	The concrete state of variables and memory
	Σ *	The state of logical variables and memory
	∆	Mapping of location to instructions (loc → Instr)
	ϕ	Logical formula defining the path taken
	Ω

  under-approximate the path predicate, allowing to handle in a precise but limited way parts of an execution which are either missing (e.g. system calls) or too costly to reason about (e.g. hash functions). For instance, concretizing read and write addresses in memory significantly reduces the complexity of the path predicate since the theory of arrays is computationally hard to solve

Symbolization (S) over-approximates the path predicate by introducing a fresh logical variable, allowing to generalize certain program steps, keeping the reasoning exhaustive but less precise. For example, symbolizing eax after a system call is a good way to simulate all possible return values of the call. It can also simulate the non-deterministic values of certain instruction like cpuid or rdtsc Propagation (P) computes the path predicate as explained in Section 3.4, without any extra-approximation.

Table 4 .

 4

		2: Concrete Store policy
	*	:: @?e := ?	:: !e :: * ⇒ C ;
	default		⇒ P ;

  .3. The corresponding policy is shown in Table4.4, where T Σ + (e) indicates whether an expression e is tainted or not in a given extended memory state Σ + (cf. Section 4.3.3).

		Table 4.3: CUTE/DART policy
	*	:: ?i ::	(@ ! ) ≺ !i	:: * ⇒ C
	*	:: ?i :: (! × ? ) ≺ !i :: * ⇒ C
	default			⇒ P
	A variant for memory operations consists in concretizing also all non-tainted expres-
	sions [HG12]. Table 4.4: CUTE/DART policy with tainting
	*	:: ?i :: (@ ! ) ≺ !i :: *	⇒ C
	*	:: *	::	*

Table 4 .

 4

	6: Mayhem policy

:: (@! ) ≺ !i :: card I (! ) < 1024 ⇒ P * ::

?i :: (@! ) ≺ !i :: * ⇒ C default ⇒ P Summary Table

Table 4 .

 4

	7: Encoding of C/S policies
	policy			language
	minimal concretization [minimal]	core language
	recursive concretization	extended ≺
	atomic concretization	[atomic]	extended ≺ and var
	incorrect concretization [incorrect] extended decisions
	r/w full-concrete		[dart/cute]	core language
	r/w full-symbolic	[pathcrawler]	core language
	r/w domain restriction	[osmose]	extended decisions
	r/w multi-level		[exe]	extended ≺
	r/w taint-based		[HG12]	extended Σ +
	r/w dataflow-based		[mayhem]	extended Σ +

Table 4 .

 4

		8: Benchmark characteristics
	category #prog	# trace instr max avg	# trace branch max avg total
	samate	50	5,000 2,772 1,177 333 16,554
	coreutils	100	5,000 1,572 1,053 171 17,198
	malware	17	5,000 3,739 1,539 675 11,490
	total	167	5,000 2,151 1,539 270 45,242

Table 4 .

 4

	9: Summary of #SAT, #UNSAT and #TO (167 programs and 45,242 queries,
	TO 30sec)
		#SAT #UNSAT #TO
	CC 4,518	40,712	12
	PC	4,436	38,897	1,909
	CP	4,651	39,310	1,281
	PP* 4,515	31,320	9,407
	PP	3,340	25,037	16,865
	total number of queries: 45,242

Table 4 .

 4

			10: Best and optimal policies
	samate	coreutils	malware	total
	opt best opt best opt best opt best
	CC 20	0	44	1	5	0	69	1
	PC 20	2	49	4	6	1	75	7
	CP 23	1	61	11	4	0	88	12
	PP* 36	12	71	24	10	5	117 41
	PP 33	9	36	7	7	2	76	18
	total number of programs: 167 -best (resp. opt): number of programs for which the considered policy
	returns the strictly highest (resp. highest) number of SAT answers, w.r.t. the other policies

Table 4 .

 4

		11: Overhead evaluation
			min	max average
	base	PP 0.04%	3%	0.3%
		CC 0.1%	17%	1.2%
	rule-based CP	0.1% 23.5% 1.45%
	C/S policy PC 0.08% 12.8% 0.85%
		PP* 0.08% 12.3% 0.95%
		PP 0.05%	4%	0.48%
		CC 0.05% 8.5%	0.5%
	hard-coded CP 0.05% 8.2%	0.5%
	C/S policy PC 0.05%	8%	0.45%
		PP* 0.05%	6%	0.45%
		PP 0.04%	3%	0.3%

Table 4 .

 4 11 reports the ratio between formula creation and formula creation plus solving. Note that solving time does not depend on the way C/S is implemented. [RQ 3] CSml does lead to a more expensive path predicate computation (average: x3 w.r.t. hard-coded callbacks and up to x5 w.r.t. no C/S at all, at worst x7 on some examples), yet [RQ 4] the cost of predicate computation is still negligible (average of 1.45% for the most expensive C/S policy; maximum of 23% on some easy-to-solve path predicates) w.r.t. the cost of predicate solving. Hence, our rule-based C/S mechanism brings extra-flexibility at only a very slight extra-cost.Threats to validity: besides issues discussed in the previous evaluation, the considered policies are rather simple w.r.t. the expressive power of CSml. While the study is of interest because these policies are representative, further investigations are required for complex CSml policies.

Table 4 .

 4

			12: Best solver summary
		CC	CP	PC	PP*	PP
	best	Yices	boolector boolector boolector boolector
	(#tr.len)	377,309	5,456	6,160	2,700	2,550
	worst	boolector	mathsat	mathsat	mathsat	mathsat
	(#tr.len)	50,938	174	210	987	987

Table 4 .

 4

		13: Call convention summary
	Name	Parameters order	Order on stack clean-up Stack
	cdecl	stack	RTL	Caller
	stdcall	stack	RTL	Callee
	fastcall ecx,edx,stack	RTL	Callee

Table 5 .

 5

	1: Disassembly methods for obfuscated codes
		feasibility infeasibility efficiency robustness query query
	dynamic analysis	/× ( †)	×
	DSE		×	×
	static analysis (syntactic)		/× ( † †)		×
	static analysis (semantic)	×		×	×
	bb-dse	×	( ‡)

Table 5 .

 5

		2: Benchmark DSE versus bb-dse
		bound		Cond. branch		Total
		k	#SAT #UNSAT #Timeout	time
	forward DSE	/	575	7749	2460	17h43m
	backward DSE	∞	575	7748	2461	17h48m
	bb-dse	100	3378	7406	0	18m78s
	bb-dse	20	10730	54	0	4m14s

Table 6 . 1 :

 61 Pinsec execution time overhead comparison

		#instrs native pinsec	instrs
			in (s) in (s)	per sec
	Aspack	377,310	0.015 75.69	4985
	Expressor	635,285	0.995 169.84	3740
	MoleBox	5,257,032 0.735 231.39	22719
	Mystic	4,531,677 0.047 116.50	38899
	PELock	2,389,016 0.165 189.68	12595
	WinUpack 657,406	0.016 77.75	8455
	Avg	2,307,954 0.329 143.47 16086.67

Table 6 .

 6

		2: Path predicate computation time and instruction/seconds
		trace len	CC	CP	PC	PP*	PP
	Aspack	377,310	22.87	23.02	18.67	19.19	17.34
	Expressor	635,285	37.30	37.94	30.38	31.40	28.84
	Crypter	1,170,108	69.79	71.01	61.04	61.51	57.73
	PELock	2,389,016	136.79	141.81	122.30	114.82	109.32
	WinUpack	657,406	51.45	49.83	43.16	47.58	41.15
	Yoda's Crypter 240,900	18.52	19.29	14.54	15.96	15.22
	avg i/s		16245.02 15952.25 18856.30 18832.28 20289.41

Table 7 .

 7

	1: Summary pre-processing optimizations
	pruning	constant	rebase high-level
		propagation		predicates
	∼mathsat	*	*	∼Yices
	* : enables other optimizations

Table 7 .

 7

			2: Backward-Pruning statistics
		#inputs #variables #constraints #terms (total)
	No pruning	619	1,173,269	218,436	1,392,324
	With pruning	61	155,593	84,262	239,916
	Gain	x10	x7.5	x2.5	x5.8

Table 7 .

 7

		3: ecx < 24 binary semantic
	Mnemonic	DBA semantic
	cmp ecx, 24 res32 := ecx -24

Table 7 .

 7 4: High-level predicates mapping[START_REF] Balakrishnan | WYSINWYX: What You See Is Not What You eXecute[END_REF]

	Comparison Conditional instruction instruction	High-level predicate
		ja, jnbe	a > u b
		jne, jnb, jnc	a ≥ u b
		jb, jnae, jc	a < u b
		jbe, jna	a ≤ u b
	cmp x, y	je, jz jne, jnz	a = b a = b
		jg, jnle	a > s b
		jge, jnl	a ≥ s b
		jl, jnge	a < s b
		jle, jng	a ≤ s b
		ja, jnbe, jb, jnae, jc	x = 0
	sub x, y	jae, jnb, jnc, jbe, jna, jge, jnl, jle, jng je, jz	true x = 0
		jg, jnle	x > s 0
		jl, jnge	x < s 0
	test x, y

ja, jnbe, jne, jnz

  Formalization Similarly to the standard RoW we defines by Sts < St 1 , St 2 . . . St n >, the new store chain where St n is an element of the chain. Thus, we defines St n (M n , b n , map n ) the tuple where M n ∈ T A is the memory, b n ∈ Base a base expression and map

	@[esp +]	3→1	cst	100→12	@[ebp+]	10→1
				50→0
		4→0	M₂	40→5	M₅	M₆
	x				M₅[100]➭12
	y				M₅[47]➭M₂[47]
		Figure 7.10: Architecture STMC-RoW

n ∈ (N × Expr). We denote Base {Expr ∪ Csts}) formed of either an expression either a constant value. Based on these definitions we define b_of_expr : Expr → (Base× N an auxiliary function that returns the base and offset of any expression. For instance b_of_expr(esp + 4) = esp, 4 or b_of_expr(43) = (Csts, 43). The update function and the STMC-RoW algorithms are formalized below:

Table 7 .

 7 k backward bound, . x maximum number of value within a map, . n number of load, . m number of store, . y number of map, . (partial) do not simply all possible load, . perf ect simplify all possible load, . WoW Write-Over-Write gained wihtout additional computation (writing over another write on the same index)

		5: Complexity comparison of RoW simplifications
	index	concrete map	store-chain k-store-chain store-map chain
		CM-RoW	STC-RoW kSTC-RoW	STMC-RoW
	constant	n • ln(m)	n.m	n • k	n • ln(m)
	values	(perfect)	(perfect)	(partial)	(perfect)
		+WoW			+WoW
	symbolic (cannot handle)	n.m	n • k	n • y • ln(x)
			(perfect)	(partial)	(partial) +WoW

.

Table 7 .

 7 6: Simplification statistics kSTC Vs STMC RoW

			CC			PC			PP*			PP
		∅	kSTC	STMC	∅	kSTC STMC	∅	kSTC STMC	∅	kSTC STMC
	inputs	119	96	61	119	114	114	119	85	85	119	116	116
	variables	482357 335926 155593 482357 353234 353234 482357 354922 353074 482357 340340 331898
	load	107574 52353	3381	107574 109755 109744 107574 100087 99203 107574 104942 100956
	store	58005	57855	0	58005	57997	57997	58005	57992	57992	58005	58005	58005
	constraints 218778 196691 84262 115357 110269 110269 150928 108131 108126 57361	52280	51217

Table 7 .

 7

			7: Internal optimization statistics kSTC Vs STMC RoW
				CC	PC		PP*	PP
			kSTC STMC	kSTC STMC kSTC STMC kSTC STMC
	replace		73209 129644	4	28	10139	10936	4960	8959
	rebase		63185	2	25	0	111	1091	0	1105
	∅		17	4243	138672 138673 128099 140637 133629 141174
	kSTC: k	min	0	36	0	36	0	1	0	1
	STMC: x max	150	15506	115	15506	149	757	7	264
		avg	5	7506	0	7488	0	15	0	12
	STMC:y		/	1	/	1	/	20581	/	24770

Table 7 .

 7

		8: Path predicate computation time and instruction/seconds
		CC	CP	PC	PP*	PP	avg
	∅	22.09s	22.04s	17.69s	18.56s	16.90s	19.46s
		17081 i/s 17119 i/s 21329 i/s 20329 i/s 22325 i/s 19392 i/s
	C	27.81s	27.38s	23.89s	24.72s	22.64s	25.29s
		13567 i/s 13780 i/s 15794 i/s 15263 i/s 16665 i/s 14920 i/s
	CR	29.41s	28.60s	25.14s	25.78s	24.28s	26.64s
		12829 i/s 13193 i/s 15008 i/s 14636 i/s 15540 i/s 14162 i/s
	CRW	79.32s	30.67s	26.46s	26.61s	25.91s	37.79s
		4756 i/s 12302 i/s 14260 i/s 14179 i/s 14562 i/s	9983 i/s
	CRH	40.84s	30.17s	37.34s	26.97s	26.29s	32.32s
		9238 i/s 12506 i/s 10105 i/s 13990 i/s 14352 i/s 11673 i/s
	avg	39.89s	27.77s	26.10s	24.53s	23.20s
		9458 i/s 13586 i/s 14454 i/s 15383 i/s 16261 i/s
			performed on a 377000 instructions path predicate

Table 7 .

 7

			9: Optimizations formula statistics
			#inputs #variables #load	#store #constraints
		∅	482,357	107,574 58,005 218,778
	CC	C CR	448,919 350,173	107,478 58,005 213,602 106,596 58,005 207,204
		CRH	155,593	3,381	0	84,262
		∅	482,357	107,574 58,005 160,782
	CP	C CR	448,904 339,972	107,478 58,005 155,607 106,596 58,005 149,209
		CRH	334,344	106,585 58,005 149,204
		∅	482,357	107,574 58,005 115,357
	PC	C CR	444,082 353,257	107,478 58,005 110,277 109,759 58,005 110,277
		CRH	353,234	109,744 57,997 110,269
		∅	482,357	107,574 58,005 150,928
	PP*	C CR	438,605 357,549	107,465 58,005 112,124 109,651 58,005 111,092
		CRH	353,074	99,203	57,992 108,126
		∅	482,357	107,574 58,005 57,361
	PP	C CR	444,070 340,396	107,478 58,005 52,282 109,759 58,005 52,282
		CRH	331,898	100,956 58,005 51,217

  Table shows many other OP used in various tools such as Sandmark [Col03].

	mov	eax , ds : x
	mov	ecx , ds : y
	imul ecx , ecx
	imul ecx , 7
	sub	ecx , 1
	imul eax , eax
	cmp	ecx , eax
	jz	< addr_trap > // false jump to junk
	.... ........	// real code

Listing 8.1: opaque predicate: 7y 2 -1 = x 2

  Pointer based invariant Aliasing is known to be a hard problem. Thus, encoding invariant pointer aliasing on specific data-structure is difficult for any automated algorithm. Collberg suggested an example based on circular list. Let's consider Table 8.1: Arithmetic opaque predicates list (non-exhaustive)

	void main () {
	// index :	0	1	2 3	4	5 6	7	8 9	10 11 12 13 14
	15 16 17 18 19
	int g [] = {36 , 58 , 1 , 46 , 23 , 5 , 16 , 65 , 2 , 41 , 2 , 7 , 1 , 37 , 0 ,
	11 , 16 , 2 , 21 , 16};
	g [14] = rand () ; // manipulable because unconstrainted ( no
	invariant )
	if ( g [3] % g [5] == g [2]) {
	// Always get into
	}
	}
	Listing 8.2: Array invariant data-structure

Table 8 .

 8 2: OP status w.r.t left/right branch status

	Left	Right	Status
	Covered Covered	not opaque
	Covered ∃π, pre ≤k π (l, ϕ p ) SAT	unknown
	Covered ∀π, pre ≤k

π (l, ϕ p ) U N SAT opaque Covered ∀π, pre ≤k π (l, ϕ p ) T IM EOU T timeout

Table 8 .

 8

			4: Opaque predicate detection results
	k	OP (5556) ok miss	Genuine (5183) TO ok miss	FP/Tot FP/OP (%) (%)
			(FN)		(FP)
	2	0	5556 5182	1	0	0.01%	0.02%
	4	903	4653 5153	30	0	0.26%	3.22%
	8	4561	995	4987	196	0	1.67%	4.12%
	12 5545	11	4890	293	0	2.50%	5.02%
	16 5556	0	4811	372	0	3.17% 6.28%
	20 5556	0	4715	468	2	3.99% 7.77%
	24 5556	0	4658	525	7	4.48% 8.63%
	32 5552	4	4579	604	25	5.15%	9.81%
	40 5548	8	4523	660	39	5.63% 10.63%
	50 5544	12	4458	725	79	6.18% 11.56%
	. Timeout: 5 sec
	. a TO counts as an UNKNOWN result (hence, classify the predicate as genuine)
	. 10,739 predicates, 5,556 opaque predicates, 5,183 genuine predicates

Table 8 .

 8

			5: Difference without/with multi-path
	K	∅	OK multip gain(%)	∅	FP multip gain(%)
		5182 5182	0.00	1	1	0.00
		5152 5153	0.02	31	30	3.23
		4975 4987	0.24	208	196	5.77
		4872 4890	0.37	311	293	5.79
		4793 4811	0.37	390	372	4.62
		4686 4713	0.57	495	468	5.45
		4623 4651	0.60	553	525	5.06
		4517 4558	0.90	640	604	5.62
		4453 4492	0.87	696	660	5.17
			. ∅ testing only one k-path for a predicate,
		. multip testing all k-path leading to a predicate.

Table 8 .

 8 Conclusion Table8.4 with k=16 achieves a very low false positives rate thus addressing Q1 since there is no more than 2 false positive per samples and the number of false positive can be considered negligible compared to the number of true opaque predicates detected.

		6: Solving time
	k	Total time (s) Avg/query(s) (10,739 queries)
	2	89	0.008
	4	96	0.009
	8	120	0.011
	12	152	0.014
	16	197	0.018
	20	272	0.025
	24	384	0.036
	32	699	0.065
	40	1145	0.107
	50	2025	0.189

  Subsequently, this obfuscation disrupt the high-level function recovery step of disassembly discussed in 2.1.3.

	<main>:	<fun>:
	call <fun>	[...]
	..... // return site push X
	..... // junk code	ret //jump to X instead
	..... // junk code	//of return site

  • integrity: does ret returns to the same address as pushed by the call? Characterize if the tampering takes place or not. A call/ret pair is either [genuine] (returns to the caller) or [violated]; • alignment: does the stack pointer (esp) is equal at call and at ret? If so, the stack pointer is denoted [aligned], [disaligned] otherwise; • multiplicy: in case of violation, is the current ret target the only possible value? This case is denoted [single] and [multiple] otherwise. As such, a well-behaving ret should be marked [genuine] and [aligned]. Conversly, a tampered ret should be marked [violated] with optional tag [single],[multiple] or [aligned],[disaligned].This taxonomy helps discriminating different kinds of violations. Figure8.5 shows an example where the ret does not jump back to the return site with an offset but beyond its own address with an offset. According to the taxonomy defined hereabove the violation is detected as [violated], [aligned], [single] tags as it jumps to the return site with an offset of +8.

	address	mnemonic	comment
	080483d1 call +5	//push 0x080483d6 as return (jump on next instruction)
	080483d6 pop edx	//pop the return address
	080483d7 add edx, 8	//add 8 (size of pop+add+push+ret+invalid)
	080483da push edx	//put back the return value
	080483db ret	//returns at 0x080483de (beyond invalid byte)
	080483dc .byte{invalid} //invalid byte (cannot disassemble)
	080483de [...]	//payload
			Figure 8.5: Violation "call +5"

Table 8 .

 8 esp {ret} ]: Compare logically the content of the value pushed at call (@[esp {call} ]) with the one used to return (@[esp {ret} ]). If it evaluates to UNSAT, a violation necessarily occured ([violated]), valid the predicate returns and cannot be tampered ([genuine]). If sat, the concrete values from the trace are used to characterize the ret integrity; • alignment: esp {call} = esp {ret} : Compare the logical esp value at the call and at the ret. If it evaluates to valid, the ret necessarily returns at the same stack offset ([aligned]), if it evaluates to unsat the ret is ([disaligned]), otherwise the alignment cannot be characterized; • multiplicity: R = @[esp {ret} ]: Check if the logical ret jump target (@[esp {ret} ]) can be different from the concrete value (R) in the trace. If it evaluates to UNSAT the ret cannot jump elsewhere and is flagged [single]. Be aware that [multiple] cannot be found by our approach, unless several distinct (non-legit) targets are observed at runtime. Indeed, finding new targets with DSE would require forward DSE.

		7: Call stack tampering taxonomy
	RT Status	integrity	alignement	multiplicity
		RT: OK	RT: OK/KO [aligned] [disaligned]
	RT Genuine VALID: [genuine] (proved)	-VALID: [aligned] (proved)
	[genuine]	SAT: /	-SAT: /
		UNSAT: ∅	-UNSAT: [disaligned] (proved)
		RT: [violated]		RT: 1/[multiple]
	RT Tampered -VALID: ∅	(idem)	-VALID : ∅
	[violated] -SAT: /		-SAT: /
		-UNSAT: [violated] (proved)		-UNSAT: [single]

Table 8 .

 8 ResultsResults are given in the table 8.8. The first 5 samples, totalize 218 different ret. Among them 77 were genuine and 141 violated. Due to the homogeneity of schemes inserted by Tigress, the diversity of tags is very low but interestingly enough results did not yield any false positive nor false negative.The second benchmark performed yields very interesting results. For instance on AC-Packer, no ret were legit and the fact that almost all of them were flagged [single] means ret are likely be used as static jumps. Results show that stack tampering obfuscation is far from being negligible in these packers since approximately 54% to 100% of all call/rets are tampered in these packers. As an example, three different kinds of tampering were detected in the ASPack packer which correspond to the three examples (see Figures 10.2, 10.1 and 10.3 in Chapter 10).

			8: Call stack tampering results
		runtime genuine	runtime violation
	Sample	#ret † proved align/ #ret † alig/ proved
			genuine disal		disal single
	simple-if	6	6	6/0	9	0/0	8
	bin-search	15	15	15/0	25	0/0	24
	bubble-sort	6	6	6/0	15	0/1	13
	mat-mult	31	31	31/0	69	0/0	68
	huffman	19	19	19/0	23	0/3	19
	ASPack	11	9	9/0	6	5/1	2
	ACProtect	0	0	0/0	48	45/1	45
	Crypter	125	94	94/0	78	0/30	32
	PE Lock	4	3	3/0	3	0/1	0

Table 9 .

 9 2 gives the results of the coverage for IDA, Objdump, Binsec (recursive traversal) and Binsecsparse disasembly on few obfuscated samples. Once obfuscated, files are approximately 8 times their original size. IDA uses both recursive disassembly, linear sweep and some heuristics to disassemble. Objdump does linear-sweep only. IDA and Binsec results are almost identical because none of the samples appear to have indirect jumps. The Objdump linear-sweep always over-disassemble some bytes at the end of functions. Interestingly, the sparse disasembly provides an average gain of 22.48% in terms of instructions coverage. The number of instructions is still far bigger than the original program. So, while it is possible to prune the dead branches, the instructions computing the opaque predicate still have to be computed. Similarly, we have performed a call/stack tampering benchmark on programs obfuscated this time with Tigress. In contrast to the previous benchmark, the aim is to have the bigger (yet accurate) possible coverage. The obfuscation turns every conditional jumps into calls and rets. No any additional spurious instructions are introduced. For this reason, the approximate size of obfuscated programs is only twice bigger.

		Table 9.2: Sparse disassembly opaque predicates
		no			Obfuscated			gain
	sample	obf. perfect IDA Objdump	Binsec	vs IDA
						rec. sparse (sparse)
	simple-if	37	185	240	244	240	185	23,23%
	huffman	558 3226	3594	3602	3594 3226	10,26%
	matrix_multiply 249	854	1075	1080	1075	854	20,67%
	bin_search	105	833	1110	1115	1110	833	24,95%
	bubble_sort	121 1026	1531	1537	1531 1026	32,98%
	Call/Stack tampering

Table 9 .

 9

			3: Sparse disassembly stack tampering
		no			Obfuscated			gain
	sample	obf. perfect IDA Objdump	Binsec	vs IDA
						rec. sparse (sparse)
	simple-if	37	83	95	98	30	83	14.45%
	huffman	558	659	678	683	526	659	2.80%
	matrix_multiply 249	461	524	533	23	461	12.0%
	bin_search	105	207	231	238	47	207	10.39%
	bubble_sort	121	170	182	185	89	170	6.6%

Table 9 .

 9

			4: Sparse disassembly coreutils
				Obfuscated
	sample	Tr.len Objdump	IDA	Dynamic	Binsec
					disas.	rec.	sparse
	basename 1,783	20,776	20,507	1,159	8,163	7,894
	env	3,692	19,714	19,460	477	6,916	6,743
	head	17,682	32,840	32,406	1,299	20,098 19,807
	mkdir	1,436	57,238	56,767	1,407	10,562 10,428
	mv	14,346 115,278 114,067	5,261	82,502 81,596

Table 9 .

 9 5: Infeasible Label Detection Power

	Program LOC Crit. #Lab #Inf	VA	WP	VA ⊕ WP
						#D	%D #D	%D #D	%D
	trityp	50	CC	24	0	0	-	0	-		-
			MCC	28	0	0	-	0	-		-
			WM	129	4	4 100%	4 100%		100%
	fourballs	35	WM	67	11	0	0%	11 100%		100%
	utf8-3	108	WM	84	29	29 100%	2	7%		100%
	utf8-5	108	WM	84	2	2 100%	2 100%		100%
	utf8-7	108	WM	84	2	2 100%	2 100%		100%
	tcas	124	CC	10	0	0	-	0	-		-
			MCC	12	1	0	0%	1 100%		100%
			WM	111	10	6	60%	6	60%		100%
	replace	100	WM	80	10	5	50%	3	30%		100%
	full_bad	219	CC	16	4	2	50%	4 100%		100%
			MCC	39	15	9	60%	15 100%		100%
			WM	46	12	7	58%	9	75%		92%
	get_tag-5 240	CC	20	0	0	-	0	-		-
			MCC	26	0	0	-	0	-		-
			WM	47	3	2	67%	0	0%		67%
	get_tag-6 240	CC	20	0	0	-	0	-		-
			MCC	26	0	0	-	0	-		-
			WM	47	3	2	67%	0	0%		67%
	gd-5	319	CC	36	0	0	-	0	-		-
			MCC	36	7	7 100%	7 100%		100%
			WM	63	1	0	0%	0	0%		100%
	gd-6	319	CC	36	0	0	-	0	-		-
			MCC	36	7	7 100%	7 100%		100%
			WM	63	0	0	-	0	-		-
	Total			1,270	121	84	69%	73	60%		98%
	Min				0	0	0%	0	0%		67%
	Max				29	29 100%	15 100%		100%
	Mean				4.7	3.2	63%	2.8	82%	4.5	95%
	#D: number of detected infeasible labels %D: ratio of detected infeasible labels
	-: no ratio of detected infeasible labels due to the absence of infeasible labels

  ConclusionAs suggested by the manual look at the results, most artifacts detected are true positive. False positives for opaque predicates are mostly due to the program structure making the other branch of a predicate to be infeasible. Results showed that certain packers do use opaque predicates but really trivial ones unlike the ones developped in O-LLVM.Call/stack tampering is less employed as it is more difficult to craft such obfuscation. Only, ACProtect, ASPack, Crypter and Yoda's Crypter seem to use it on purpose.

	address mnemonic		layer comment
	10043a9 mov [ebp+0x3a8], eax	0	//Patch push value at 10043ba*
	10043af popa		0	//restore initial program context
	10043b0 jnz 0x10043ba		0	//enter last SM layer (payload)
	Enter Layer 1
	10043ba push 0x10011d7		1	//push the address of the entrypoint
	10043bf ret		0	//use ret to jump on it
	10011d7 [...]		1	//start executing payload
	*(at runtime eax=10011d7 and ebp+0x3a8=10043bb)
	Figure 10.3: ASPack violation 3/3 (trace)
	address len mnemonic	comment
	1004a3a 5	call 0x1004c96	//push 0x1004a3f as return site
	1004c96 5	call 0x1004c9c	//push 0x1004c9b as return site
	1004c9c 1	pop esi		//pop return address in esi
	1004c9d 5	sub esi, 4474311
	1004ca3 1	ret		//return to 0x1004a3f
	Figure 10.1: ASPack violation 1/3 (trace)
	address mnemonic	comment
	1004002 call 0x100400a //push 0x1004007 as return
	1004007 .byte{invalid} //invalid byte (cannot disassemble)
	1004008 [...]		//not disassembled
	100400a pop ebp	//pop return address in ebp
	100400b inc ebp	//increment ebp
	100400c push ebp	//push back the value
	100400d ret		//jump on 0x1004008
	Figure 10.2: ASPack violation 2/3 (CFG)

Table 10 .

 10 Samples This use-case is based on 3 X-Tunnel samples, kindly provided by Joan Calvet formerly at ESET Montreal[START_REF] Calvet | Visiting The Bear Den, A Journey in the Land of (Cyber-)Espionage[END_REF] (I warmly thank him again). These three samples have apparently been compiled at few months of difference. The particularity is that the first sample dated of the 25/06/2015 is not obfuscated while the two others are. The last sample was compiled the 02/11/2015 thus these three samples are if timestamp are corrects, somewhat covering the evolution of the software on a 5 month period. The main issue raised is:

			2: Samples infos
		Sample #1	Sample #2	Sample #3
		42DEE3[...]	C637E0[...]	99B454[...]
	Obfuscated	No	Yes	Yes
	Size	1.1 Mo	2.1 Mo	1.8 Mo
	Date creation	25/06/2015 5h15m34 02/07/2015 9h42m44 02/11/2015 8h45m54
	#functions	3039	3775	3488
	#instructions	231907	505008	434143
	Mean instr/fun ∼76	∼134	∼125
	#imports	133	139	135

RQ: Is there new functionalities in the obfuscated samples ?

Table 10

 10

	.3: Execution time

Table 10 .

 10

	4: Opaque predicates variety
	OP #1	OP #2
	7y 2 -1 = x 2	2 x 2 +1 = y 2 + 3
	C637 (#1) 6016 (49.02%) 6257 (50.98%)
	99B4 (#2) 4618 (45.37%) 5560 (54.62%)

Table 10 . 5

 105

			: Opaque predicates evaluation
	#pred	OK	OK	FN	OP	OP	FP	OK	Likely OP	To
	C637 (#1) 34505 17196		1046	11973		2968	1156	165	1
		(49.8%) (3.0%) (34.7%) (8.6%) (3.4%) (0.4%)
	99B4 (#2) 30147 16148		914	9790		2543	606	146	0
		(53.7%) (3.0%) (32.5%) (8.4%) (2.0%) (0.5%)
	likely: predicates were both branches were unsat

  Thus authors might have considered useless to obfuscated these functions.

	%pred obfu	C637 (#1)	99B4 (#2)
	0-10%	3060	2906
	10-20%	4	5
	20-50%	0	0
	50-60%	5	7
	60-70%	39	23
	70-80%	110	67
	80-90%	175	131
	90-100%	384	351

distribution of the percentage of obfuscation per function

Table 10 .

 10

		6: Code simplification results
	#instr #alive #dead #spurious alive-(42DE insts)
				(231,907)
	C637 (#1) 507,206	279,483 121,794 (55%) (24%)	103,731 (20%)	47,576
	99B4 (#2) 436,598	241,177 113.764 (55%) (26%)	79,202 (18%)	9,270

  Proxy component aiming at connecting machines not primarly connect on internet to access it. Used as part of targeted attacks of APT28, it is use to exfiltrate data by ciphered channels. i Advanced Persistent Threat represent targeted attacks against certain organization or person performed as a long term process. Such attacks usually involve a whole ecosystem of malware, infrastructure and vulnerability exploits.. i, 151 Agence Nationale de la Recherche French organization for academic research. i, 4, 151 ANSI/ISO C Specification Language is a behavioral specification language for C programs. It allows to express a wide range of properties and is defined as a formal language allowing to perform various analyzes on it. i, 125, 151 anti-debug group all the techniques aiming at preventing the debugging of the software. It can be checking if debugged, attaching to itself etc. i, 14 anti-tampering group all the techniques aiming at preventing the static or dynamic modification of the software. i, 14, 18 anti-VM group all the techniques aiming at preventing the software of being run in a virtual machine (that could indicate being analyzed). i, 14 Application Binary Interface defines the interface between two modules, within the kernel or between use-space programs and kernel. i, 54, 151 Application Programming Interface represent a set of routines definitions, protocols or formats used to facilitate the interaction between two different piece of software. i, 151 APT28 Nickname given by FireEye to identify a criminal group acting since 2007. The same group is identified under other nickname like "Sofacy", "Sednit" or "Pawn Storm". i, 8, 134 bootkit Malicious, software which task is to infect the boot process by interleaving the transition from boot process to the system boot with its own startup. i, 3, 134 Local Privilege Escalation is the mean by which a non-priviledged user gain priviledged access to a machine. i, 151 Low-Level Virtual Machine is a tool-chain providing an intermediate representation LLVM-IR allowing to develop compiler front-ends and back-ends. i, 151 Malware Software developped with the intent to harm a computer system by altering its availability, confidentiality or integrity. i, 3 Mixed-Boolean Arithmetic obfuscation used to obfuscated constant values, or simple condition into linear arithmetic operations. i, 13, 151 Off-The-Shelf idiomatic expression to represent an object (or software) ready to use. i, 25, 152 packer A packer is a program aiming at embedding a program in another. The goal is to compress the packed binary or to protect its content from analysis. Used for intellectual property such programs are also used to hide malwares. i, 8, 18 polymorphism generic term, grouping all software changing of form between two execution or during the execution. It includes self-modification. i, 15, 18 Programmable Logic Controller Industrial digital computer used to control the manufacturing or the operation of physical systems (robots, assembly lines etc). i, 3, 152 race condition specific event or output dependent on the sequencing or timing of uncontrollable events. i, xxx ransomware specific malware ciphering files of the infected machine and requesting the payment of a ransom to decipher files. i, 3 Return-Oriented Programming exploitation technique aiming at bypass not executable stack by using ret instructions of the different functions to encode a shellcode or a specific trampoline. i, 152 right-to-left designate the way parameters are transmitted by the calling convention. i, 53, 152 rootkits Malicious, software running with the kernel permissions. i, 3 Satisfiability Modulo Theories is a decision problem for logical formulas with respect to different theories expressed in first-order logic. i, 21, 152 secure trigger protection technique, aiming at revealing or deciphering the payload of a software only under very specific settings. The setting or environment triggering the deciphering is designed to be hardly guessed and is thus secure. i, 15

	OTS Off-The-Shelf. i, 25, 152, Glossary:
	Off-The-Shelf
	PLC Programmable Logic Controller. i, 3,
	152, Glossary: Programmable Logic
	Controller Glossary
	QF_ABV Qantifier-Free Array and Bitvec-
	tors. i, 92
	ABI Application Binary Interface. i, 54, 151, Glossary: Application Binary In-QF_BV Qantifier-Free Bitvectors. i, 92 X-Tunnel	DBI Dynamic Binary Instrumentation. i, 68, 151, Glossary: Dynamic Binary
	terface RCE Remote Code Execution. i, 134		Instrumentation
	ACSL ANSI/ISO C Specification Language. i, 125, 151, Glossary: ANSI/ISO C Specification Language ROP Return-Oriented Programming. i, 19, 152, Glossary: Return-Oriented Pro-gramming	DNC Democratic National Committee. i, 134, 151, Glossary: Democratic Na-tional Committee
	ANR Agence Nationale de la Recherche. i, 4, 151, Glossary: Agence Nationale de la Recherche RTL right-to-left. i, 53, 152, Glossary: right-to-left	DPLL Davis-Putnam-Logemann-Loveland. i, 73, 151, Glossary: Davis-Putnam-Log-emann-Loveland
	API Application Programming Interface. i, SE Symbolic Execution. i, 21, 25	DRM Digital Right Management. i, 11,
	151, Glossary: Application Program-ming Interface SMT Satisfiability Modulo Theories. i, 21, 73, 137, 152, Glossary: Satisfiability		151, Glossary: Digital Right Manage-ment
	Modulo Theories APT Advanced Persistent Threat. i, 134, 151, Glossary: Advanced Persistent Threat LHS Laboratoire de Haute Sécurité. i, 4, AST Abstract Syntax Tree. i, 125 151, Glossary: Laboratoire de Haute TCG Tiny Code Generator. i, 68, 152, Sécurité Glossary: Tiny Code Generator
	C&C Command-and-Control. i, 134, 135, 151, Glossary: Command-and-Control TSC Time Stamp Counter. i, 55, 152, Glos-sary: Time Stamp Counter	LLVM Low-Level Virtual Machine. i, 68, 151, Glossary: Low-Level Virtual Ma-chine
	CFG Control Flow Graph. i, 6, 11, 12, 151, Glossary: Control Flow Graph UaF Use-After-Free. i, 7, 122, 152, Glos-sary: Use-After-Free	LPE Local Privilege Escalation. i, 134, 151, Glossary: Local Privilege Escalation
	CGC Cyber Grand Challenge. i, 151, Glos-sary: Cyber Grand Challenge VPC Virtual Private Counter. i, 18	to-right LTR left-to-right. i, 53, 151, Glossary: left-
	CST Call/Stack Tampering. i	MBA Mixed-Boolean Arithmetic. i, 13, 151,
	DARPA Defense Advanced Research Projects	Glossary: Mixed-Boolean Arithmetic
	Agency. i, 149	NATO North Atlantic Treaty Organization.
	DBA Dynamic Bitvector Automata. i, xxi,		i, 134
	151, Glossary: Dynamic Bitvector Au-
	tomata	OP Opaque Predicates. i, 101

enforced by bounding the depth of the path

Property 5 comes also from the sequential ordering of rules and the presence of a default rule.

https://developers.google.com/protocol-buffers/

http://zeromq.org/

It does not used the standard GDB remote debugging interface for now

http://www.flare-on.com/

A complete demo is available at https://youtu.be/0xUc2jbpjQo

† each ret is counted only once

https://www.ece.uvic.ca/ frodo/jasper

relational domains have very recently been added into VA prior to this work

Remerciements

• dynamic: similar to contextual, but the opaqueness is made by comparing two dynamic configurations that are made to be disjoint thanks to dynamically computed values (eg: two disjoint pointer values etc..) scales on any path length. It all depends on predicates needed to be checked as chown in the previous Chapter 8. Combination interaction Another critical aspect when designing an analysis combination is to determine how the two analyses will communicate and what will the information exchange be. This depends on the information and results produced by the analysis.

For instance, abstract interpretation can transmit information about its invariant (see Section 9.4), while fuzzing or random testing yield inputs and information about covered paths. A strict black-box integration usually weaken the potential of algorithms combination while a gray-box or a white-box combination unleash the analyses potential but is harder to do.

Sparse disassembly: Use-case binary-level 9.2.1 Introduction

Standard disassembly

We call legit an instruction in a binary code if it is part of a real execution of the code. Two qualities expected for a disassembler are (1) safety: does the algorithm recover only legit instructions? and (2) completeness: does the algorithm recover all legit instructions? Standard disassembly approaches essentially include static recursive disassembly, static linear sweep and dynamic disassembly.

• Recursive disassembly consists in exploring the executable file from a given entrypoint, recursively, following the possible successors of each instructions. A recursive disassembly may miss a lot of instruction, typically, because of computed jumps (jmp eax) or of self-modification. Like all static algorithms, the approach can easily be fooled into disassembling junk code from opaque predicates or call/stack tampering spurious bytes. The approach is neither safe nor complete.

• Linear sweep consists in decoding linearly all possible instructions in executable code sections. The technique aims at being more complete than recursive traversal, yet it comes at the price of many additional mis-interpreted code instructions. Like all static techniques it can still miss instructions hidden by code overlapping or self-modification. Hence the technique is unsafe and often incomplete on obfuscated codes. The assertion in function g cannot be proved neither by value nor by wp alone on a platform like Frama-C. value is unable to prove that x+a ≥ x is always true because it lacks of relational domains and does not recognize that the x on both side of the term is the same variable and having the same value 9 . The wp because it works on a per function basis, has no knowledge of x and a valuation in the function g and because of possible int overflows it cannot prove the assertion.

Using our combined method, we first run value on the whole program, then we bring all relevant variable information into g, which is transformed into the code presented in Figure 9.2. With this additional information, wp gained enough information to prove the assertion.

int g ( int x , int a ) { // @assume a >= 0 && a <= 20; // @assume x >= -1000 && x <= 1000; int res ; if ( x + a >= x ) res = 1; else res = 0; // @assert res == 1; } Listing 9.2: Use case enriched with hypothesis for WP

Experiments & Results

In the experiments the tools mentionned in Section 9.4.4 were used on 12 benchmarks coming from the Siemens test suite (tcas and replace), the Verisec benchmark (get_tag and full_bad from Apache source code) and MediaBench (gd from libgd). We also consider three coverage criteria: CC, MCC and WM [START_REF] Ammann | Introduction to Software Testing[END_REF]. Each of these coverage criteria were encoded with labels as explained in Section 9.4.1. Our overall benchmark consists in 26 pairs program-test requirements. Among the 1,270 test requirements of this benchmark, 121 were shown to be infeasible in a prior manual examination. We solely focus here on the detection efficiency. The impact on test generation (not the focus of this thesis) is detailled in the article [START_REF] Bardin | Sound and Quasi-Complete Detection of Infeasible Test Requirements[END_REF].

Wave-model difference

A throuhghout study of the different self-modification models has been made in 2015 [START_REF] Ugarte-Pedrero | SoK: Deep Packer Inspection: A Longitudinal Study of the Complexity of Run-Time Packers[END_REF]. This annexe aim at emphasizing the difference between Codisasm [START_REF] Bonfante | CoDisasm: Medium Scale Concatic Disassembly of Self-Modifying Binaries with Overlapping Instructions[END_REF] and Pinsec [Dav+16b] differences. Let's consider N the current layer of self-modification. The self-modification detected is performed by tagging memory cells with a given layer number. If that memory cells is later executed the current layer level N will switch to this number if strictly superior than the previous N . The difference between the two models lays in the way to propagate the self-modification aka the marking of memory cells. On an instruction writing in memory Codisasm will use the global current layer counter N while Pinsec will use the value of the instruction itself denoted i n where i is the instruction and n the layer associated to it. In this model all instruction are marked with layer 0 by default. Thus, an instruction is only marked with n + 1 if it is written by an instruction of level n. The figure B.1 shows graphicaly the difference between the two models. Both modeling will update theirs global counter to N = 1 when entering F#1. Meanwhile the execution flow might return the original code and while Pinsec will consider F#2 as another chunk of the layer 1 Codisasm will consider it to be another layer.