
BARF : Un framework multiplataforma de código abierto para análisis binario e ingeniería inversa
El análisis de código binario es una actividad crucial en muchas áreas de las ciencias de la computación y disciplinas de ingeniería de software, que abarcan desde la seguridad del software y el análisis de programas hasta la ingeniería inversa. El análisis manual de binarios es una tarea difícil y que consume mucho tiempo, y existen herramientas de software que buscan automatizar o asistir a los analistas humanos. Sin embargo, la mayoría de estas herramientas tienen varias restricciones técnicas y comerciales que limitan el acceso y uso por una gran parte de las comunidades académicas y profesionales. BARF es un framework de análisis binario de código abierto que tiene como objetivo soportar una amplia gama de tareas de análisis de código binario comunes en la disciplina de seguridad informática. Es una plataforma scripteable que soporta la elevación de instrucciones de múltiples arquitecturas, la traducción binaria a una representación intermedia, un framework extensible para plugins de análisis de código y la interoperación con herramientas externas como depuradores, solvers SMT y herramientas de instrumentación. El framework 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:
| Última Versión | v0.6.0 |
|---|---|
| URL | https://github.com/programa-stic/barf-project/releases/tag/v0.6.0 |
| Registro de Cambios | https://github.com/programa-stic/barf-project/blob/v0.6.0/CHANGELOG.md |
Todos los paquetes fueron probados 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 solvers SMT:
El siguiente comando instala BARF en su sistema:
$ sudo python setup.py install
También puede instalarlo localmente:
$ sudo python setup.py install --user
Este es un ejemplo muy simple que muestra cómo abrir un archivo binario e imprimir cada instrucción con su traducción al lenguaje 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 restricciones sobre el código usando un solver 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 debe 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 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 si las restricciones que establecimos pueden ser resueltas.
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 examples.
El framework se divide en tres componentes principales: core, arch y analysis.
Este componente contiene módulos esenciales:
REIL: Proporciona definiciones para el lenguaje REIL. También implementa un emulador y un parser.SMT: Proporciona medios para interactuar con los solvers SMT Z3 y CVC4. También proporciona funcionalidad para traducir instrucciones REIL a expresiones SMT.BI: El módulo Binary Interface se encarga de cargar archivos binarios para su procesamiento (utiliza PEFile y PyELFTools).Cada arquitectura soportada se proporciona como un subcomponente que contiene los siguientes módulos.
Architecture: Describe la arquitectura, es decir, registros, tamaño de dirección de memoria.Translator: Proporciona traductores a REIL para cada instrucción soportada.Disassembler: Proporciona funcionalidades de desensamblado (utiliza Capstone).Parser: Transforma las instrucciones de formato texto a objeto.Hasta ahora, este componente consiste en los módulos: Control-Flow Graph, Call Graph y Code Analyzer. Los dos primeros proporcionan funcionalidad para la recuperación de CFG y CG, respectivamente. El último es una interfaz de alto nivel para la funcionalidad relacionada con el solver SMT.
BARFgadgets es un script de Python construido sobre BARF que permite buscar, clasificar y verificar gadgets ROP dentro de un programa binario. La etapa de búsqueda encuentra todos los gadgets que terminan en ret, jmp y call dentro del binario. La etapa de clasificación clasifica los gadgets encontrados anteriormente según los siguientes tipos:
Esto se realiza mediante emulación de instrucciones. Finalmente, la etapa de verificación consiste en usar un solver SMT para verificar la semántica asignada a cada gadget 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 más información, consulte README.
BARFcfg es un script de Python construido sobre BARF que permite recuperar el grafo 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 construido sobre BARF que permite recuperar el grafo 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 de Python para generación y ejecución de código ensamblador x86_64/ARM.
Este paquete fue desarrollado para probar la traducción de instrucciones 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 máquina virtual REIL. Finalmente, se comparan ambos contextos finales (el obtenido mediante ejecución nativa y el de emulación) para detectar diferencias.
Para más información, consulte PyAsmJIT.
Licencia BSD de 2 cláusulas. Para más información, consulte LICENSE.