# L'approccio

Ci basiamo sull'intuizione chiave che una traccia offuscata T' (dal codice offuscato P') combina istruzioni originali del codice originale P (la traccia T corrispondente a T' nel codice originale) e istruzioni della macchina virtuale VM tali che T' = T + VM(T). Se siamo in grado di distinguere tra queste due sottosequenze di istruzioni T e VM(T), possiamo quindi ricostruire un percorso del programma originale P a partire da una traccia T'. Ripetendo questa operazione per coprire tutti i percorsi del programma virtualizzato, saremo in grado di ricostruire il programma originale P. Nel nostro esempio pratico, il codice originale ha un numero finito di percorsi eseguibili, cosa che accade in molte situazioni che coinvolgono la protezione della proprietà intellettuale. Per fare ciò, procediamo con i seguenti passaggi:

1. Identificare la funzione virtualizzata e i suoi argomenti
2. Generare una traccia VMProtect del target
3. Rieseguire la traccia VMP e costruire espressioni simboliche per ottenere la relazione tra input e output
4. Applicare ottimizzazioni sulle espressioni simboliche per evitare il più possibile le istruzioni della VM
5. Elevare la nostra rappresentazione simbolica a LLVM-IR per costruire una nuova versione non protetta del target

## Esempio 1: Una semplice operazione bit a bit

Prendiamo come primo esempio la seguente funzione: prende due input e restituisce `x ^ y` che è protetta da VMProtect.

```c
int xor(int x, int y) {
  return x ^ y;
}
``````cpp
int secret(int x, int y) {
  VMProtectBegin("secret");
  int r = x ^ y;
  VMProtectEnd();
  return r;
}

Puoi vedere il risultato [qui](https://github.com/jonathansalwan/vmprotect-devirtualization/blob/HEAD/vmp_traces/sample2.vmp.trace). Il formato delle tracce utilizza tre tipi di operazioni: `mr`, `r` e `i`.
`mr` è un accesso in lettura alla memoria eseguito dall'istruzione `i`, e `r` sono i registri della CPU. Per esempio:```
mr:0x7ffda459d718:8:0x227db4f8
r:0x40200a:0x0:0x7ffda459f571:0x2:0x40200a:0x0:0x0:0x7ffda459d688:0x0:0x0:0x7feee9b80ac0:0x7feee9b8000f:0xad1c3e:0x0:0x0:0x0
i:0x89173e:8:488BB42490000000

