Introduzione a Pocket: offuscatore per espressioni MBA

24 luglio 2023 – 26 min – 5334 parole

L’offuscamento del codice è una tecnica che consente di applicare delle trasformazioni ad un codice per rendere più difficile e più complessa eventuali analisi statiche (automatiche e non). L’analisi statica raggruppa una serie di operazioni che un’analista può svolgere su un eseguibile per cercare di ottenere le informazioni come le strutture ad alto livello, le variabili originali.

Tra le tecniche di analisi statica di un software, possiamo trovare il reverse engineering, chiamata anche ingegneria inversa. Questa tecnica consente di recuperare parte delle informazioni che permettono ad un’analista di comprendere meglio come funziona il software, in che modo interagisce con i dati e quali algoritmi utilizza. Ottenere il codice originario presenta spesso diverse sfide e insidie dal momento che il codice macchina non consente di esprimere i cicli e le strutture dati di alto livello.

Per alcuni linguaggi di programmazione (come Java), è possibile recuperare il codice iniziale senza problemi. È molto probabile che analizzando una qualsiasi applicazione basata su Java o .NET si riesca a trovare la maggior parte parte della logica originale. Questo è dato dall’espressività del loro linguaggio macchina, come ad esempio nel Java Bytecode, in cui è possibile memorizzare più informazioni rispetto al linguaggio macchina primitivo utilizzato dalla CPU (Assembly).

Tutti gli strumenti di reverse engineering come IDA, Ghidra e Binary Ninja basano il loro funzionamento su alcuni componenti come i disassemblatori (consentono la traduzione da un flusso grezzo di byte alle istruzioni in linguaggio macchina) e decompilatori (consentono la traduzione dal linguaggio macchina ad un linguaggio C-like di alto livello, includendo informazioni come stringhe e cicli). Questi strumenti sono divenuti con il tempo molto potenti e con un po’ di fortuna è possibile recuperare gran parte della logica del programma. I decompilatori sono ancora approssimativi: non possono certamente generare codice ricompilabile, però attraverso il codice “decompilato” è possibile ricreare il software.

Un esempio? 3D Pinball Space Cadet è il tentativo della ricostruzione del gioco popolare 3D Pinball per Windows XP. Gli analisti sono riusciti tramite Ghidra e IDA a ricostruire gran parte delle strutture dati originali, popolarle con i valori corretti e riesumere il gioco per portarlo su piattaforme differennti (Nintendo 3DS, AmigaOS, Android). Come hanno fatto? Hanno utilizzato un processo che mischiava reverse engineering e debugging dell’applicativo originale per riuscire a capire come funzionasse la gestione delle collisioni, l’aggiornamento del punteggio e la gestione dei suoni.

L’attività di reverse engineering consente agli analisti di andare in profondità rispetto a come il software lavora, su quali dati si basa e potenzialmente su eventuali punti deboli del software. Qui si apre un enorme vaso di Pandora. Una parte delle informazioni che vengono incluse all’interno del software potrebbero essere riservate ad uno specifico utente o potrebbero celare alcuni dettagli che non vogliamo cedere al primo che esegue strings software_aziendale. Se pensiamo poi ad assets aziendale, le prime aziende quotate in borsa sono produttori di software e paradossalmente il software (e gli algoritmi) è il loro prodotto di punta: devono proteggerlo.

Immaginiamo di trovare all’interno di un software una specifica sequenza di istruzioni che rendono il software più veloce, più performante o semplicemente migliore per i clienti. Come concorrente potrei essere interessato a replicare le stesse istruzioni o la stessa idea nel mio software per ridurre il divario tra il mio software e quello della concorrenza. Il software potrebbe contenere inoltre alcuni segreti come chiavi API, metodi interni/privati che l’azienda d’origine potrebbe voler nascondere, a cui sono interessato essendo il principale avversario.

Molto velatamente ho introdotto alcuni punti per motivare la scelta di offuscare il codice. La protezione della proprietà intellettuale è uno dei motivi principali per voler offuscare il codice e rendere più complessa l’analisi statica. Gli algoritmi che l’azienda sviluppa per rendere più performante un’applicazione oppure per fare alcune scelte che hanno un impatto socio/economico sono algoritmi costituiscono una risorsa molto preziosa per l’attaccante. Per rendere più difficile l’analisi, è necessario complicare le informazioni su cui si basano i decompilatori: istruzioni e dati. La tecnica per rendere più complicato un qualsiasi programma si chiama offuscamento e consente dato un programma P di generare un programma P’ più difficile da analizzare.

