barf project
1.0.0
L'analyse du code binaire est une activité cruciale dans de nombreux domaines des sciences informatiques et des disciplines d'ingénierie logicielle allant de la sécurité des logiciels et de l'analyse du programme à l'ingénierie inverse. L'analyse binaire manuelle est une tâche difficile et longue et il existe des outils logiciels qui cherchent à automatiser ou à aider les analystes humains. Cependant, la plupart de ces outils ont plusieurs restrictions techniques et commerciales qui limitent l'accès et l'utilisation par une grande partie des communautés universitaires et praticiennes. Barf est un cadre d'analyse binaire open source qui vise à soutenir un large éventail de tâches d'analyse de code binaire qui sont courantes dans la discipline de la sécurité de l'information. Il s'agit d'une plate-forme scriptable qui prend en charge la levée des instructions de plusieurs architectures, la traduction binaire par une représentation intermédiaire, un cadre extensible pour les plugins d'analyse de code et l'interopération avec des outils externes tels que les débogueurs, les solveurs SMT et les outils d'instrumentation. Le cadre est conçu principalement pour l'analyse assistée par l'homme, mais il peut être entièrement automatisé.
Le projet BARF comprend BARF et les outils et packages connexes. Jusqu'à présent, le projet est composé des éléments suivants:
Pour plus d'informations, voir:
État actuel:
| Dernière version | v0.6.0 |
|---|---|
| URL | https://github.com/programa-sttic/barf-project/releases/tag/v0.6.0 |
| Modifier le journal | https://github.com/programa-sttic/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 l'ingénierie inverse. Ça peut:
ELF , PE , etc.),Il est actuellement en cours de développement .
Barf dépend des solveurs SMT suivants:
La commande suivante installe la barf sur votre système:
$ sudo python setup.py installVous pouvez également l'installer localement:
$ sudo python setup.py install --usersudo pip install pyasmjitsudo apt-get install graphvizCeci est un exemple très simple qui montre comment ouvrir un fichier binaire et imprimer chaque instruction avec sa traduction dans la langue intermédiaire ( reil ).
from barf import BARF
# Open binary file.
barf = BARF ( "examples/misc/samples/bin/branch4.x86" )
# Print assembly instruction.
for addr , asm_instr , reil_instrs in barf . translate ():
print ( "{:#x} {}" . format ( addr , asm_instr ))
# Print REIL translation.
for reil_instr in reil_instrs :
print ( " t {}" . format ( reil_instr )) Nous pouvons également récupérer le CFG et l'enregistrer dans un fichier .dot .
# Recover CFG.
cfg = barf . recover_cfg ()
# Save CFG to a .dot file.
cfg . save ( "branch4.x86_cfg" )Nous pouvons vérifier les restrictions 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 vous devez attribuer aux emplacements de 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.
Tout d'abord, nous ajoutons les instructions au composant Analyzer.
from barf import BARF
# Open ELF file
barf = BARF ( "examples/misc/samples/bin/constraint1.x86" )
# Add instructions to analyze.
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 y ajoutons les restrictions souhaitées.
ebp = barf . code_analyzer . get_register_expr ( "ebp" , mode = "post" )
# Preconditions: set range for variable a and 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: set desired value for the result
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 que les restrictions que nous établissons peuvent être résolues.
if barf . code_analyzer . check () == 'sat' :
print ( "[+] Satisfiable! Possible assignments:" )
# Get concrete value for 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 )
# Print values
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 ( "[-] Unsatisfiable!" )Vous pouvez voir ces exemples et plus dans le répertoire des exemples.
Le cadre est divisé en trois composants principaux: le noyau , l'arc et l'analyse .
Ce composant contient des modules essentiels:
REIL : fournit des définitions pour la langue Reil. Il implémente également un émulateur et un analyseur .SMT : fournit des moyens d'interfacer avec le solveur SMT Z3 et CVC4. En outre, il fournit des fonctionnalités pour traduire les instructions REIL dans les expressions SMT.BI : Le module d'interface binaire est responsable du chargement des fichiers binaires pour le traitement (il utilise Pefile et Pyelftools.) Chaque architecture prise en charge est fournie comme un sous-composant qui contient les modules suivants.
Architecture : décrit l'architecture, c'est-à-dire les registres, la taille de l'adresse mémoire.Translator : fournit des traducteurs à Reil pour chaque instruction prise en charge.Disassembler : fournit des fonctionnalités de désassemblage (il utilise la pierre angulaire.)Parser : transforme l'instruction de la chaîne en forme d'objet. Jusqu'à présent, ce composant se compose de modules: graphique de contrôle de contrôle , graphique d'appel et analyseur de code . Les deux premiers fournissent respectivement des fonctionnalités pour la récupération CFG et CG. Ce dernier, c'est une interface de haut niveau avec la fonctionnalité liée au solveur SMT.
BARFgadgets est un script Python construit sur Barf qui vous permet de rechercher , de classifier et de vérifier les gadgets ROP dans un programme binaire. L'étape de recherche trouve tous les gadgets ret -, jmp - et call à l'intérieur du binaire. L'étape de classification classe précédemment les gadgets trouvés selon les types suivants:
Cela se fait par émulation d'instructions. Enfin, l'étape de vérification consiste à utiliser un solveur SMT pour vérifier le sémantique attribué à chaque gadget dans 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
Tool for finding, classifying and verifying ROP gadgets.
positional arguments:
filename Binary file name.
optional arguments:
-h, --help show this help message and exit
--version Display version.
--bdepth BDEPTH Gadget depth in number of bytes.
--idepth IDEPTH Gadget depth in number of instructions.
-u, --unique Remove duplicate gadgets (in all steps).
-c, --classify Run gadgets classification.
-v, --verify Run gadgets verification (includes classification).
-o OUTPUT, --output OUTPUT
Save output to file.
-t, --time Print time of each processing step.
--sort {addr,depth} Sort gadgets by address or depth (number of
instructions) in ascending order.
--color Format gadgets with ANSI color sequences, for output
in a 256-color terminal or console.
--show-binary Show binary code for each gadget.
--show-classification
Show classification for each gadget.
--show-invalid Show invalid gadget, i.e., gadgets that were
classified but did not pass the verification process.
--summary SUMMARY Save summary to file.
-r {8,16,32,64} Filter verified gadgets by operands register size.
Pour plus d'informations, voir Readme.
BARFcfg est un script Python construit sur Barf qui vous permet de récupérer le graphique de contrôle 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
Tool for recovering CFG of a binary.
positional arguments:
filename Binary file name.
optional arguments:
-h, --help show this help message and exit
-s SYMBOL_FILE, --symbol-file SYMBOL_FILE
Load symbols from file.
-f {txt,pdf,png,dot}, --format {txt,pdf,png,dot}
Output format.
-t, --time Print process time.
-d OUTPUT_DIR, --output-dir OUTPUT_DIR
Output directory.
-b, --brief Brief output.
--show-reil Show REIL translation.
--immediate-format {hex,dec}
Output format.
-a, --recover-all Recover all functions.
-r RECOVER, --recover RECOVER
Recover specified functions by address (comma
separated).
BARFcg est un script Python construit sur Barf qui vous permet de récupérer le graphique d'appel d'un programme binaire.
usage: BARFcg [-h] [-s SYMBOL_FILE] [-f {pdf,png,dot}] [-t] [-a | -r RECOVER]
filename
Tool for recovering CG of a binary.
positional arguments:
filename Binary file name.
optional arguments:
-h, --help show this help message and exit
-s SYMBOL_FILE, --symbol-file SYMBOL_FILE
Load symbols from file.
-f {pdf,png,dot}, --format {pdf,png,dot}
Output format.
-t, --time Print process time.
-a, --recover-all Recover all functions.
-r RECOVER, --recover RECOVER
Recover specified functions by address (comma
separated).
PyasmJit est un package Python pour la génération et l'exécution de code d'assemblage x86_64 / ARM.
Ce package a été développé afin de tester la traduction d'instructions BARF de x86_64 / ARM à 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 l'exécution native et celui de l'émulation) sont comparés pour les différences.
Pour plus d'informations, voir Pyasmjit.
La licence BSD 2 clause. Pour plus d'informations, voir la licence.
