BARF : Framework de 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:

• BARF : Um framework multiplataforma open source de Análise Binária e Engenharia Reversa
• PyAsmJIT : Um JIT para as arquiteturas Intel x86_64 e ARM.
• Ferramentas construídas sobre o BARF:
  • BARFgadgets : Permite pesquisar, classificar e verificar gadgets ROP dentro de um programa binário.
  • BARFcfg : Permite recuperar o grafo de fluxo de controle das funções de um programa binário.
  • BARFcg : Permite recuperar o grafo de chamadas das funções de um programa binário.

Para mais informações, veja:

• BARF: Um framework multiplataforma open source de Análise Binária e Engenharia Reversa (Whitepaper) [en]
• BARFing Gadgets (apresentação ekoparty2014) [es]

Status atual:

Todos os pacotes foram testados no Ubuntu 16.04 (x86_64).

BARF

BARF é um pacote Python para análise binária e engenharia reversa. Ele pode:

• Carregar programas binários em diferentes formatos (ELF, PE, etc),
• Suporta a arquitetura Intel x86 para 32 e 64 bits,
• Suporta a arquitetura ARM para 32 bits,
• Opera em uma linguagem intermediária (REIL), portanto todos os algoritmos de análise são independentes de arquitetura,
• Possui integração com solvers SMT Z3 e CVC4, o que significa que você pode expressar fragmentos de código como fórmulas e verificar restrições sobre eles.

Atualmente está em desenvolvimento.

Instalação

BARF depende dos seguintes solvers SMT:

• Z3 : Um provador de teoremas de alto desempenho desenvolvido na Microsoft Research.
• CVC4 : Um provador de teoremas automático open source eficiente para problemas de satisfatibilidade modulo teorias (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

Notas

• Apenas um solver SMT é necessário para funcionar. Você pode escolher entre Z3 e CVC4 ou instalar ambos.
• Para executar alguns testes, você precisa instalar o PyAsmJIT primeiro: sudo pip install pyasmjit
• Você pode precisar instalar o Graphviz: sudo apt-get install graphviz

Início Rápido

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.

Visão Geral

O framework é dividido em três componentes principais: core, arch e analysis.

Core

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.)

Arch

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.

Análise

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.

Ferramentas

BARFgadgets

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:

• No-Operation,
• Move Registrador,
• Carregar Constante,
• Operação Aritmética/Lógica,
• Carregar Memória,
• Armazenar Memória,
• Carregamento Aritmético/Lógico,
• Armazenamento Aritmético/Lógico e
• Indefinido.

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

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

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

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.

Licença

A Licença BSD 2-Clause. Para mais informações, veja LICENSE.