BARF : Framework d'analyse binaire et de rétro-ingénierie

L'analyse de code binaire est une activité cruciale dans de nombreux domaines des sciences informatiques et du génie logiciel, allant de la sécurité logicielle et de l'analyse de programmes à la rétro-ingénierie. L'analyse binaire manuelle est une tâche difficile et chronophage, et il existe des outils logiciels qui cherchent à automatiser ou à assister les analystes humains. Cependant, la plupart de ces outils présentent plusieurs restrictions techniques et commerciales qui limitent l'accès et l'utilisation par une grande partie des communautés académiques et professionnelles. BARF est un framework open source d'analyse binaire qui vise à prendre en charge un large éventail de tâches d'analyse de code binaire courantes dans la discipline de la sécurité informatique. Il s'agit d'une plateforme scriptable qui prend en charge l'élévation d'instructions depuis plusieurs architectures, la traduction binaire vers une représentation intermédiaire, un framework extensible pour les plugins d'analyse de code et l'interopérabilité avec des outils externes tels que les débogueurs, les solveurs SMT et les outils d'instrumentation. Le framework est conçu principalement pour l'analyse assistée par un humain mais peut être entièrement automatisé.

Le projet BARF comprend BARF et les outils et packages associés. Jusqu'à présent, le projet se compose des éléments suivants :

• BARF : Un framework open source multiplateforme d'analyse binaire et de rétro-ingénierie
• PyAsmJIT : Un JIT pour les architectures Intel x86_64 et ARM.
• Outils construits sur BARF :
  • BARFgadgets : Permet de rechercher, classifier et vérifier les gadgets ROP dans un programme binaire.
  • BARFcfg : Permet de reconstruire le graphe de flot de contrôle des fonctions d'un programme binaire.
  • BARFcg : Permet de reconstruire le graphe d'appel des fonctions d'un programme binaire.

Pour plus d'informations, voir :

• BARF: A multiplatform open source Binary Analysis and Reverse engineering Framework (Livre blanc) [en]
• BARFing Gadgets (présentation ekoparty2014) [es]

Statut actuel :

Tous les packages ont été testés sur Ubuntu 16.04 (x86_64).

BARF

BARF est un package Python pour l'analyse binaire et la rétro-ingénierie. Il peut :

• Charger des programmes binaires dans différents formats (ELF, PE, etc.),
• Prend en charge l'architecture Intel x86 pour 32 et 64 bits,
• Prend en charge l'architecture ARM pour 32 bits,
• Fonctionner sur un langage intermédiaire (REIL) rendant ainsi tous les algorithmes d'analyse indépendants de l'architecture,
• S'intégrer avec les solveurs SMT Z3 et CVC4, ce qui permet d'exprimer des fragments de code sous forme de formules et de vérifier des contraintes sur ceux-ci.

Il est actuellement en cours de développement.

Installation

BARF dépend des solveurs SMT suivants :

• Z3 : Un prouveur de théorèmes haute performance développé à Microsoft Research.
• CVC4 : Un prouveur de théorèmes automatique open source efficace pour les problèmes de satisfiabilité modulo théories (SMT).

La commande suivante installe BARF sur votre système :

$ sudo python setup.py install

Vous pouvez également l'installer localement :

$ sudo python setup.py install --user

Remarques

• Un seul solveur SMT est nécessaire pour fonctionner. Vous pouvez choisir entre Z3 et CVC4, ou installer les deux.
• Pour exécuter certains tests, vous devez d'abord installer PyAsmJIT : sudo pip install pyasmjit
• Vous pourriez avoir besoin d'installer Graphviz : sudo apt-get install graphviz

Démarrage rapide

Voici un exemple très simple qui montre comment ouvrir un fichier binaire et afficher chaque instruction avec sa traduction dans le langage intermédiaire (REIL).

from barf import BARF

# Ouvrir le fichier binaire.
barf = BARF("examples/misc/samples/bin/branch4.x86")

# Afficher l'instruction assembleur.
for addr, asm_instr, reil_instrs in barf.translate():
    print("{:#x} {}".format(addr, asm_instr))

    # Afficher la traduction REIL.
    for reil_instr in reil_instrs:
        print("\t{}".format(reil_instr))

Nous pouvons également reconstruire le CFG et le sauvegarder dans un fichier .dot.

# Reconstruire le CFG.
cfg = barf.recover_cfg()

# Sauvegarder le CFG dans un fichier .dot.
cfg.save("branch4.x86_cfg")

