# アプローチ

我々は、難読化されたトレース T'（難読化されたコード P' からのもの）が、元のコード P の元の命令（元のコード内の T' に対応するトレース T）と、仮想マシン VM の命令を組み合わせたものであり、T' = T + VM(T) となるという重要な直感に依存しています。これらの命令の部分列 T と VM(T) を区別できれば、トレース T' から元のプログラム P の1つのパスを再構築できます。この操作を繰り返して仮想化されたプログラムのすべてのパスを網羅することで、元のプログラム P を再構築できます。私たちの実用的な例では、元のコードは有限数の実行可能パスを持ちます。これは、知的財産保護を伴う多くの状況に当てはまります。そのために、以下の手順を実行します。

1. 仮想化された関数とその引数を特定する
2. ターゲットのVMProtectトレースを生成する
3. VMPトレースをリプレイし、シンボリック式を構築して入力と出力の関係を取得する
4. シンボリック式に最適化を適用して、VMからの命令を可能な限り回避する
5. シンボリック表現をLLVM-IRにリフトして、ターゲットの新しい保護されていないバージョンを構築する

## 例1: 単純なビット演算

最初の例として、次の関数を取り上げます。2つの入力を受け取り、VMProtectによって保護された `x ^ y` を返します。```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` の3種類の操作を使用します。`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) を使用して、トレースの経路述語（path predicate）を構築します。シンボリック変数（関数の入力）を含むすべての式はシンボリックなまま保持され、入力に関係しない式はすべて具体化（concretized）されることに注意してください。言い換えれば、私たちのシンボリック式には、仮想マシンに関連する操作（マシン機構自体はユーザーに依存しない）は一切含まれず、元のプログラムに関連する操作のみが含まれます。

たとえば、以下は具体化の例です。左側には、シンボリック変数を含まない部分式（`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) へのリフターです。
これにより、式を合成すると、次の式が得られます
`(bvxor x y)`。これは大きな成果です。さらに、この式を LLVM-IR にリフトして、新しい非仮想化
バイナリコードをコンパイルできます。

## 例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トレース](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を完全に破りました。

## 例3: 複数の基本ブロック

`secret`関数にサイズに関係なく基本ブロックが1つしか含まれていない場合、非常に良い結果が得られました。つまり、この時点で1つのパスを仮想化解除することができます。関数全体の動作を再構築するには、到達可能なパスを順次仮想化解除する必要があります。そのためには、ユーザー依存の分岐に対してパスカバレッジを実行する必要があります。最終的には、元の関数の異なるパスを表すパスツリーが結果として得られます。パスツリーは、同じプレフィックスを持ち、その後にT1では条件C、T2ではnot(C)が続く2つのトレースT1とT2から、if-then-else構文を導入することで得られます。パスツリーが構築されると、LLVMにCFGを生成させることができます。

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

Tigressソフトウェアプロテクションでは、仮想ジャンプが実際の`jcc`命令で実装されていたため、ジャンプ条件をすばやく特定できました。しかし、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` フラグに潜在的なシンボリックジャンプが見つかる可能性があることを示しています。
また、このスクリプトは（シンボリック実行を使用した）新しいモデルを提供しており、別のパスを取るはずです。それでは、このモデルを使用して
2番目のトレースを生成しましょう（モデルを見てみると、ソースコードに関して正しいことがわかります）。```
$ ./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

このステップでは、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 }