barf project
1.0.0
A análise do código binário é uma atividade crucial em muitas áreas das ciências da computação e das disciplinas de engenharia de software que variam de segurança de software e análise de programa a engenharia reversa. A análise binária manual é uma tarefa difícil e demorada e existem ferramentas de software que buscam automatizar ou ajudar os analistas humanos. No entanto, a maioria dessas ferramentas possui várias restrições técnicas e comerciais que limitam o acesso e o uso por uma grande parte das comunidades acadêmicas e profissionais. O BARF é uma estrutura de análise binária de código aberto que visa suportar uma ampla gama de tarefas de análise de código binário que são comuns na disciplina de segurança da informação. É uma plataforma que suporta o levantamento de instruções de várias arquiteturas, tradução binária para uma representação intermediária, uma estrutura extensível para plug -ins de análise de código e interoperação com ferramentas externas, como depuradores, solucionadores de SMT e ferramentas de instrumentação. A estrutura foi projetada principalmente para análise assistida pelo homem, mas pode ser totalmente automatizada.
O projeto Barf inclui barf e ferramentas e pacotes relacionados. Até agora, o projeto é composto pelos seguintes itens:
Para mais informações, consulte:
Status atual:
| Última lançamento | v0.6.0 |
|---|---|
| Url | https://github.com/programa-stic/barf-project/releases/tag/v0.6.0 |
| Alterar log | https://github.com/programa-stic/barf-project/blob/v0.6.0/changelog.md |
Todos os pacotes foram testados no Ubuntu 16.04 (x86_64).
O BARF é um pacote Python para análise binária e engenharia reversa. Pode:
ELF , PE , etc),Está atualmente em desenvolvimento .
O BARF depende dos seguintes solucionadores de SMT:
O comando a seguir instala o BARF em seu sistema:
$ sudo python setup.py installVocê também pode instalá -lo localmente:
$ sudo python setup.py install --usersudo 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 as restrições no código usando um solucionador 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ê deseja saber quais valores você deve atribuir aos locais de memória ebp-0x4 , ebp-0x8 e ebp-0xc para obter um valor específico no registro eax após a execução do código.
Primeiro, adicionamos as instruções ao componente do 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 )Em seguida, geramos expressões para cada variável de interesse e adicionamos as restrições desejadas.
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 )Por fim, verificamos que 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 esses e mais exemplos no diretório Exemplos.
A estrutura é dividida em três componentes principais: núcleo , arco e análise .
Este componente contém módulos essenciais:
REIL : fornece definições para a linguagem REIL. Também implementa um emulador e um analisador .SMT : fornece meios para interface com o solucionador Z3 e CVC4 SMT. Além disso, fornece funcionalidade para traduzir instruções de reil para expressões SMT.BI : O módulo de interface binária é responsável pelo carregamento de 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, registros, tamanho do endereço de memória.Translator : fornece tradutores para o REIL para cada instrução suportada.Disassembler : fornece funcionalidades de desmontagem (usa Capstone.)Parser : transforma a instrução de string em forma de objeto. Até agora, esse componente consiste em módulos: gráfico de fluxo de controle , gráfico de chamada e analisador de código . Os dois primeiros fornecem funcionalidade para a recuperação de CFG e CG, respectivamente. Este último, é uma interface de alto nível para a funcionalidade relacionada ao solucionador SMT.
BARFgadgets é um script python construído sobre o BARF que permite pesquisar , classificar e verificar os gadgets de ROP dentro de um programa binário. O estágio de pesquisa encontra todos os gadgets ret -, jmp -e call o interior do binário. O estágio de classificação classifica os gadgets encontrados anteriormente de acordo com os seguintes tipos:
Isso é feito através da emulação de instrução. Finalmente, o estágio de verificação consiste em usar um solucionador 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, consulte ReadMe.
BARFcfg é um script python construído sobre o BARF que permite recuperar o gráfico 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 gráfico 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).
O Pyasmjit é um pacote Python para geração e execução do código de montagem X86_64/ARM.
Este pacote foi desenvolvido para testar a tradução de instruções do BARF de x86_64/braço para reil. A idéia principal é poder 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 a diferenças.
Para mais informações, consulte Pyasmjit.
A licença de cláusula 2 BSD. Para mais informações, consulte a licença.