Nous pouvons vérifier les contraintes sur le code à l'aide d'un solveur SMT. Par exemple, supposons que vous ayez le code suivant :

 80483ed:       55                      push   ebp
 80483ee:       89 e5                   mov    ebp,esp
 80483f0:       83 ec 10                sub    esp,0x10
 80483f3:       8b 45 f8                mov    eax,DWORD PTR [ebp-0x8]
 80483f6:       8b 55 f4                mov    edx,DWORD PTR [ebp-0xc]
 80483f9:       01 d0                   add    eax,edx
 80483fb:       83 c0 05                add    eax,0x5
 80483fe:       89 45 fc                mov    DWORD PTR [ebp-0x4],eax
 8048401:       8b 45 fc                mov    eax,DWORD PTR [ebp-0x4]
 8048404:       c9                      leave
 8048405:       c3                      ret

Et vous voulez savoir quelles valeurs assigner aux emplacements mémoire ebp-0x4, ebp-0x8 et ebp-0xc afin d'obtenir une valeur spécifique dans le registre eax après l'exécution du code.

D'abord, nous ajoutons les instructions au composant analyseur.

from barf import BARF

# Ouvrir le fichier ELF
barf = BARF("examples/misc/samples/bin/constraint1.x86")

# Ajouter les instructions à analyser.
for addr, asm_instr, reil_instrs in barf.translate(0x80483ed, 0x8048401):
    for reil_instr in reil_instrs:
        barf.code_analyzer.add_instruction(reil_instr)

Ensuite, nous générons des expressions pour chaque variable d'intérêt et ajoutons les restrictions souhaitées sur celles-ci.

ebp = barf.code_analyzer.get_register_expr("ebp", mode="post")

# Préconditions : définir la plage pour les variables a et b
a = barf.code_analyzer.get_memory_expr(ebp-0x8, 4, mode="pre")
b = barf.code_analyzer.get_memory_expr(ebp-0xc, 4, mode="pre")

for constr in [a >= 2, a <= 100, b >= 2, b <= 100]:
    barf.code_analyzer.add_constraint(constr)

# Postconditions : définir la valeur souhaitée pour le résultat
c = barf.code_analyzer.get_memory_expr(ebp-0x4, 4, mode="post")

for constr in [c >= 26, c <= 28]:
    barf.code_analyzer.add_constraint(constr)

Enfin, nous vérifions si les restrictions que nous avons établies peuvent être résolues.

if barf.code_analyzer.check() == 'sat':
    print("[+] Satisfiable ! Assignations possibles :")

    # Obtenir la valeur concrète des expressions
    a_val = barf.code_analyzer.get_expr_value(a)
    b_val = barf.code_analyzer.get_expr_value(b)
    c_val = barf.code_analyzer.get_expr_value(c)

    # Afficher les valeurs
    print("- a : {0:#010x} ({0})".format(a_val))
    print("- b : {0:#010x} ({0})".format(b_val))
    print("- c : {0:#010x} ({0})".format(c_val))

    assert a_val + b_val + 5 == c_val
else:
    print("[-] Insatisfiable !")

Vous pouvez consulter ces exemples et d'autres dans le répertoire examples.

Vue d'ensemble

Le framework est divisé en trois composants principaux : core, arch et analysis.

Core

Ce composant contient les modules essentiels :

• REIL : Fournit les définitions du langage REIL. Il implémente également un émulateur et un analyseur syntaxique.
• SMT : Fournit les moyens d'interfacer les solveurs SMT Z3 et CVC4. Il fournit également des fonctionnalités pour traduire les instructions REIL en expressions SMT.
• BI : Le module Binary Interface est responsable du chargement des fichiers binaires pour le traitement (il utilise PEFile et PyELFTools).

Arch

Chaque architecture prise en charge est fournie en tant que sous-composant contenant les modules suivants :

• Architecture : Décrit l'architecture, c'est-à-dire les registres, la taille des adresses mémoire.
• Translator : Fournit des traducteurs vers REIL pour chaque instruction prise en charge.
• Disassembler : Fournit des fonctionnalités de désassemblage (il utilise Capstone).
• Parser : Transforme les instructions de la chaîne de caractères en forme objet.

Analysis

Jusqu'à présent, ce composant comprend les modules : Control-Flow Graph, Call Graph et Code Analyzer. Les deux premiers fournissent respectivement des fonctionnalités de reconstruction du CFG et du CG. Le dernier est une interface de haut niveau vers les fonctionnalités liées au solveur SMT.

Outils

BARFgadgets

BARFgadgets est un script Python construit sur BARF qui vous permet de rechercher, classifier et vérifier les gadgets ROP dans un programme binaire. L'étape de recherche trouve tous les gadgets se terminant par ret, jmp et call dans le binaire. L'étape de classification classe les gadgets trouvés précédemment selon les types suivants :

• No-Operation,
• Move Register,
• Load Constant,
• Arithmetic/Logical Operation,
• Load Memory,
• Store Memory,
• Arithmetic/Logical Load,
• Arithmetic/Logical Store et
• Undefined.

Ceci est réalisé par émulation d'instructions. Enfin, l'étape de vérification consiste à utiliser un solveur SMT pour vérifier la sémantique attribuée à chaque gadget lors de la deuxième étape.