In questo articolo, introdurremo POCKET, un programma che consente di avere un primo approccio all’offuscamento. Pocket è un programma a linea di comando che accetta una espressione MBA (Mixed Boolean Arithmetic) e applicando alcune regole di trasformazione si riesce a rendere più complessa l’espressione. Per capire meglio come funziona e quali vantaggi presenta, introduciamo un esempio reale.

Il compito dei decompilatori

Una volta che il disassemblatore ha tradotto la sequenza di byte grezzi in microistruzioni assembly, il risultato può essere simile a qualcosa così:

inc eax
and eax, ebx
and eax, ecx

Il decompilatore può quindi incominciare a tradurre le microistruzioni in un linguaggio più semplice. All’inizio il decompilatore lavora tramite “pattern matching”: nota infatti un incremento in eax, un and tra eax ed ebx, ed un altro and tra eax ed ebx. Le istruzioni commentate diventano così:

inc eax				; eax = eax + 1
and eax, ebx		; eax = eax & ebx
and eax, ecx      	; eax = eax & ecx

Il decompilatore nota che in tutte e tre le espressioni eax è il registro di sinistra utilizzato per l’assegnamento; il decompilatore quindi provvede a riscrivere le espressioni con un’unica espressione: eax = ((eax + 1) & ebx) & ecx. Ipotizziamo inoltre di assegnare ad eax il valore 2, ad ebx il valore 5 e ad ecx il valore 3. Il risultato finale di questa espressione è 3. All’interno di un programma questo valore potrebbe rappresentare l’indice di un elemento, il numero di volte da iterare all’interno di un loop. Potreste pensare che sia un valore da niente.

Ma invece di valori molto semplici perché non possiamo assegnare un valore come 0x80021002 ad eax? Il risultato è 0x80021002, tuttavia basta aggiungere una singola istruzione per rendere le cose più interessanti. Aggiungiamo jmp %eax. In questo modo, l’esecuzione della successiva istruzione è dinamica: dipende dal valore di eax. Come detto, quindi, non ci preoccupiamo dei possibili valori che un dato può assumere.

Ci preoccupiamo invece della leggibilità dell’espressione per un decompilatore. L’espressione eax = ((eax + 1) & ebx) & ecx è molto leggibile: sono 2 semplici operazioni and e una somma. Immaginando di conoscere i valori di eax, ebx, ed ecx, il decompilatore potrebbe addirittura sostituire eax con il valore calcolato:

eax = 0x80021002
eax = ((eax + 1) & ebx) & ecx

// risultato: 0x80021003

L’espressione che abbiamo appena analizzato contiene operazioni algebriche (come la somma) e operazioni logiche (AND): per questo, l’espressione prende il nome di espressione Mixed Boolean Arithmetic. È molto semplice da calcolare come espressione e non richiede particolari accortezze. Come possiamo renderla più inaccessibile? Per il momento consideriamo solo trasformazioni sull’espressioni.

