barf project
1.0.0
El análisis del código binario es una actividad crucial en muchas áreas de las ciencias de la computadora y las disciplinas de ingeniería de software que van desde la seguridad del software y el análisis de programas hasta la ingeniería inversa. El análisis binario manual es una tarea difícil y que requiere mucho tiempo y hay herramientas de software que buscan automatizar o ayudar a los analistas humanos. Sin embargo, la mayoría de estas herramientas tienen varias restricciones técnicas y comerciales que limitan el acceso y el uso de una gran parte de las comunidades académicas y profesionales. BARF es un marco de análisis binario de código abierto que tiene como objetivo admitir una amplia gama de tareas de análisis de código binario que son comunes en la disciplina de seguridad de la información. Es una plataforma scriptable que admite el levantamiento de instrucciones de múltiples arquitecturas, traducción binaria a una representación intermedia, un marco extensible para complementos de análisis de código e interoperación con herramientas externas como debuggers, solucionadores SMT y herramientas de instrumentación. El marco está diseñado principalmente para el análisis asistido por humanos, pero puede ser completamente automatizado.
El proyecto BARF incluye BARF y herramientas y paquetes relacionados. Hasta ahora, el proyecto está compuesto por los siguientes elementos:
Para más información, consulte:
Estado actual:
| Último lanzamiento | V0.6.0 |
|---|---|
| Url | https://github.com/programa-stic/barf-project/releases/tag/v0.6.0 |
| Registro de cambio | https://github.com/programa-stic/barf-project/blob/v0.6.0/changelog.md |
Todos los paquetes se probaron en Ubuntu 16.04 (x86_64).
BARF es un paquete de Python para análisis binario e ingeniería inversa. Puede:
ELF , PE , etc.),Actualmente está en desarrollo .
BARF depende de los siguientes solucionadores SMT:
El siguiente comando instala BARF en su sistema:
$ sudo python setup.py installTambién puede instalarlo localmente:
$ sudo python setup.py install --usersudo pip install pyasmjitsudo apt-get install graphvizEste es un ejemplo muy simple que muestra cómo abrir un archivo binario e imprimir cada instrucción con su traducción al idioma intermedio ( 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 )) También podemos recuperar el CFG y guardarlo en un archivo .dot .
# Recover CFG.
cfg = barf . recover_cfg ()
# Save CFG to a .dot file.
cfg . save ( "branch4.x86_cfg" )Podemos verificar las restricciones en el código utilizando un solucionador SMT. Por ejemplo, suponga que tiene el siguiente código:
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
Y desea saber qué valores tiene que asignar a las ubicaciones de memoria ebp-0x4 , ebp-0x8 y ebp-0xc para obtener un valor específico en el registro eax después de ejecutar el código.
Primero, agregamos las instrucciones al componente del analizador.
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 )Luego, generamos expresiones para cada variable de interés y agregamos las restricciones deseadas sobre ellas.
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 )Finalmente, verificamos las restricciones que establecemos se pueden resolver.
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!" )Puede ver estos y más ejemplos en el directorio de ejemplos.
El marco se divide en tres componentes principales: núcleo , arco y análisis .
Este componente contiene módulos esenciales:
REIL : proporciona definiciones para el lenguaje Reil. También implementa un emulador y un analizador .SMT : proporciona medios para interactuar con Z3 y CVC4 SMT Solver. Además, proporciona funcionalidad para traducir las instrucciones de Reil a las expresiones SMT.BI : El módulo de interfaz binaria es responsable de cargar archivos binarios para el procesamiento (utiliza PeFile y PyelfTools). Cada arquitectura compatible se proporciona como un subcomponente que contiene los siguientes módulos.
Architecture : describe la arquitectura, es decir, registros, tamaño de la dirección de memoria.Translator : proporciona traductores a Reil para cada instrucción compatible.Disassembler : proporciona funcionalidades desmontables (usa Capstone).Parser : transforma la instrucción de cadena a forma de objeto. Hasta ahora, este componente consta de módulos: gráfico de flujo de control , gráfico de llamadas y analizador de código . Los dos primeros proporcionan funcionalidad para la recuperación de CFG y CG, respectivamente. Este último, es una interfaz de alto nivel para la funcionalidad relacionada con el solucionador SMT.
BARFgadgets es un script de Python basado en BARF que le permite buscar , clasificar y verificar los dispositivos ROP dentro de un programa binario. La etapa de búsqueda encuentra todos los gadgets ret -, jmp y call dentro del binario. La etapa de clasificación clasifica los dispositivos encontrados anteriormente de acuerdo con los siguientes tipos:
Esto se hace a través de la emulación de instrucciones. Finalmente, la etapa de verificación consiste en usar un solucionador SMT para verificar la semántica asignada a cada dispositivo en la segunda etapa.
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.
Para obtener más información, consulte ReadMe.
BARFcfg es un script de Python basado en BARF que le permite recuperar el gráfico de flujo de control de un programa binario.
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 es un script de Python basado en BARF que le permite recuperar el gráfico de llamadas de un programa binario.
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 es un paquete Python para la generación y ejecución de código de ensamblaje X86_64/ARM.
Este paquete se desarrolló para probar la traducción de instrucciones de BARF de x86_64/ARM a Reil. La idea principal es poder ejecutar fragmentos de código de forma nativa. Luego, el mismo fragmento se traduce a Reil y se ejecuta en una VM Reil. Finalmente, ambos contextos finales (uno obtenido a través de la ejecución nativa y la de la emulación) se comparan con las diferencias.
Para obtener más información, ver Pyasmjit.
La licencia de cláusula BSD 2. Para obtener más información, consulte la licencia.
