Symbolic Execution: un approccio alternativo al bruteforce per il Password cracking
Utilizzeremo angr, un toolkit per l'analisi dei binari, scritto in Python. Angr permette di svolgere l'esecuzione simbolica dinamica dei binari, oltre a varie analisi statiche.
Durante le CTF, molto spesso la soluzione di una particolare challenge richiede la scoperta, o il crack, di una password o comunque di una chiave di accesso. Una delle soluzioni più immediate è il metodo bruteforce (attacco a forza bruta), che consiste nell'inserire tutte le possibili password per cercare di indovinare quella corretta.
Non sempre è possibile effettuare un bruteforce, per varie ragioni (una su tutte, il tempo che impiegherebbe).
Esistono metodologie più raffinate rispetto al bruteforce che si possono utilizzare in queste situazioni, e alcune volte queste risultano anche più efficaci, portando al crack di una password in poco tempo. La tecnica che verrà introdotta in questo articolo è chiamata esecuzione simbolica (Symbolic Execution in inglese).
Utilizzeremo angr, un toolkit per l'analisi dei binari, scritto in Python. Angr permette di svolgere l'esecuzione simbolica dinamica dei binari, oltre a varie analisi statiche.
Che cosa si intende per esecuzione simbolica?
Il concetto fondamentale nell'esecuzione simbolica, è il concetto di variabile simbolica. Una variabile simbolica, invece di contenere un valore completo (Esempio: 5), contiene un simbolo, ovvero semplicemente un etichetta.
Di conseguenza, eseguendo operazioni aritmetiche fra variabili simboliche, il risultato sarà una catena di operazioni, definita come abstract syntax tree o AST, concetto appartenente alla teoria dei compilatori. Questo albero rappresenta il flusso di operazioni eseguito da un programma, per ogni input passato.
Esempio:
x = 3
y = x + 2
print yIn questo programma, se il valore di input della variabile x è uguale a 3 (valore concreto), nella normale esecuzione, il risultato dell'operazione tra x e 2 è uguale 5.
Nell'esecuzione simbolica, il risultato dell' operazione x + 2, è x + 2! Ovvero, la variabile y conterrà l'operazione, non il suo risultato.
Quindi y == (AST)(x + 2)
y non ha un valore concreto, y è un AST.
Installazione di angr
angr è una libreria Python, si installa quindi allo stesso modo delle altre librerie dell'interprete. La documentazione ufficiale consiglia di installare sempre angr in virtualenv, in modo da evitare conflitti con altre librerie del sistema operativo. Inoltre, il supporto per python2 presto terminerà, quindi angr va installato con python3.
Se si possiede un sistema *nix, prima vanno installate le varie dipendenze della libreria con questo comando:
sudo apt-get install python3-dev libffi-dev build-essential virtualenvwrapperPoi installare angr lanciando questo comando:
virtualenv --python=$(which python3) angr && pip3 install angrUna volta terminata l'installazione, avviamo angr in una shell python per verificare che l'istallazione nell'ambiente virtuale sia andata a buon fine:
luca@luca-Lenovo-Y50-70:~$ source angr/bin/activate
(angr) luca@luca-Lenovo-Y50-70:~$ ipython
In [1]: import angr AST e variabili simboliche in angr
Per prima cosa, mostriamo come il concetto di variabile simbolica si traduce in bitvectors in angr.
La prima operazione che bisogna fare è creare un nuovo progetto, per indicare ad angr quale sarà l'eseguibile che prenderemo in analisi:
In [2]: proj = angr.Project('/bin/true')in angr, un progetto ( da qui in avanti indicato come Project o proj ) rappresenta l' immagine iniziale del programma. Quando il programma viene eseguito (simbolicamente) con angr, ad ogni momento dell'esecuzione il programma si trova in uno specifico stato, rappresentato dall'oggetto SimState:
In [3]: state = proj.factory.entry_state()
<SimState @ 0x401670>Lo stato contiene tutte le informazioni su memoria del programma, registri, dati e altro. il valore 0x401670 è l'indirizzo di memoria della prossima istruzione assembly eseguita (I.e il valore di eip/rip)
Il metodo entry_state() ritorna lo stato del programma al suo entry point.
Per accedere a registri e memoria del programma, ci sono le properties dell' oggetto SimState: regs and mem
In [4]: state.regs.rip
<BV64 0x401670>
In [5]: state.regs.rax
<BV64 0x1c>
In [6]: state.mem[proj.entry].int.resolved
<BV32 0x8949ed31>Notiamo come i valori nei registri e quelli nella memoria (ignoriamo per ora le properties .int e .resolved) non siano interi, ma sono infatti bitvectors, di grandezza, in questo caso, 32 0 64 bit.
I bitvector sono semplicemente una sequenza di bit ( in maniera simile agli interi in C ) e possono essere creati con lunghezza variabile. Creiamone un paio:
In [7]: one = state.solver.BVV(1, 64)
In [8]: one
<BV64 0x1>
In [9]: one_hundred = state.solver.BVV(100, 64)
In [10]: one_hundred
<BV64 0x64>Essendo degli interi, si possono sommare per esempio (anche con interi Python):
In [11]: one + one_hundred
<BV64 0x65>
In [12]: one + 0x4
<BV64 0x5>Ora creiamo dei bitvector che siano però delle variabili simboliche, quello che a noi più interessa in questo momento:
In [13]: x = state.solver.BVS("x", 64)
In [14]: x
<BV64 x_9_64>
In [15]: y = state.solver.BVS("y", 64)
In [16]: y
<BV64 y_10_64>Come vediamo, per creare bitvector simbolici si utilizza il metodo BVS(), mentre per creare bitvector con valori concreti si utilizza il metodo BVV(). Inoltre, angr assegna un identificativo univoco ad ogni bitvector simbolico, incrementando anche un contatore.
E ora, se sommiamo x e y, quale ci aspettiamo sia il risultato?
In [17]: x + y
<BV64 x_0_64 + y_1_64>Il risultato sarà un AST indicante l'operazione tra le variabili simboliche.
In angr, ogni bitvector simbolico è un AST. Un'operazione tra 2 AST ritornerà sempre come risultato un AST:
In [18]: tree = (x + 1) / (y + 2)
In [19]: tree
<BV64 (x_9_64 + 0x1) / (y_10_64 + 0x2)>Oltre a valori interi, con i bitvectors possono essere rappresentati float, double ma soprattutto boolean.
In [20]: x == 1
<Bool x_9_64 == 0x1>
In [21]: x + y == one_hundred + 5
<Bool (x_9_64 + y_10_64) == 0x69>Dato lo stato di esecuzione di un programma, tramite l'AST potremo risalire alla catena di operazioni che dal programma sono state svolte fino a quel punto, capendo per quale valore di quale variabile, la condizione booleana si è rivelata falsa, e quale deve esse il valore che porterà la condizione ad essere true.
In questo esempio, quale deve essere il valore di input di x e y affinchè la condizione "x + y = 0x69" sia vera? Angr ci aiuta a rispondere a questo genere di domande.
Vediamone un esempio più concreto.
Cracking
Il nostro programma in analisi è un binario in formato ELF chiamato crackme (link https://gist.github.com/inaz2/e609a9e00906fb68f9a916b878d5fc75)
Di questo binario disponiamo del sorgente, ma non è questo ciò che conta (l'esempio è banale, ma utile per capire le basi di angr).
La funzione target è crackme():
int crackme(char *s, int n)
{
if (strlen(s) != 13) {
return 0;
}
if (strcmp(s, "hacktheplanet") != 0) {
return 0;
}
if (n != 1337) {
return 0;
}
return 1;
}
Disassemblata:
$ objdump -M intel -d crackme | sed -n '/<crackme>:/,/^$/p'
00000000004005f6 <crackme>:
4005f6: 55 push rbp
4005f7: 48 89 e5 mov rbp,rsp
4005fa: 48 83 ec 10 sub rsp,0x10
4005fe: 48 89 7d f8 mov QWORD PTR [rbp-0x8],rdi
400602: 89 75 f4 mov DWORD PTR [rbp-0xc],esi
400605: 48 8b 45 f8 mov rax,QWORD PTR [rbp-0x8]
400609: 48 89 c7 mov rdi,rax
40060c: e8 9f fe ff ff call 4004b0 <strlen@plt>
400611: 48 83 f8 0d cmp rax,0xd
400615: 74 07 je 40061e <crackme+0x28>
400617: b8 00 00 00 00 mov eax,0x0
40061c: eb 31 jmp 40064f <crackme+0x59>
40061e: 48 8b 45 f8 mov rax,QWORD PTR [rbp-0x8]
400622: be 34 07 40 00 mov esi,0x400734
400627: 48 89 c7 mov rdi,rax
40062a: e8 a1 fe ff ff call 4004d0 <strcmp@plt>
40062f: 85 c0 test eax,eax
400631: 74 07 je 40063a <crackme+0x44>
400633: b8 00 00 00 00 mov eax,0x0
400638: eb 15 jmp 40064f <crackme+0x59>
40063a: 81 7d f4 39 05 00 00 cmp DWORD PTR [rbp-0xc],0x539
400641: 74 07 je 40064a <crackme+0x54>
400643: b8 00 00 00 00 mov eax,0x0
400648: eb 05 jmp 40064f <crackme+0x59>
40064a: b8 01 00 00 00 mov eax,0x1
40064f: c9 leave
400650: c3 retCome vediamo dalla funzione main del programma:
int main(int argc, char *argv[])
{
if (crackme(argv[1], atoi(argv[2])) == 1) {
puts("good job!");
} else {
puts("wrong.");
}
return 0;
}Se la funzione crackme ritorna 1, allora siamo autenticati, altrimenti no. Guardando la funzione crackme disassemblata, vediamo come il suo valore di ritorno è 1 se e solo se l'istruzione mov eax, 0x1 ad indirizzo 0x40064a viene eseguita, che, nella terminologia di angr, significa che esista almeno uno stato di esecuzione del programma in cui rip è uguale a 0x40064a.
Quale dovrà essere l'input passato affinchè esista tale stato di esecuzione?
Io ho realizzato un exploit diverso da quello dell'autore originale, che utilizza i nuovi metodi solver.eval() e il SimulationManager di angr. Inoltre, il mio exploit è indipendente dall' indirizzo di memoria della funzione crackme, perchè se lo calcola al momento (bypassando cosi ASLR, anche se completamente inutile perchè mi sto "hackerando" da solo lol)
Cominciamo creando un nuovo progetto in angr:
import angr
proj = angr.Project('/home/luca/workspace/crackme/crackme', load_options={'auto_load_libs': False})Ci ricaviamo l'indirizzo della funzione "crackme" del binario, attraverso la libreria di angr:
cfg = proj.analyses.CFGFast()
fun = proj.kb.functions.get('crackme')
addr_crackme = fun.startpoint.addrIgnoriamo i warning emessi dall'interprete.
Creiamo un nuovo stato di esecuzione:
state = proj.factory.blank_state(addr=addr_crackme)A differenza del primo esempio, dove ho utilizzato il metodo entry_state(), questa volta utilizzo il metodo blank_state(), che crea uno stato di esecuzione partendo dall'indirizzo di memoria passato input. Conviene iniziare l'esecuzione simbolica direttamente dalla funzione target e non dall'entry point del programma, poichè altrimenti l'AST generato sarebbe molto più grande e l'exploit necessiterebbe di più tempo per risolvere tutti gli input possibili.
Ora creiamo un nuovo oggetto chiamato SimulationManager. Questo è uno dei core object di angr, e le sue funzionalità sono davvero tante. Per il nostro scopo, ci basta sapere che il SimulationManager è in grado di risalire l'AST, partendo dall'ultima istruzione eseguita, attraverso il metodo explore().
simgr = proj.factory.simulation_manager(state)
simgr.explore(find=addr_crackme + 0x54, avoid=addr_crackme + 0x59)
Una volta lanciato il metodo explore, possiamo fare un dump della memoria del processo per lo stato di esecuzione cui risulterà che l'istruzione ad indirizzo crackme + 0x54, ovvero:
mov eax, 0x1E stata eseguita.
L'exploit finale è questo:
import angr
proj = angr.Project('./crackme', load_options={'auto_load_libs': False})
cfg = proj.analyses.CFGFast()
fun = proj.kb.functions.get('crackme')
addr_crackme = fun.startpoint.addr
state = proj.factory.blank_state(addr=addr_crackme)
simgr = proj.factory.simulation_manager(state)
simgr.explore(find=addr_crackme + 0x54, avoid=addr_crackme + 0x59)
if len(simgr.found) > 0:
found = simgr.found[0]
arg1 = found.solver.eval(found.memory.load(found.regs.rbp-0x8, 8, endness='Iend_LE'), cast_to=int)
arg2 = found.solver.eval(found.memory.load(found.regs.rbp-0xc, 4, endness='Iend_LE'), cast_to=int)
print("arg1: ", found.solver.eval(found.memory.load(arg1, 0x10), cast_to=bytes))
print("arg2: ", arg2)Se lo copiamo e incolliamo dentro ipython, ecco che avremo effettuato il crack della password di autenticazione:
Completo!
Fonti e approfondimenti (in inglese):