Ad esempio, sappiamo che una qualsiasi operazione di somma tra X e Y X+Y può essere trascritta come (X & Y) + (X | Y). Proviamo ad applicare questra trasformazione: nel nostro caso X sarà eax mentre Y un valore immediato, ovvero 1. Il risultato di questa trasformazione è (eax & 1) + (eax | 1) e riscrivendo l’espressione eax = (((eax & 1) + (eax | 1) & ebx) & ecx. Possiamo quindi passare alla seconda trasformazione che interessa X & Y. L’operazione di AND tra due numeri interi equivale a (X + Y) - (X | Y), in questo caso X = (eax & 1) + (eax | 1) mentre Y = ebx: il risultato finale è (((eax & 1) + (eax | 1)) + ebx) - (((eax & 1) + (eax | 1)) | ebx).

Applichiamo un’ultima volta questa regola per ottenere l’espressione finale offuscata:

((((((eax & 1) + (eax | 1)) + ebx) - (((eax & 1) + (eax | 1)) | ebx)) + ecx) - (((((eax & 1) + (eax | 1)) + ebx) - (((eax & 1) + (eax | 1)) | ebx)) | ecx))

Abbiamo quindi capito con un reale esempio le potenzialità delle espressioni MBA. L’offuscamento di queste espressioni consiste nell’applicare in modo iterativo le regole di riscrittura per aumentare la complessità di queste espressioni, preservandone la semantica. Infatti le regole di riscrittura delle espressioni non devono cambiare il risultato dell’espressione (perché altrimenti l’offuscamento sarebbe invalido).

Le regole di trasformazione si basano su alcune operazioni che se eseguite in un certo ordine risultano essere equivalenti alle operazioni originali.

Utilizzando POCKET

POCKET è uno strumento che consente di applicare in modo automatico queste regole di trasformazione ed è stato scritto in Rust con la grammatica basata su Pest. Lo sviluppo del progetto non è stato particolarmente ostico dal momento che ho consentito di delegare gran parte della complessità del parser a Pest. La difficoltà è stata più cercare di comprendere il metodo di funzionamento di Rust, capire come ovviare ad alcune problematiche di borrowing e un fastidioso problema con un stack overflow. (Spoiler: chiamavo ricorsivamente la stessa operazione)

Compilando il progetto con cargo compile, viene generato il binario pocket. Possiamo avviarlo senza problemi, resterà in attesa di una espressione in input. Per riprendere l’espressione di prima possiamo considerare: (A + 1) & B & C. POCKET costruisce un albero sintattico dall’espressione che verrà attraversato per applicare le regole di trasformazione. Un albero sintattico per l’espressione dell’esempio è:

.
|-- &
|------ +
|--------- A
|--------- 1
|------ &
|-------- B
|-------- C

Ogni nodo può essere uno di 4 tipi diversi:

Immediate e cont sono terminali in quanto non hanno figli, mentre BinaryOperation ha due figli e UnaryOperator un figlio solo. Una volta che l’albero è stato costruito, l’albero viene visitato interamente per poter applicare le regole di trasformazione: immaginatevi uno switch costruito in base all’operazione binaria da sostituire.

I valori di X e di Y vengono ogni volta sostituiti dai figli sinistro e destro delle operazioni, in questo modo riesco ad effettuare la sostituzione senza perdere il contesto in cui mi trovo. Sto lavorando per poter aggiungere ulteriori trasformazioni sui valori immediati. Se le trasformazioni per le operazioni binarie sono limitate, le trasformazioni per i valori immediati sono potenzialmente infiniti: posso scrivere 2 come la differenza tra 48 e 46, oppure tra 54 e 52 oppure la differenza tra 52 e 54 cambiati di segno.

Le trasformazioni di equivalenza sono frutto di studi sulla compatibilità degli operatori nell’aritmetica binaria. Poniamo caso di avere una espressione del tipo 2 * (x ^ y): questa è equivalente a (2x ^ 2y). Il lettore meno attento potrebbe aver confuso queste due formule con la semplice proprietà distributiva: moltiplico x e y per due e mantengo l’operazione di XOR.

Non funziona sempre così!!! Già con 3 * (x ^ y) != (3x ^ 3y) la proprietà distributiva sparisce. La compatibilità tra le formule e gli operatori si basa sul tipo di insieme che stiamo considerando: l’insieme basato sull’aritmetica binaria!

Ritornando all’esempio, il risultato dell’offuscamento risulta così:

((((((A & 1) + (A | 1)) + B) - (((A & 1) + (A | 1)) | B)) + C) - (((((A & 1) + (A | 1)) + B) - (((A & 1) + (A | 1)) | B)) | C))

Mentre se si volesse avere un altro livello di offuscamento partendo dalla espressione di prima, ecco qui il risultato:

((((((((((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + 
(1 + ((~A) | (~1))))))) & B) + (((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1)
- (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) | B)) ^ (-(((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A
) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) + (B + (1 + ((~((((A + 1) - 
(A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))
)) | (~B))))))) + (2 * (((((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A |
1)) | (A + (1 + (1 + ((~A) | (~1))))))) & B) + (((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)
))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) | B)) & (-(((((A + 1) - (A | 1)) & 
A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) + (B + (1 
+ ((~((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 
+ ((~A) | (~1)))))))) | (~B))))))))) & C) + (((((((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)
)))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) & B) + (((((A + 1) - (A | 1)) & (A +
(1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) | B)) ^ (-(((
(A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) |
(~1))))))) + (B + (1 + ((~((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - 
(A | 1)) | (A + (1 + (1 + ((~A) | (~1)))))))) | (~B))))))) + (2 * (((((((A + 1) - (A | 1)) & (A +
(1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) & B) + ((
(((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + (
(~A) | (~1))))))) | B)) & (-(((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A 
+ 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) + (B + (1 + ((~((((A + 1) - (A | 1)) & (A + (
1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1)))))))) | (~B)
)))))))) | C)) ^ (-(((((((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (
A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) & B) + (((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) 
| (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) | B)) ^ (-(((((A + 1) 
- (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1
))))))) + (B + (1 + ((~((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) -
(A | 1)) | (A + (1 + (1 + ((~A) | (~1)))))))) | (~B))))))) + (2 * (((((((A + 1) - (A | 1)) & (A + (1 
+ (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) & B) + (((((A + 1
) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1)
)))))) | B)) & (-(((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | 
(A + (1 + (1 + ((~A) | (~1))))))) + (B + (1 + ((~((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)
)))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1)))))))) | (~B))))))))) + (C + (1 + ((~(((((
((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A)
| (~1))))))) & B) + (((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1))
| (A + (1 + (1 + ((~A) | (~1))))))) | B)) ^ (-(((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))
)) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) + (B + (1 + ((~((((A + 1) - (A | 1)) &
(A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1)))))))) | (~B))
)))) + (2 * (((((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A |
(1 + (1 + ((~A) | (~1))))))) & B) + (((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A 
+ 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) | B)) & (-(((((A + 1) - (A | 1)) & (A + (1 + (1 
+ ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) + (B + (1 + ((~((((A +
1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | 
(~1)))))))) | (~B)))))))))) | (~C))))))) + (2 * (((((((((((A + 1) - (A | 1)) & (A + (1 + (1 +
((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) & B) + (((((A +
1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((
~A) | (~1))))))) | B)) ^ (-(((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (
A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) + (B + (1 + ((~((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~
	A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1)))))))) | (~B))))))) + (2 * ((
(((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~
	A) | (~1))))))) & B) + (((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (
A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) | B)) & (-(((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) |
 (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) + (B + (1 + ((~((((A + 1) - (A 
 	| 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1)))))
 ))) | (~B))))))))) & C) + (((((((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) 
- (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) & B) + (((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) |
 (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) | B)) ^ (-(((((A + 1) - (A | 1)
 ) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) + (
 B + (1 + ((~((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (
 1 + (1 + ((~A) | (~1)))))))) | (~B))))))) + (2 * (((((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) 
 | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) & B) + (((((A + 1) - (A | 1))
& (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) | B))
& (-(((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (
1 + ((~A) | (~1))))))) + (B + (1 + ((~((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + 
(((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1)))))))) | (~B))))))))) | C)) & (-(((((((((A + 1
) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))
))))) & B) + (((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (
A + (1 + (1 + ((~A) | (~1))))))) | B)) ^ (-(((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))
))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) + (B + (1 + ((~((((A + 1) - (
A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1)))))))
) | (~B))))))) + (2 * (((((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A |
1)) | (A + (1 + (1 + ((~A) | (~1))))))) & B) + (((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))
))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) | B)) & (-(((((A + 1) - (A | 1)) & (A
 + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) + (B + (1 
+ ((~((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 
+ ((~A) | (~1)))))))) | (~B))))))))) + (C + (1 + ((~((((((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A)
| (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) & B) + (((((A + 1) - (A | 1))
 & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) | B)) 
^ (-(((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1  
((~A) | (~1))))))) + (B + (1 + ((~((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((
A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1)))))))) | (~B))))))) + (2 * (((((((A + 1) - (
A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1)))))))
 & B) + (((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + 
(1 + ((~A) | (~1))))))) | B)) & (-(((((A + 1) - (A | 1)) & (A + (1 + (1 + ((~A) | (~1)))))) + (((
A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1))))))) + (B + (1 + ((~((((A + 1) - (A | 1)) & (A +
(1 + (1 + ((~A) | (~1)))))) + (((A + 1) - (A | 1)) | (A + (1 + (1 + ((~A) | (~1)))))))) | (~B)))
))))))) | (~C)))))))))

