programa-stic/barf-projectBARF : Un framework open source multiplateforme 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 :
Pour plus d'informations, voir :
Statut actuel :
| Dernière version | v0.6.0 |
|---|---|
| URL | https://github.com/programa-stic/barf-project/releases/tag/v0.6.0 |
| Journal des modifications | https://github.com/programa-stic/barf-project/blob/v0.6.0/CHANGELOG.md |
Tous les packages ont été testés sur Ubuntu 16.04 (x86_64).
BARF est un package Python pour l'analyse binaire et la rétro-ingénierie. Il peut :
ELF, PE, etc.),Il est actuellement en cours de développement.
BARF dépend des solveurs SMT suivants :
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
sudo pip install pyasmjitsudo apt-get install graphvizVoici 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 !")