# El enfoque

Nos basamos en la intuición clave de que un trace ofuscado T' (del código ofuscado P') combina instrucciones
originales del código original P (el trace T correspondiente a T' en el código original) e
instrucciones de la máquina virtual VM, de modo que T' = T + VM(T). Si somos capaces de distinguir
entre estas dos subsecuencias de instrucciones T y VM(T), entonces podemos reconstruir una ruta del
programa original P a partir de un trace T'. Repitiendo esta operación para cubrir todas las rutas del
programa virtualizado, podremos reconstruir el programa original P. En nuestro ejemplo práctico, el código
original tiene un número finito de rutas ejecutables, lo cual es común en muchas situaciones que involucran
protección de propiedad intelectual. Para ello, procedemos con los siguientes pasos:

1. Identificar la función virtualizada y sus argumentos
2. Generar un trace de VMProtect del objetivo
3. Reproducir el trace VMP y construir expresiones simbólicas para obtener la relación entre entradas y salida
4. Aplicar optimizaciones en las expresiones simbólicas para evitar en lo posible las instrucciones de la VM
5. Elevar nuestra representación simbólica a LLVM-IR para construir una nueva versión no protegida del objetivo

## Ejemplo 1: Una operación bitwise simple

Tomemos como primer ejemplo la siguiente función: toma dos entradas y devuelve `x ^ y` que está protegida por VMProtect.```cpp
int secret(int x, int y) {
  VMProtectBegin("secret");
  int r = x ^ y;
  VMProtectEnd();
  return r;
}

Puedes ver el resultado [aquí](https://github.com/jonathansalwan/vmprotect-devirtualization/blob/HEAD/vmp_traces/sample2.vmp.trace). El formato de traza utiliza tres tipos de operaciones: `mr`, `r` e `i`.
`mr` es un acceso de lectura de memoria realizado por la instrucción `i`, y `r` son los registros de la CPU. Por ejemplo:```
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 vez que se ha generado la traza VMP, la reproducimos usando el script [attack_vmp.py](https://github.com/jonathansalwan/vmprotect-devirtualization/blob/HEAD/attack_vmp.py). Este script utiliza [Triton](https://github.com/jonathansalwan/Triton) para construir el predicado de ruta de la traza. Nótese que todas las expresiones que involucran variables simbólicas (entradas de la función) se mantienen simbólicas, mientras que todas las expresiones de entrada no relacionadas se concretizan. En otras palabras, nuestras expresiones simbólicas no contienen ninguna operación relacionada con la máquina virtual (el mecanismo en sí mismo no depende del usuario), sino solo operaciones relacionadas con el programa original.

Por ejemplo, a continuación se muestra un ejemplo de concretización. A la izquierda tenemos un AST que contiene subexpresiones que no involucran una variable simbólica (`1 + 2` y `6 ^ 3`). Por lo tanto, estas ramas se concretizan y se reemplazan por las constantes `3` y `5`, lo que conduce al AST de la derecha. **Así es como desvirtualizamos el código.**

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

**Una nota sobre el formula-level backward slicing**: Como es común en la ejecución simbólica, la representación simbólica se calcula primero de manera progresiva a lo largo del camino, luego todas las operaciones lógicas y definiciones que no afectan ni al resultado final ni al camino seguido se eliminan de la expresión simbólica (formula slicing, también conocido como formula pruning). Esto resulta en realizar sobre la fórmula el equivalente de un análisis de código de backward slicing desde la salida del programa. Así, al retorno de la función `secret`, tenemos una expresión de la relación entre las entradas y la salida sin las instrucciones de VMProtect.

El script `./attack_vmp.py` toma como parámetros el archivo de traza y el tamaño de las variables simbólicas. Recuerde, eran `edi` y `esi`, así que tienen 4 bytes de longitud. El resultado del script es el siguiente:```
$ ./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 ==============================

Sin embargo, no logramos recuperar la expresión original que era una simple operación `XOR`. Parece que el `XOR` ha sido traducido a operaciones bitwise. Afortunadamente, recientemente lanzamos nuevas funcionalidades en el proyecto Triton que son un [synthesizer](https://github.com/JonathanSalwan/Triton/issues/1074) y un elevador a [LLVM-IR](https://github.com/JonathanSalwan/Triton/issues/1078). Por lo tanto, podemos sintetizar la expresión lo que nos da la expresión `(bvxor x y)`. Es una buena victoria y ahora podemos ir más allá elevando esta expresión a LLVM-IR y luego compilar un nuevo código binario desvirtualizado.

## Ejemplo 2: Una operación MBA protegida

Bien, ahora echemos un vistazo a otro ejemplo que intenta ocultar una operación MBA. El código fuente original es el siguiente:```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 vez que se genere el [trace de VMP](https://github.com/jonathansalwan/vmprotect-devirtualization/blob/HEAD/vmp_traces/sample3.vmp.trace), ejecutemos el 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 ==============================

Usando optimizaciones de LLVM logramos eliminar el ruido de nuestra salida desvirtualizada y así romper el MBA.
Podemos ver la operación `XOR` con su constante (`%0 = xor i8 %SymVar_0, 92`) y el `+ y` (`%6 = add nsw i32 %5, %1`).
Las instrucciones intermedias solo manejan el signo. Para resumir este ejemplo, desvirtualizamos completamente la función `secret`
usando el script `attack_vmp.py` y luego rompimos completamente el MBA usando optimizaciones de LLVM.

## Ejemplo 3: Más de un bloque básico

Obtuvimos muy buenos resultados si la función `secret` contiene solo un bloque básico independientemente de su tamaño. Así que en este punto
somos capaces de desvirtualizar un camino. Para reconstruir el comportamiento completo de la función, tenemos que desvirtualizar sucesivamente
los caminos alcanzables. Para ello, debemos realizar una cobertura de caminos en ramas dependientes del usuario. Al final, obtenemos como resultado
un árbol de caminos que representa los diferentes caminos de la función original. El árbol de caminos se obtiene introduciendo
una construcción if-then-else a partir de dos trazas T1 y T2 con el mismo prefijo seguidas de una condición C en T1 y un no(C)
en T2. Una vez que se construye un árbol de caminos, podemos dejar que LLVM genere un CFG.

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

Con la protección de software Tigress, los saltos virtuales se implementaron con instrucciones `jcc` reales, lo que nos permitió
identificar rápidamente la condición de salto. Sin embargo, las cosas se vuelven más complejas cuando los saltos virtuales están involucrados
con VMProtect, ya que no utiliza instrucciones `jcc` para saltar a otro bloque virtual. Tuvimos que definir
marcadores en una traza dinámica para detectar la condición involucrada en una rama dependiente del usuario. Esta es la parte experimental
de este ataque, ya que los marcadores no son muy precisos pero funcionaron para nuestras muestras.

Bien, consideremos la siguiente muestra:```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;
}

El script nos dice que puede haber un salto simbólico potencial encontrado en la bandera `AF` en la dirección `0x80d905`.
También proporciona un nuevo modelo (usando ejecución simbólica) que debería tomar el otro camino. Así que generemos una
segunda traza usando este modelo (si observas el modelo, es correcto con respecto a nuestro código fuente).```
$ ./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

En este paso desvirtualizamos las dos trazas y las fusionamos en expresiones `if-then-else`. Después de elevar la expresión a LLVM-IR obtenemos un CFG con solo 480 instrucciones LLVM, lo cual ya es una buena ganancia en comparación con los miles de instrucciones ejecutadas por la máquina virtual. Pero podemos hacerlo mejor si usamos optimizaciones de 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 }