Come abbiamo specificato più volte, le regole di trasformazione possono continuare ad essere applicate all’infinito. È chiaro che già al terzo livello di offuscamento le espressioni generate sono molto pesanti da visualizzare. Ci chiediamo quindi: come possiamo effettivamente verificare che le trasformazioni sono andate a buon fine?

Il dogma centrale della biologia dell’offuscamento riporta “tutte le trasformazioni devono essere applicate SE E SOLO SE la trasformazione non modifica il risultato originale”. In maniera più elegante, possiamo dire quindi che una espressione offuscata è equivalente ad una espressione se e solo se l’espressione offuscata, valutata correttamente, restituisce lo stesso risultato dell’espressione originale. Per verificare quindi le riscritture, ho scritto un semplice interprete.

fn eval(&self, node: &Node) -> i32{
    match node {
        Node::Cont(_set, value) => *value,
        Node::Immediate(value) => *value,
        Node::UnaryExpr { op, child } => {
            let child = self.eval(child);
            return match op{
                UnaryOperator::Not => !child,
                UnaryOperator::Minus => -child,
            }
        },
        Node::BinaryExpr { op, lhs, rhs } => {
            let left_value = self.eval(lhs);
            let right_value = self.eval(rhs);
            match op{
                Operator::And => left_value & right_value,
                Operator::Or => left_value | right_value,
                Operator::Xor => left_value ^ right_value,
                Operator::Plus => left_value + right_value,
                Operator::Minus=> left_value - right_value,
                Operator::Mul => left_value * right_value,
            }
        },
    }
}

