# 접근 방식

우리는 난독화된 트레이스 T'(난독화된 코드 P'로부터)가 원래 코드 P의 명령어(원래 코드에서 T'에 해당하는 트레이스 T)와 가상 머신 VM의 명령어를 결합하여 T' = T + VM(T)와 같다는 핵심 통찰에 의존합니다. 이 두 명령어 하위 시퀀스 T와 VM(T)를 구별할 수 있다면, 트레이스 T'로부터 원래 프로그램 P의 한 경로를 재구성할 수 있습니다. 이 작업을 반복하여 가상화된 프로그램의 모든 경로를 포괄하면 원래 프로그램 P를 재구성할 수 있습니다. 실제 예제에서 원래 코드는 실행 가능한 경로의 유한한 개수를 가지며, 이는 지적 재산권 보호와 관련된 많은 상황에서 해당됩니다. 이를 위해 다음 단계를 수행합니다:

1. 가상화된 함수와 그 인자를 식별합니다.
2. 대상의 VMProtect 트레이스를 생성합니다.
3. VMP 트레이스를 재생하고 심볼릭 표현식을 구성하여 입력과 출력 간의 관계를 얻습니다.
4. 심볼릭 표현식에 최적화를 적용하여 VM의 명령어를 최대한 피합니다.
5. 심볼릭 표현을 LLVM-IR로 리프팅하여 대상의 새로운 보호되지 않은 버전을 구축합니다.

## 예제 1: 간단한 비트 연산

첫 번째 예제로 다음 함수를 살펴보겠습니다: 두 개의 입력을 받아 `x ^ y`를 반환하며, 이는 VMProtect로 보호됩니다.```cpp
int secret(int x, int y) {
  VMProtectBegin("secret");
  int r = x ^ y;
  VMProtectEnd();
  return r;
}

결과는 [여기](https://github.com/jonathansalwan/vmprotect-devirtualization/blob/HEAD/vmp_traces/sample2.vmp.trace)에서 확인할 수 있습니다. 트레이스 형식은 세 가지 종류의 연산을 사용합니다: `mr`, `r`, `i`.
`mr`는 명령어 `i`에 의해 수행된 메모리 읽기 접근이고, `r`은 CPU 레지스터입니다. 예를 들어:```
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

VMP 추적이 생성되면 [attack_vmp.py](https://github.com/jonathansalwan/vmprotect-devirtualization/blob/HEAD/attack_vmp.py) 스크립트를 사용하여 이를 재생합니다. 이 스크립트는 [Triton](https://github.com/jonathansalwan/Triton)을 사용하여 추적의 경로 술어를 구축합니다. 기호 변수(함수의 입력)를 포함하는 모든 표현식은 기호로 유지되며, 입력과 관련 없는 표현식은 구체화됩니다. 즉, 기호 표현식에는 가상 머신(기계 자체는 사용자에 의존하지 않음)과 관련된 연산이 포함되지 않고 원래 프로그램과 관련된 연산만 포함됩니다.

예를 들어, 아래는 구체화의 예입니다. 왼쪽에는 기호 변수를 포함하지 않는 하위 표현식(`1 + 2` 및 `6 ^ 3`)이 포함된 AST가 있습니다. 따라서 이러한 분기는 구체화되어 상수 `3` 및 `5`로 대체되어 오른쪽의 AST가 됩니다. **이것이 코드를 역가상화하는 방법입니다.**

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

**수식 수준 역방향 슬라이싱에 대한 참고 사항**: 기호 실행에서 일반적인 것처럼 기호 표현은 먼저 경로를 따라 순방향으로 계산된 다음, 최종 결과나 따라간 경로에 영향을 미치지 않는 모든 논리 연산 및 정의가 기호 표현식에서 제거됩니다(수식 슬라이싱, 일명 수식 가지치기). 이는 프로그램 출력에서 역방향 슬라이싱 코드 분석과 동등한 작업을 수식에 수행합니다. 따라서 `secret` 함수의 반환 시점에 VMProtect의 명령어 없이 입력과 출력 간의 관계에 대한 표현식을 얻을 수 있습니다.

`./attack_vmp.py` 스크립트는 추적 파일과 기호 변수의 크기를 매개변수로 사용합니다. `edi`와 `esi`였으므로 각각 4바이트 길이입니다. 스크립트의 결과는 다음과 같습니다.```
$ ./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 ==============================

하지만 우리는 간단한 `XOR` 연산이었던 원래 표현식을 복구하지 못했습니다. `XOR`이 비트 연산으로 변환된 것 같습니다. 다행히도, 우리는 최근 Triton 프로젝트에 [합성기(synthesizer)](https://github.com/JonathanSalwan/Triton/issues/1074)와 [LLVM-IR](https://github.com/JonathanSalwan/Triton/issues/1078)로의 리프터(lifter)라는 새로운 기능을 출시했습니다. 따라서 우리는 표현식을 합성하여 `(bvxor x y)` 표현식을 얻을 수 있습니다. 이것은 좋은 성과이며, 이제 이 표현식을 LLVM-IR으로 리프팅한 후 새로운 탈가상화(devirtualized) 바이너리 코드를 컴파일하는 더 나아갈 수 있습니다.


## 예시 2: 보호된 MBA 연산

자, 이제 MBA 연산을 숨기려는 또 다른 예제를 살펴보겠습니다. 원본 소스 코드는 다음과 같습니다:```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;
}

[VMP trace](https://github.com/jonathansalwan/vmprotect-devirtualization/blob/HEAD/vmp_traces/sample3.vmp.trace)가 생성되면, `./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 ==============================

LLVM 최적화를 사용하여 역가상화된 출력에서 노이즈를 제거하고 MBA를 해독할 수 있었습니다.
`XOR` 연산과 해당 상수(`%0 = xor i8 %SymVar_0, 92`) 및 `+ y`(`%6 = add nsw i32 %5, %1`)를 볼 수 있습니다.
그 사이의 명령어는 부호를 처리하는 데만 사용됩니다. 이 예제를 요약하면, `attack_vmp.py` 스크립트를 사용하여 `secret` 함수를 완전히 역가상화한 후 LLVM 최적화를 사용하여 MBA를 완전히 해독했습니다.

## Example 3: More than one basic block

`secret` 함수에 크기에 관계없이 하나의 기본 블록만 포함되어 있으면 매우 좋은 결과를 얻었습니다. 따라서 이 시점에서 하나의 경로를 역가상화할 수 있습니다. 전체 함수 동작을 재구성하려면 도달 가능한 경로를 연속적으로 역가상화해야 합니다. 이를 위해 사용자 종속 분기에 대한 경로 커버리지를 수행해야 합니다. 최종적으로 원래 함수의 여러 경로를 나타내는 경로 트리를 결과로 얻습니다. 경로 트리는 동일한 접두사를 가진 두 개의 트레이스 T1과 T2에서 T1의 조건 C와 T2의 not(C) 다음에 if-then-else 구성을 도입하여 얻습니다. 경로 트리가 구축되면 LLVM이 CFG를 생성하도록 할 수 있습니다.

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

Tigress 소프트웨어 보호 기능에서는 가상 점프가 실제 `jcc` 명령어로 구현되어 점프 조건을 빠르게 식별할 수 있었습니다. 그러나 VMProtect에서는 가상 점프가 포함될 때 상황이 더 복잡해집니다. VMProtect는 다른 가상 블록으로 점프하기 위해 `jcc` 명령어를 사용하지 않기 때문입니다. 사용자 종속 분기에 관련된 조건을 찾기 위해 동적 트레이스에 마커를 정의해야 했습니다. 마커가 정확하지는 않지만 샘플에서 작동했기 때문에 이 공격의 실험적인 부분입니다.

자, 다음 샘플을 고려해 보겠습니다:```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;
}

스크립트는 주소 `0x80d905`의 `AF` 플래그에서 잠재적인 심볼릭 점프가 발견될 수 있다고 알려줍니다. 또한 다른 경로를 취해야 하는 새로운 모델(심볼릭 실행 사용)을 제공합니다. 이 모델을 사용하여 두 번째 트레이스를 생성해 보겠습니다(모델을 살펴보면 소스 코드와 관련하여 올바른 것입니다).```
$ ./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

이 단계에서 우리는 두 트레이스를 가상화 해제하고 이를 `if-then-else` 표현식으로 병합했습니다.
표현식을 LLVM-IR로 리프팅한 후, 우리는 가상 머신이 실행했던 수천 개의 명령어와 비교하여 단 480개의 LLVM 명령어만 있는 CFG를 얻습니다. 이는 이미 좋은 성과입니다.
하지만 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 }