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 y

In 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 virtualenvwrapper

Poi installare angr lanciando questo comando:

virtualenv --python=$(which python3) angr && pip3 install angr

Una volta terminata l'installazione, avviamo angr in una shell python per verificare che l'istallazione nell'ambiente virtuale sia andata a buon fine:

[email protected]:~$ source angr/bin/activate
(angr) [email protected]:~$ 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 <[email protected]>
  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 <[email protected]>
  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                      ret

Come 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.addr

Ignoriamo 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, 0x1

E 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):

  1. https://en.wikipedia.org/wiki/Symbolic_execution
  2. https://en.wikipedia.org/wiki/Abstract_syntax_tree
  3. https://angr.io/
  4. https://docs.angr.io/core-concepts
  5. https://ipython.org/
  6. https://arxiv.org/pdf/1610.00502.pdf