programa-stic/barf-projectBARF : Um framework multiplataforma de código aberto para Análise Binária e Engenharia Reversa
A análise de código binário é uma atividade crucial em muitas áreas das ciências da computação e disciplinas de engenharia de software, desde segurança de software e análise de programas até engenharia reversa. A análise binária manual é uma tarefa difícil e demorada e existem ferramentas de software que buscam automatizar ou auxiliar analistas humanos. No entanto, a maioria dessas ferramentas possui diversas restrições técnicas e comerciais que limitam o acesso e uso por uma grande parte das comunidades acadêmica e profissional. BARF é um framework de análise binária open source que visa suportar uma ampla gama de tarefas de análise de código binário comuns na disciplina de segurança da informação. É uma plataforma scriptável que suporta elevação de instruções de múltiplas arquiteturas, tradução binária para uma representação intermediária, um framework extensível para plugins de análise de código e interoperabilidade com ferramentas externas como depuradores, solvers SMT e ferramentas de instrumentação. O framework é projetado principalmente para análise assistida por humanos, mas pode ser totalmente automatizado.
O projeto BARF inclui BARF e ferramentas e pacotes relacionados. Até agora, o projeto é composto pelos seguintes itens:
Para mais informações, veja:
Status atual:
| Último Lançamento | v0.6.0 |
|---|---|
| URL | https://github.com/programa-stic/barf-project/releases/tag/v0.6.0 |
| Registro de Mudanças | https://github.com/programa-stic/barf-project/blob/v0.6.0/CHANGELOG.md |
Todos os pacotes foram testados no Ubuntu 16.04 (x86_64).
BARF é um pacote Python para análise binária e engenharia reversa. Ele pode:
ELF, PE, etc),Atualmente está em desenvolvimento.
BARF depende dos seguintes solvers SMT:
O seguinte comando instala o BARF no seu sistema:
$ sudo python setup.py install
Você também pode instalá-lo localmente:
$ sudo python setup.py install --user
Este é um exemplo muito simples que mostra como abrir um arquivo binário e imprimir cada instrução com sua tradução para a linguagem intermediária (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))
Também podemos recuperar o CFG e salvá-lo em um arquivo .dot.
# Recover CFG.
cfg = barf.recover_cfg()
# Save CFG to a .dot file.
cfg.save("branch4.x86_cfg")
Podemos verificar restrições no código usando um solver SMT. Por exemplo, suponha que você tenha o seguinte 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
E você quer saber quais valores precisa atribuir aos locais de memória ebp-0x4, ebp-0x8 e ebp-0xc para obter um valor específico no registrador eax após executar o código.
Primeiro, adicionamos as instruções ao componente analisador.
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)
Então, geramos expressões para cada variável de interesse e adicionamos as restrições desejadas sobre elas.
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 se as restrições que estabelecemos podem ser resolvidas.
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!")
Você pode ver estes e mais exemplos no diretório examples.
O framework é dividido em três componentes principais: core, arch e analysis.
Este componente contém módulos essenciais:
REIL: Fornece definições para a linguagem REIL. Também implementa um emulador e um parser.SMT: Fornece meios para interfacear com solvers SMT Z3 e CVC4. Além disso, fornece funcionalidade para traduzir instruções REIL para expressões SMT.BI: O módulo Binary Interface é responsável por carregar arquivos binários para processamento (usa PEFile e PyELFTools.)Cada arquitetura suportada é fornecida como um subcomponente que contém os seguintes módulos.
Architecture: Descreve a arquitetura, ou seja, registradores, tamanho do endereço de memória.Translator: Fornece tradutores para REIL para cada instrução suportada.Disassembler: Fornece funcionalidades de desmontagem (usa Capstone.)Parser: Transforma instrução de string para forma de objeto.Até agora, este componente consiste nos módulos: Control-Flow Graph, Call Graph e Code Analyzer. Os dois primeiros fornecem funcionalidade para recuperação de CFG e CG, respectivamente. O último é uma interface de alto nível para a funcionalidade relacionada ao solver SMT.
BARFgadgets é um script Python construído sobre o BARF que permite pesquisar, classificar e verificar gadgets ROP dentro de um programa binário. O estágio de pesquisa encontra todos os gadgets terminados em ret, jmp e call dentro do binário. O estágio de classificação classifica os gadgets encontrados anteriormente de acordo com os seguintes tipos:
Isso é feito através de emulação de instruções. Finalmente, o estágio de verificação consiste em usar um solver SMT para verificar a semântica atribuída a cada gadget no segundo estágio.
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 mais informações, veja README.
BARFcfg é um script Python construído sobre o BARF que permite recuperar o grafo de fluxo de controle de um programa binário.
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 é um script Python construído sobre o BARF que permite recuperar o grafo de chamadas de um programa binário.
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 é um pacote Python para geração e execução de código assembly x86_64/ARM. Este pacote foi desenvolvido para testar a tradução de instruções do BARF de x86_64/ARM para REIL. A ideia principal é ser capaz de executar fragmentos de código nativamente. Em seguida, o mesmo fragmento é traduzido para REIL e executado em uma VM REIL. Finalmente, ambos os contextos finais (o obtido através da execução nativa e o da emulação) são comparados em busca de diferenças.
Para mais informações, veja PyAsmJIT.
A Licença BSD 2-Clause. Para mais informações, veja LICENSE.