usage: BARFgadgets [-h] [--version] [--bdepth BDEPTH] [--idepth IDEPTH] [-u]
                   [-c] [-v] [-o OUTPUT] [-t] [--sort {addr,depth}] [--color]
                   [--show-binary] [--show-classification] [--show-invalid]
                   [--summary SUMMARY] [-r {8,16,32,64}]
                   filename

Outil de recherche, classification et vérification de gadgets ROP.

arguments positionnels:
  filename              Nom du fichier binaire.

arguments optionnels:
  -h, --help            Affiche ce message d'aide et quitte.
  --version             Affiche la version.
  --bdepth BDEPTH       Profondeur du gadget en nombre d'octets.
  --idepth IDEPTH       Profondeur du gadget en nombre d'instructions.
  -u, --unique          Supprime les gadgets en double (à toutes les étapes).
  -c, --classify        Exécute la classification des gadgets.
  -v, --verify          Exécute la vérification des gadgets (inclut la classification).
  -o OUTPUT, --output OUTPUT
                        Sauvegarde la sortie dans un fichier.
  -t, --time            Affiche le temps de chaque étape de traitement.
  --sort {addr,depth}   Trie les gadgets par adresse ou profondeur (nombre d'instructions) en ordre croissant.
  --color               Formate les gadgets avec des séquences de couleurs ANSI, pour une sortie dans un terminal ou console 256 couleurs.
  --show-binary         Affiche le code binaire pour chaque gadget.
  --show-classification
                        Affiche la classification pour chaque gadget.
  --show-invalid        Affiche les gadgets invalides, c'est-à-dire les gadgets qui ont été classifiés mais n'ont pas passé le processus de vérification.
  --summary SUMMARY     Sauvegarde le résumé dans un fichier.
  -r {8,16,32,64}       Filtre les gadgets vérifiés par la taille du registre des opérandes.

Pour plus d'informations, voir README.

BARFcfg

BARFcfg est un script Python construit sur BARF qui vous permet de reconstruire le graphe de flot de contrôle d'un programme binaire.

usage: BARFcfg [-h] [-s SYMBOL_FILE] [-f {txt,pdf,png,dot}] [-t]
               [-d OUTPUT_DIR] [-b] [--show-reil]
               [--immediate-format {hex,dec}] [-a | -r RECOVER]
               filename

Outil de reconstruction du CFG d'un binaire.

arguments positionnels:
  filename              Nom du fichier binaire.

arguments optionnels:
  -h, --help            Affiche ce message d'aide et quitte.
  -s SYMBOL_FILE, --symbol-file SYMBOL_FILE
                        Charge les symboles depuis un fichier.
  -f {txt,pdf,png,dot}, --format {txt,pdf,png,dot}
                        Format de sortie.
  -t, --time            Affiche le temps de traitement.
  -d OUTPUT_DIR, --output-dir OUTPUT_DIR
                        Répertoire de sortie.
  -b, --brief           Sortie concise.
  --show-reil           Affiche la traduction REIL.
  --immediate-format {hex,dec}
                        Format de sortie.
  -a, --recover-all     Reconstruit toutes les fonctions.
  -r RECOVER, --recover RECOVER
                        Reconstruit les fonctions spécifiées par adresse (séparées par des virgules).

BARFcg

BARFcg est un script Python construit sur BARF qui vous permet de reconstruire le graphe d'appel d'un programme binaire.

usage: BARFcg [-h] [-s SYMBOL_FILE] [-f {pdf,png,dot}] [-t] [-a | -r RECOVER]
              filename

Outil de reconstruction du CG d'un binaire.

arguments positionnels:
  filename              Nom du fichier binaire.

arguments optionnels:
  -h, --help            Affiche ce message d'aide et quitte.
  -s SYMBOL_FILE, --symbol-file SYMBOL_FILE
                        Charge les symboles depuis un fichier.
  -f {pdf,png,dot}, --format {pdf,png,dot}
                        Format de sortie.
  -t, --time            Affiche le temps de traitement.
  -a, --recover-all     Reconstruit toutes les fonctions.
  -r RECOVER, --recover RECOVER
                        Reconstruit les fonctions spécifiées par adresse (séparées par des virgules).

PyAsmJIT

PyAsmJIT est un package Python pour la génération et l'exécution de code assembleur x86_64/ARM.

Ce package a été développé afin de tester la traduction des instructions BARF de x86_64/ARM vers REIL. L'idée principale est de pouvoir exécuter des fragments de code nativement. Ensuite, le même fragment est traduit en REIL et exécuté dans une machine virtuelle REIL. Enfin, les deux contextes finaux (celui obtenu par exécution native et celui de l'émulation) sont comparés pour détecter les différences.

Pour plus d'informations, voir PyAsmJIT.

Licence

La licence BSD 2-Clause. Pour plus d'informations, voir LICENSE.