
BARF : 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
sudo pip install pyasmjitsudo apt-get install graphvizEste é 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: