Devirtualization - 1

안상준·2025년 8월 12일

VMProtect

목록 보기

5/6

https://github.com/JonathanSalwan/VMProtect-devirtualization
본 블로그는 위의 깃허브 내용을 정리한 블로그로 VMProtect 3.x 버전으로 보호된 pure function에 대하여 devirtualize 하는 실험을 다룬다.

Introduction

가상화된 함수가 단 하나의 basic block만 포함한 경우 아주 좋은 결과를 보임
basic block이 2개 이상 포함할 경우 매우 실험적이지만, 2개의 basic block을 포함한 sample로 devirtualization, reconstruct 성공

Pure function

실험은 유한한 함수, side effect가 없는 pure function을 대상으로 진행하였다.

x = 4
while x != 0:
	x /= 2

def func() {
	x = 3
    print(x)
}

Approach

가상화 코드의 trace는 원본 코드의 trace + VM명령어(dispatcher, handler)로 구성돼 있다.
원본코드, 가상 머신 관련 명령어를 구분할 수 있다면 가상화 코드의 trace로 부터 원본 코드이 하나의 실행 경로를 재구성 가능하다.

실험 순서
1. 가상화된 함수와 인자를 식별
2. VMProtect trace 생성
3. 입력과 출력 사이의 관계를 나타내는 symbolic expression을 구성
4. VM 관련 명령어는 최대한 피하고 symbolic expression에 최적화를 적용
5. symbolic representation을 LLVM-IR로 lift하기

Example 1: A simple bitwise operation

먼저 간단한 bitwise 연산을 대상으로 devirtualize를 진행하였다.

int secret(int x, in ty) {
	VMProtectBegin("secret");
   	int r = x ^ y;
    VMProtectEnd();
    return r;

위 코드에서 int r = x ^ y 연산만 가상화를 하였고

코드를 분석해 보면 함수의 시작이 4011c0이고 두 개의 argument를 가지며, 함수 리턴 주소는 4011ef인 것을 볼 수 있다.

Pintool

Pintool을 이용하여 가상화가 적용된 부분만 trace를 생성하였다.
실행 명령어는

$ ./pin/pin 
-t ./pin/source/tools/VMP_Trace/obj-intel64/VMP_Trace.so 
-start 4198848 # 시작 주소
-end 4198895 # 끝 주소
-- ./vmp_binaries/binaries/sample2.vmp.bin 1 2 # 인자 전달
&> ./vmp_traces/sample2.vmp.trace # 출력 파일

위와 같이 된다. 시작 주소는 위에서 찾은 함수의 시작과 끝 주소를 decimal로 변경한 것이다.

Log

실행하게 되면

이렇게 trace가 뜨는데 r은 레지스터 값으로

위와 같은 순서로 레지스터 값들이 기록된다.
i는 명령어다.

Symbolic expression

생성된 trace를 attack_vmp.py script를 이용하여 분석한다.

forward symbolic execution : 순방향으로 symbolic expression을 구성
formula slicing / puring : 최종 결과나 실행 경로에 영향을 주지 않는 모든 연산과 정의를 수식에서 제거
backward slicing : symbolic expression에서 불필요한 요소들을 제거

이를 통해 입력과 출력 사이의 관계만 남은 expression을 갖게 되고, VMProtect 명령어는 제거되어 존재하지 않는다.

Result

Triton을 이용하여 LLVM-IR로 lift한 결과다. IR을 보면 %SymVar_0, %SymVar_1 두 값을 xor 하고, 결과를 리턴하는 것을 볼 수 있다.

Example 2 : A MBA operation protected

이번에는 MBA(Mixed Bitwise Arithmetic)연산을 devirtualize하는 실험을 진행하였다.

원본 코드다. 아까와 같은 과정을 거쳐 함수의 시작과 끝의 trace를 구하고, Triton을 통해 LLVM-IR로 lift한다.

Result

결과를 보면 무척이나 긴 것을 볼 수 있다. 이를 -opt를 이용하여 최적화를 해주면

최종적으로 위와 같은 IR을 얻을 수 있다.

Example 3 : More than one basic block

함수 전체를 복원하려면, 도달 가능한 모든 실행 경로들을 devirtualize 해야 한다. 사용자 입력에 따라 달라지는 분기문에 대한 경로 커버리지를 수행해야 한다. path tree를 구축하면, LLVM을 이용해 이를 CFG로 생성한다.

코드는 위와 같은 코드를 사용하였다.

Marker

Tigres는 jcc(jne, je, jg, ...)와 같은 진짜 조건 분기 명령어를 사용하여 분석하기 쉽다. 하지만 VMProtect는 내부적으로 간접분기 + 핸들러 체인 방식을 사용하기 때문에 분석하기 어렵다. 이를 해결하기 위해 동적 분석중에 분기가 발생하는 시점을 추적하기 위해 marker를 사용하였다.

False branch

먼저 pin을 이용하여 else로 가는 trace를 추출한다.

$./pin/pin -t
./pin/source/tools/VMP_Trace/obj-intel64/VMP_Trace.so
-start 4198848 -end 4198928 -- 
./vmp_binaries/binaries/sample5.vmp.bin 1 2
&> ./vmp_traces/sample5.vmp.trace.1

인자로 1과 2를 보내 else로 가도록 하였고 이렇게 trace를 생성하여 IR로 lift한 결과

위와 같이 나오게 된다. Triton 모델에서 symbolic jump를 발견 하였고, argument를 0과 3e9(1001)로 할 것을 제안한다. 이는 true table 분석을 위한 것이다.

True branch

이번에는 true로 가는 trace를 생성해 보았다.

$./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.1

trace를 이용하여 IR로 lift한 결과

위와 같이 나오고 최적화를 적용하면

최종적으로 이렇게 나온다. false와 다르게 결과가 매우 긴 것을 볼 수 있는데 이는 Triton 내부에서 True인 경우에는 조건문 까지 같이 해석하기 때문에 그렇다.