Una volta generata la traccia VMP, la riproduciamo utilizzando lo script [attack_vmp.py](https://github.com/jonathansalwan/vmprotect-devirtualization/blob/HEAD/attack_vmp.py). Questo script usa
[Triton](https://github.com/jonathansalwan/Triton) per costruire il predicato di percorso della traccia. Nota che tutte le espressioni che
coinvolgono variabili simboliche (input della funzione) vengono mantenute simboliche, mentre tutte le espressioni non correlate agli input vengono concretizzate. In
altre parole, le nostre espressioni simboliche non contengono alcuna operazione relativa alla macchina virtuale (il meccanismo
stesso non dipende dall'utente) ma solo operazioni relative al programma originale.

Ad esempio, di seguito è riportato un esempio di concretizzazione. A sinistra abbiamo un AST che contiene sottoespressioni che non coinvolgono
variabili simboliche (`1 + 2` e `6 ^ 3`). Quindi questi rami vengono concretizzati e sostituiti con costanti `3` e `5`, portando
all'AST a destra. **È così che devirtualizziamo il codice.**

<p align="center">
  <img src="https://assets.kitploit.com/production/public/readmes/8096/857ed50cfe9cb2347f816ece1d8dc4c13174c971dcb65ebc5621be14269a5ca8.png">
</p>

**Nota sul backward slicing a livello di formula**: Come è comune nell'esecuzione simbolica, la rappresentazione simbolica viene prima
calcolata in avanti lungo il percorso, quindi tutte le operazioni logiche e le definizioni che non influenzano né il risultato
finale né il percorso seguito vengono rimosse dall'espressione simbolica (slicing della formula, noto anche come pruning della formula). Questo si rivela
equivalente, sulla formula, a un'analisi del codice di backward slicing a partire dall'output del programma. Quindi, al ritorno della
funzione `secret`, abbiamo un'espressione della relazione tra gli input e l'output senza le istruzioni di VMProtect.

Lo script `./attack_vmp.py` accetta come parametri il file di traccia e la dimensione delle variabili simboliche. Ricorda, erano `edi` e
`esi`, quindi sono lunghi 4 byte. Il risultato dello script è il seguente:```
$ ./attack_vmp.py --trace1 ./vmp_traces/sample2.vmp.trace --symsize 4
[+] Replaying the VMP trace
[+] Symbolize inputs
[+] Instruction executed: 12462
[+] Emulation done
[+] Return value: 0x3
[+] Devirt expr: (bvor (bvnot (bvor (bvnot (bvnot x)) (bvnot y))) (bvnot (bvor (bvnot x) (bvnot (bvand (bvnot y) (bvnot y))))))
[+] Synth expr: (bvxor x y)

[+] LLVM IR ==============================

; ModuleID = 'tritonModule'
source_filename = "tritonModule"

define i32 @__triton(i32 %SymVar_0, i32 %SymVar_1) {
entry:
  %0 = xor i32 %SymVar_0, %SymVar_1
  ret i32 %0
}

[+] EOF LLVM IR ==============================

Tuttavia, non siamo riusciti a recuperare l'espressione originale che era una semplice operazione `XOR`. Sembra che lo `XOR` sia stato
tradotto in operazioni bitwise. Fortunatamente, abbiamo recentemente rilasciato nuove funzionalità nel progetto Triton, ovvero
un [synthesizer](https://github.com/JonathanSalwan/Triton/issues/1074) e un lifter verso
[LLVM-IR](https://github.com/JonathanSalwan/Triton/issues/1078). Possiamo quindi sintetizzare l'espressione, ottenendo l'espressione
`(bvxor x y)`. È un buon successo e ora possiamo andare oltre, sollevando questa espressione in LLVM-IR e poi compilare un nuovo codice binario
devirtualizzato.

## Esempio 2: Un'operazione MBA protetta

Ok, ora diamo un'occhiata a un altro esempio che tenta di nascondere un'operazione MBA. Il codice sorgente originale è il seguente:```cpp
// This function is an MBA that computes: (x ^ 92) + y
// We will protect this MBA with VMProtect and see if we can recover "(x ^ 92) + y"
char secret(char x, char y) {
  VMProtectBegin("secret");
  int a = 229 * x + 247;
  int b = 237 * a + 214 + ((38 * a + 85) & 254);
  int c = (b + ((-(2 * b) + 255) & 254)) * 3 + 77;
  int d = ((86 * c + 36) & 70) * 75 + 231 * c + 118;
  int e = ((58 * d + 175) & 244) + 99 * d + 46;
  int f = (e & 148);
  int g = (f - (e & 255) + f) * 103 + 13;
  int r = (237 * (45 * g + (174 * g | 34) * 229 + 194 - 247) & 255) + y;
  VMProtectEnd();
  return r;
}

Una volta generata la [traccia VMP](https://github.com/jonathansalwan/vmprotect-devirtualization/blob/HEAD/vmp_traces/sample3.vmp.trace), esegui lo script `./attack_vmp.py`.```
$ ./attack_vmp.py --trace1 ./vmp_traces/sample3.vmp.trace --symsize 1
[+] Replaying the VMP trace
[+] Symbolize inputs
[+] A potential symbolic jump found on CF flag: 0x821dac: popfq - Model: {0: x:32 = 0xa3, 1: y:32 = 0xff}
[+] A potential symbolic jump found on CF flag: 0x87f437: popfq - Model: {0: x:32 = 0xa3, 1: y:32 = 0xff}
[+] Instruction executed: 25085
[+] Emulation done
[+] Return value: 0x5f
[+] Devirt expr: In: (bvadd (bvadd (bvshl (bvadd (_ bv1 32) (bvnot (bvlshr (concat (_ bv0 8) (_ bv0 8) ((_ extract 15 8)  ...
[+] Synth expr: In: (bvadd (bvadd (bvshl (bvadd (_ bv1 32) (bvnot (bvlshr (concat (_ bv0 8) (_ bv0 8) ((_ extract 15 8)  ...

[+] LLVM IR ==============================

; ModuleID = 'tritonModule'
source_filename = "tritonModule"

define i32 @__triton(i8 %SymVar_0, i8 %SymVar_1) {
entry:
  %0 = xor i8 %SymVar_0, 92
  %1 = and i8 %SymVar_0, 0
  %2 = zext i8 %1 to i32
  %3 = or i32 0, %2
  %4 = shl i32 %3, 8
  %5 = zext i8 %0 to i32
  %6 = or i32 %4, %5
  %7 = and i8 %SymVar_1, 0
  %8 = zext i8 %7 to i32
  %9 = or i32 0, %8
  %10 = shl i32 %9, 8
  %11 = zext i8 %SymVar_1 to i32
  %12 = or i32 %10, %11
  %13 = zext i8 %7 to i32
  %14 = or i32 0, %13
  %15 = shl i32 %14, 8
  %16 = zext i8 %SymVar_1 to i32
  %17 = or i32 %15, %16
  %18 = lshr i32 %17, 7
  %19 = xor i32 %18, -1
  %20 = add i32 1, %19
  %21 = shl i32 %20, 8
  %22 = add i32 %21, %12
  %23 = add i32 %22, %6
  ret i32 %23
}

[+] EOF LLVM IR ==============================

Utilizzando le ottimizzazioni LLVM siamo riusciti a rimuovere il rumore dall'output devirtualizzato e quindi a rompere l'MBA.
Possiamo vedere l'operazione `XOR` con la sua costante (`%0 = xor i8 %SymVar_0, 92`) e `+ y` (`%6 = add nsw i32 %5, %1`).
Le istruzioni intermedie gestiscono solo il segno. Per riassumere questo esempio, abbiamo completamente devirtualizzato la funzione
`secret` usando lo script `attack_vmp.py` e poi abbiamo completamente rotto l'MBA usando le ottimizzazioni LLVM.

## Esempio 3: Più di un blocco di base

Abbiamo ottenuto risultati molto buoni se la funzione `secret` contiene solo un blocco di base, indipendentemente dalle sue dimensioni. Quindi a questo punto
siamo in grado di devirtualizzare un percorso. Per ricostruire il comportamento dell'intera funzione, dobbiamo devirtualizzare successivamente
i percorsi raggiungibili. Per farlo, dobbiamo eseguire una copertura dei percorsi sui rami dipendenti dall'utente. Alla fine, otteniamo come risultato
un albero dei percorsi che rappresenta i diversi percorsi della funzione originale. L'albero dei percorsi si ottiene introducendo
costruzioni if-then-else da due tracce T1 e T2 con lo stesso prefisso seguite da una condizione C in T1 e un not(C)
in T2. Una volta costruito un albero dei percorsi, possiamo lasciare che LLVM generi un CFG.

<p align="center">
  <img src="https://assets.kitploit.com/production/public/readmes/8096/fc5d1bf9a1544b9b44ef164247f3fc38d04bf45d7c2d7a3c0b21ea3d6636cd39.png">
</p>

Con la protezione software Tigress, i salti virtuali erano implementati con vere istruzioni `jcc` che ci hanno permesso
di identificare rapidamente la condizione di salto. Tuttavia, le cose diventano più complesse quando i salti virtuali sono coinvolti
con VMProtect, poiché non utilizza istruzioni `jcc` per saltare a un altro blocco virtuale. Abbiamo dovuto definire
dei marcatori su una traccia dinamica per individuare la condizione coinvolta in un ramo dipendente dall'utente. Questa è la parte sperimentale
di questo attacco, poiché i marcatori non sono molto precisi, ma hanno funzionato per i nostri campioni.

Ok, consideriamo il seguente esempio:```cpp
int secret(int x, int y) {
  VMProtectBegin("secret");
  int r = 0;
  if (x + y == 1001)
    r = x + 1;
  else
    r = y - 1;
  VMProtectEnd();
  return r;
}

Lo script ci informa che potrebbe esserci un potenziale salto simbolico trovato sul flag `AF` all'indirizzo `0x80d905`. Fornisce inoltre un nuovo modello (usando l'esecuzione simbolica) che dovrebbe prendere l'altro percorso. Quindi generiamo una seconda traccia usando questo modello (se diamo un'occhiata al modello, è corretto rispetto al nostro codice sorgente).```
$ ./pin/pin -t ./pin/source/tools/VMP_Trace/obj-intel64/VMP_Trace.so -start 4198848 -end 4198928 -- ./vmp_binaries/binaries/sample5.vmp.bin 0 1001 &> ./vmp_traces/sample5.vmp.trace.2

A questo punto abbiamo devirtualizzato le due tracce e le abbiamo unite in espressioni `if-then-else`.
Dopo aver sollevato l'espressione in LLVM-IR otteniamo un CFG con solo 480 istruzioni LLVM, il che è
già un buon guadagno rispetto alle migliaia di istruzioni eseguite dalla macchina virtuale.
Ma possiamo fare meglio se utilizziamo le ottimizzazioni di LLVM:```llvm
$ opt -S -O3 ./devirt/sample5.ll
; ModuleID = './devirt/sample5.ll'
source_filename = "tritonModule"

; Function Attrs: mustprogress nofree norecurse nosync nounwind readnone willreturn
define i32 @__triton(i32 %SymVar_0, i32 %SymVar_1) local_unnamed_addr #0 {
entry:
  %0 = add i32 %SymVar_0, 1
  %1 = add i32 %SymVar_1, -1
  %2 = add i32 %SymVar_1, %SymVar_0
  %.not = icmp eq i32 %2, 1001
  %3 = select i1 %.not, i32 %0, i32 %1
  ret i32 %3
}

attributes #0 = { mustprogress nofree norecurse nosync nounwind readnone willreturn }