SecurityInsider
Le blog des experts sécurité Wavestone

L’exécution symbolique avec le framework angr


1. L’analyse de binaire, une problématique courante lors de tests d’intrusion et de réponse à incident
Lors de l’analyse statique d’un binaire exécutable, une des premières étapes est généralement la reconstruction du graphe de flot de contrôle (ou CFG pour control flow graph). Cette structure représente le code exécuté sous la forme d’un graphe dont les nœuds représentent les blocs d’instructions exécutées et dont les liens symbolisent les branchements possibles.

Dans le cadre d’une analyse de malware, il est parfois possible d’identifier certains blocs de code comme étant malveillants, par la présence d’appel à des fonctions rarement présentes dans des exécutables légitimes par exemple. Cependant, si le travail de l’analyste est de découvrir quelles sont les actions qui sont réalisées par un malware, il doit également pouvoir identifier les conditions nécessaires à leur exécution.


Un exemple de graphe de flot de contrôle (CFG)

Dans la figure précédente, on remarque que pour que l’action « executeMalware() » soit exécutée, le chemin d’exécution doit successivement valider les conditions « getWindowsVersion() > 6 » et « getDayOfTheWeek() == 3 ».
Cependant, lors de l’analyse d’un binaire, la taille du CFG est généralement plus conséquente et les instructions analysées sont écrites dans un langage très bas-niveau, rendant ainsi les conditions beaucoup plus compliquées à interpréter.


2. Concepts et principes de l’exécution symbolique 
Afin de pouvoir simplifier une telle analyse, et d’être capable d’évaluer de manière automatisée les exécutions possibles d’un binaire, il existe une méthode formelle appelée l’exécution symbolique.
Contrairement à l’exécution classique (ou concrète) d’un programme, où chaque registre du processeur et chaque case mémoire contient une valeur déterminée à chaque instant, l’exécution symbolique consiste à exécuter un programme de manière « abstraite », en remplaçant les valeurs inconnues par des « symboles ».
Considérons par exemple le pseudocode suivant, et le graphe de flot de contrôle associé :
Un programme et son CFG associé

Si la fonction input() symbolise une entrée de l’utilisateur, celle-ci n’a donc pas une valeur connue avant l’exécution du programme. Lors d’une exécution symbolique, les valeurs renvoyées par cette fonction seront donc remplacées par des « symboles ».
À chaque branchement conditionnel rencontré, l’algorithme d’exécution symbolique emprunte les deux chemins possibles, et enregistre les contraintes correspondant à chacune des conditions. Le graphe suivant représente le résultat d’une exécution symbolique du programme précédent, définissant les symboles x0 et y0 comme les valeurs initiales de x et y. Les expressions entre accolades représentent les contraintes correspondant à chaque chemin.
Résultat d’une exécution symbolique du programme précédent

Une fois l’exécution symbolique réalisée, il est possible de déterminer que la condition nécessaire pour atteindre le nœud « win() » est {x==x0, y==y0, x0-y0==100, y0==2*x0}. Cet ensemble de contraintes peut être simplifiée automatiquement en {x==x0, y==y0, x0== -100, y0== -200}.
Grâce à l’exécution symbolique, il a donc été possible de déterminer de manière automatisée les conditions permettant d’atteindre un certain état du programme.

3. Le framework angr
Le framework Python angr (http://angr.io) permet d’appliquer facilement les concepts de l’exécution symbolique à un binaire exécutable. Afin d’illustrer son utilisation, nous allons résoudre un challenge de la Nuit du Hack 2016  : un crackme nommé « lol_so_obfuscated ».


Exécution du binaire

Il s’agit programme qui accepte en argument une chaine de caractère, et affiche une série de nombres suivi d’un message, « You’re wrong » dans l’exemple.
Une rapide analyse du CFG de la fonction main du binaire indique que :
  1.  Une fonction nommée « encrypt » est appelée, avec comme paramètres une chaine de caractères inscrite en dur dans le binaire et l’argument fourni par l’utilisateur ;
  2.  Le résultat de cette fonction est comparé avec une autre chaine de caractères inscrite en dur dans la pile d’exécution
  3.  Si les chaines correspondent, le programme affiche « You’re right » 
  4.  Sinon, le programme affiche « You’re wrong ».



Extrait du CFG de la fonction main, avec l’outil radare2

Le but du challenge est donc de trouver une entrée utilisateur qui permette au programme d’exécuter le code situé à l’adresse « 0x400745 » (3), c’est-à-dire qui fasse afficher le message « You’re right ».
L’exécution symbolique est parfaitement adaptée pour répondre à ce type de problématique. Notamment, le framework angr permet de résoudre relativement simplement ce challenge en exécutant le code suivant (toutes les étapes ont été commentées) :

L’exécution du code permet de calculer la solution du challenge sans aucune interaction supplémentaire :


On remarquera que seules les adresses des blocs « You’re right » et « You’re wrong » challenge (en rouge dans le code), obtenues par simple observation du CFG du programme, ont été nécessaires afin de résoudre le challenge. Aucune étape de reverse-engineering n’a été effectuée ; notamment les opérations réalisées par la fonction encrypt n’ont fait l’objet d’aucune étude.

4. En conclusion
L’exécution symbolique est un outil puissant pouvant grandement simplifier l’analyse de code. Outre la recherche de conditions permettant d’atteindre un certain état, il permet également de pouvoir détecter certains types de vulnérabilités comme des dépassements de tampon (« buffer overflow »), ou même de prouver leur absence de manière formelle.

Un des principaux atouts du framework angr est sa facilité de prise en main, celui-ci ayant une API plutôt intuitive (une fois les concepts de base de l’exécution symbolique maitrisée). Il dispose également d’une documentation (https://docs.angr.io/) permettant de s’approprier facilement l’outil, et d’une liste grandissante d’exemples de challenges de CTF résolus avec angr (https://github.com/angr/angr-doc/tree/master/examples).

De nombreux outils permettant l’exécution symbolique existent également, parmi lesquels :
·         Miasm (https://github.com/cea-sec/miasm), un framework très complet de reverse-engineering développé par le CEA, qui permet l’exécution symbolique, mais aussi l’édition de binaire exécutable, l’émulation de code, la traduction dans un langage intermédiaire permettant la simplification du code, l’intégration dans l’outil IDA, etc. Néanmoins, ce framework pèche par l’absence d’une documentation permettant de prendre rapidement l’outil en main :)
·         KLEE (http://klee.github.io), un moteur d’exécution symbolique basé sur LLVM, qui s’utilise donc avant compilation via l’ajout de code dans les fichiers source du programme testé. Ce type d’outil est notamment utile lors des développements d’un logiciel afin de vérifier l’absence de certaines vulnérabilités. 



Maxime MEIGNAN







Aucun commentaire:

Enregistrer un commentaire