La funzione eval consente di valutare una espressione composto da operazioni binarie, operazioni unarie, valori immediati e insiemi. Dal momento che troviamo le stesse operazioni implementate in Rust l’unica preoccupazione che vogliamo affrontare è sulla valutazione del nodo destro e sinistro. Ad esempio riprendendo il solito esempio (A + 1) & B & C: per eseguire l’operazione AND di (A + 1) & B, vogliamo prima visitare il sottoalbero del figlio destro e il sottoalbero del figlio sinistro.

Per il figlio destro il valore è praticamente dato dal valore contenuto all’interno del nodo (viene restituito *value da eval). Per il figlio sinistro invece è necessario valutare A + 1. Quindi richiamiamo per entrambi la funzione eval per lhs e per rhs, successivamente esegue l’operazione di somma. La domanda che può sorgere spontaneamente riguarda il numero contenuto all’interno del nodo SET. Se POCKET accetta una espressione, come determina il numero per ogni lettera?

Non utilizziamo valori randomici; per garantire il determinismo tra i vari passaggi di offuscamento, assegniamo per ora il numero del carattere ASCII che rappresenta il set. Ad esempio, A diventa 65, B 66 e così via. In un futuro molto vicino, implementerò una tabella chiave-valore che conterrà un numero randomico per ogni set. La tabella viene mantenuta per tutti i passi di offuscamento. In questo modo riusciamo a verificare che l’espressione offuscata consente di calcolare lo stesso valore dell’espressione originale. Mancherebbe solamente la trasformazione in codice assembly e poi POCKET potrebbe essere veramente implementato come rewriter di binari.

Le espressioni MBA sono risultate molto interessanti! L’obiettivo di POCKET è stato quello di sviluppare un progetto con Rust che avesse una qualsiasi utilità nel mondo dell’ingegneria del software. Non considero POCKET un software maturo, né completo, ma solo un progetto del weekend per imparare meglio come poter manipolare un AST, come costruire un interprete in Rust e come poter sostituire alcuni nodi. È possibile migliorare il progetto includendo più regole e agendo su alcuni casi limite che i programmi di contrattacco potrebbero eliminare.

Il paper di riferimento per avere un approccio più rigoroso e formale è Information Hiding in Software with Mixed Boolean-Arithmetic Transforms di Yongxin Zhou, Alec Main, Yuan X. Gu e Harold Johnson. Lettura consigliata per poter descrivere formalmente le espressioni MBA!

Contrattacchi

È possibile affermare che questi metodi di offuscamento possono essere sicuri da eventuali contrattacchi? Assolutamente no. L’industria e la ricerca accademica ha prodotto diversi paper che includono metodi sempre più sofisticati di risoluzione delle espressioni offuscate. Tendenzialmente noi vorremmo che la trasformazione da espressione originale ad espressione offuscata sia irreversibile. Tuttavia, dal momento che le regole delle trasformazioni sono ben note in letteratura, è possibile sviluppare diversi programmi che possono risolvere e “riassumere” le espressioni offuscate.

Nel prossimo articolo, citeremo per bene eventuali contrattacchi e relativi paper contro l’offuscamento delle MBA. Basti pensare che LLVM ha una parte di codice che serve proprio a condensare eventuali espressioni offuscate tramite pattern matching. Qui un estratto:

// A & (A ^ B) --> A & ~B
if (match(Op1, m_OneUse(m_c_Xor(m_Specific(Op0), m_Value(B)))))
  return BinaryOperator::CreateAnd(Op0, Builder.CreateNot(B));
// (A ^ B) & A --> A & ~B
if (match(Op0, m_OneUse(m_c_Xor(m_Specific(Op1), m_Value(B)))))
  return BinaryOperator::CreateAnd(Op1, Builder.CreateNot(B));

Dovremo cercare di rendere POCKET immune a questi controattacchi. Implementeremo nuove operazioni per rendere la vita più complessa ai programmi che cercano di riscrivere le espressioni offuscate in espressioni più semplici. Se avete domande o curiosità sul progetto POCKET, o semplicemente volete segnalarmi un refuso/errore, contattatemi su seekbytes@protonmail.com.