programa-stic/barf-projectBARF : Un framework open source multipiattaforma per l'Analisi Binaria e il Reverse engineering
L'analisi del codice binario è un'attività cruciale in molte aree dell'informatica e dell'ingegneria del software, che vanno dalla sicurezza del software all'analisi dei programmi fino al reverse engineering. L'analisi binaria manuale è un compito difficile e dispendioso in termini di tempo, e esistono strumenti software che cercano di automatizzare o assistere gli analisti umani. Tuttavia, la maggior parte di questi strumenti presenta diverse restrizioni tecniche e commerciali che ne limitano l'accesso e l'uso da parte di gran parte delle comunità accademiche e professionali. BARF è un framework open source per l'analisi binaria che mira a supportare un'ampia gamma di attività di analisi del codice binario comuni nella disciplina della sicurezza informatica. È una piattaforma scriptabile che supporta il sollevamento delle istruzioni da più architetture, la traduzione binaria in una rappresentazione intermedia, un framework estensibile per plugin di analisi del codice e l'interoperabilità con strumenti esterni come debugger, risolutori SMT e strumenti di strumentazione. Il framework è progettato principalmente per l'analisi assistita dall'uomo ma può essere completamente automatizzato.
Il progetto BARF include BARF e gli strumenti e i pacchetti correlati. Finora il progetto è composto dai seguenti elementi:
Per maggiori informazioni, vedere:
Stato attuale:
Tutti i pacchetti sono stati testati su Ubuntu 16.04 (x86_64).
BARF è un pacchetto Python per l'analisi binaria e il reverse engineering. Può:
ELF, PE, ecc.),È attualmente in fase di sviluppo.
BARF dipende dai seguenti risolutori SMT:
Il seguente comando installa BARF sul sistema:
$ sudo python setup.py install
Puoi anche installarlo localmente:
$ sudo python setup.py install --user
Questo è un esempio molto semplice che mostra come aprire un file binario e stampare ogni istruzione con la sua traduzione nel linguaggio intermedio (REIL).
from barf import BARF
# Apri file binario.
barf = BARF("examples/misc/samples/bin/branch4.x86")
# Stampa istruzioni assembly.
for addr, asm_instr, reil_instrs in barf.translate():
print("{:#x} {}".format(addr, asm_instr))
# Stampa traduzione REIL.
for reil_instr in reil_instrs:
print("\t{}".format(reil_instr))
Possiamo anche recuperare il CFG e salvarlo in un file .dot.
# Recupera CFG.
cfg = barf.recover_cfg()
# Salva CFG in un file .dot.
cfg.save("branch4.x86_cfg")
Possiamo verificare vincoli sul codice utilizzando un risolutore SMT. Ad esempio, supponiamo di avere il seguente codice:
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 si vuole sapere quali valori assegnare alle locazioni di memoria ebp-0x4, ebp-0x8 e ebp-0xc per ottenere un valore specifico nel registro eax dopo l'esecuzione del codice.
Per prima cosa, aggiungiamo le istruzioni al componente analizzatore.
from barf import BARF
# Apri file ELF
barf = BARF("examples/misc/samples/bin/constraint1.x86")
# Aggiungi istruzioni da analizzare.
for addr, asm_instr, reil_instrs in barf.translate(0x80483ed, 0x8048401):
for reil_instr in reil_instrs:
barf.code_analyzer.add_instruction(reil_instr)
Quindi, generiamo espressioni per ogni variabile di interesse e aggiungiamo i vincoli desiderati su di esse.
ebp = barf.code_analyzer.get_register_expr("ebp", mode="post")
# Precondizioni: imposta intervallo per le variabili a e 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)
# Postcondizioni: imposta valore desiderato per il risultato
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)
Infine, verifichiamo se i vincoli stabiliti possono essere risolti.
if barf.code_analyzer.check() == 'sat':
print("[+] Soddisfacibile! Possibili assegnazioni:")
# Ottieni valore concreto per le espressioni
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)
# Stampa valori
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("[-] Insoddisfacibile!")
Puoi vedere questi e altri esempi nella directory examples.
Il framework è suddiviso in tre componenti principali: core, arch e analysis.
Questo componente contiene moduli essenziali:
REIL: Fornisce definizioni per il linguaggio REIL. Implementa anche un emulatore e un parser.SMT: Fornisce mezzi per interfacciarsi con i risolutori SMT Z3 e CVC4. Inoltre, fornisce funzionalità per tradurre istruzioni REIL in espressioni SMT.BI: Il modulo Binary Interface è responsabile del caricamento dei file binari per l'elaborazione (utilizza PEFile e PyELFTools).Ogni architettura supportata è fornita come sottocomponente che contiene i seguenti moduli.
Architecture: Descrive l'architettura, ovvero registri, dimensione dell'indirizzo di memoria.Translator: Fornisce traduttori in REIL per ogni istruzione supportata.Disassembler: Fornisce funzionalità di disassemblaggio (utilizza Capstone).Parser: Trasforma le istruzioni da stringa a forma oggetto.Finora questo componente consiste nei moduli: Control-Flow Graph, Call Graph e Code Analyzer. I primi due forniscono funzionalità rispettivamente per il recupero di CFG e CG. L'ultimo è un'interfaccia di alto livello per le funzionalità relative al risolutore SMT.
BARFgadgets è uno script Python basato su BARF che consente di cercare, classificare e verificare i gadget ROP all'interno di un programma binario. La fase di ricerca trova tutti i gadget che terminano con ret, jmp e call all'interno del binario. La fase di classificazione classifica i gadget trovati in precedenza secondo i seguenti tipi:
Ciò viene fatto tramite emulazione delle istruzioni. Infine, la fase di verifica consiste nell'utilizzare un risolutore SMT per verificare la semantica assegnata a ciascun gadget nella seconda fase.
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.
Per maggiori informazioni, vedere README.
BARFcfg è uno script Python basato su BARF che consente di recuperare il
grafo di flusso di controllo di un programma 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 è uno script Python basato su BARF che consente di recuperare il
grafo delle chiamate di un programma 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 è un pacchetto Python per la generazione e l'esecuzione di codice assembly x86_64/ARM.
Questo pacchetto è stato sviluppato per testare la traduzione delle istruzioni BARF da x86_64/ARM a REIL. L'idea principale è essere in grado di eseguire frammenti di codice in modo nativo. Quindi, lo stesso frammento viene tradotto in REIL ed eseguito in una VM REIL. Infine, entrambi i contesti finali (quello ottenuto tramite esecuzione nativa e quello dell'emulazione) vengono confrontati per rilevare differenze.
Per maggiori informazioni, vedere PyAsmJIT.
La licenza BSD 2-Clause. Per maggiori informazioni, vedere LICENSE.