Breaking State-of-the-Art Binary Code Obfuscation via Program Synthesis
Black Hat Asia, Singapore
March 22, 2018

Tim Blazytko, @mr_phrazer

Moritz Contag, @dwuid

http://synthesis.tohttps://dwuid.com
Chair for Systems Security
Ruhr-Universität Bochum<firstname.lastname>@rub.deSetting the SceneObfuscated code, semantics?

 Traditional deobfuscation techniques

Orthogonal approach2

Motivation
Prevent Complicate reverse engineering attempts.
• Intellectual Property• Malicious Payloads• Digital Rights Management

3Motivation
Prevent Complicate reverse engineering attempts.
• Intellectual Property• Malicious Payloads• Digital Rights Management“We achieved our goals. We were uncracked for 13 whole days.”– Martin Slater, 2K Australia, on BioShock (2007).

3

How to protect software?

Approaches

Abuse shortcomings of ﬁle parsers and other tools of the trade.
• fld tbyte ptr [__bad_values] crashing OllyDbg 1.10.
• Fake SizeOfImage crashing process dumpers.

5Approaches

Abuse shortcomings of ﬁle parsers and other tools of the trade.
• fld tbyte ptr [__bad_values] crashing OllyDbg 1.10.
• Fake SizeOfImage crashing process dumpers.

Detect artifacts of the debugging process.
• PEB.BeingDebugged bit being set.
• int 2D and exception handling in debuggers.

5Approaches
Abuse shortcomings of ﬁle parsers and other tools of the trade.
• fld tbyte ptr [__bad_values] crashing OllyDbg 1.10.
• Fake SizeOfImage crashing process dumpers.

Detect artifacts of the debugging process.
• PEB.BeingDebugged bit being set.
• int 2D and exception handling in debuggers.

5Requirements

1. We want the technique to be semantics-preserving.

Preserve the observable behavior of the application.

6

Requirements

1. We want the technique to be semantics-preserving.
2. We want to avoid external dependencies, focus on code only.

Assume white-box attack scenario.

6Requirements

1. We want the technique to be semantics-preserving.
2. We want to avoid external dependencies, focus on code only.
3. We want techniques where effort(deploy) ≪ effort(attack).

Anti-Debugging tricks are effort 1:1.

6

Code Obfuscation Techniques
Opaque Predicates

t f

A

B

A

ß

t
B

C
t
C

f
C'

f

Opaque Predicatestrue

call GetCurrentProcess
cmp eax, 0xffffffffje__block_a__block_a: …
…

false

__block_b: …
…

9

Opaque Predicatesalways taken

call GetCurrentProcess
cmp eax, 0xffffffffje__block_a__block_a: …
…

never taken

dead code 💀

Opaque True Predicate
9Opaque Predicatesalways taken

call GetCurrentProcess
cmp eax, 0xffffffffje__block_a__block_a: …
…

⟵ opaque predicate
never taken

dead code 💀

Opaque True Predicate
9Opaque Predicatesalways taken

call GetCurrentProcess
cmp eax, 0xffffffffje__block_a__block_a: …
…

⟵ opaque value
never taken

dead code 💀

Opaque True Predicate
9Opaque Predicatesalways taken

mov
cmp
je

__block_a: …
…

eax, 0xffffffff
eax, 0xffffffff__block_anever taken

dead code 💀

Opaque True Predicate
9Opaque Predicatesnever taken

mov
cmp
je

dead code 💀

eax, 0xffffffff
eax, 0xdeadbeef__block_a

always taken__block_b: …
…

Opaque False Predicate
9Opaque Predicatestrue

call rand
cmp eax, 0xdeadbeef
je__block_afalse

semanticallyequivalent__block_a: …
…

≡__block_a': …
…

Random Opaque Predicate
duplicated block9Opaque Predicates⊕ Increase in complexity (branch count, McCabe)⊕ Can be built on hard problems (e. g., aliasing)

B Examples– GetCurrentProcess() ⇒ −1
– fldpi1 ⇒ st(0) = π⊕ Forces analyst to encode additional knowledge– x2 ≥ 0 ∀x

⊕ Hard to solve statically– x + 1 ̸= x ∀x
– pointer A must-alias pointer B– checksum(code) = 0x1c43b5cf

10

Opaque Predicates⊕ Increase in complexity (branch count, McCabe)⊕ Can be built on hard problems (e. g., aliasing)

B Examples– GetCurrentProcess() ⇒ −1
– fldpi1 ⇒ st(0) = π⊕ Forces analyst to encode additional knowledge– x2 ≥ 0 ∀x

⊕ Hard to solve statically– x + 1 ̸= x ∀x
– pointer A must-alias pointer B⊖ Solved for free using concrete execution traces– checksum(code) = 0x1c43b5cf

10

Code Obfuscation Techniques
Virtual MachinesVirtual Machines

mov ecx, [esp+4]
xor eax, eax
mov ebx, 1__secret_ip:
mov edx, eax
add edx, ebx
mov eax, ebx
mov ebx, edx
loop __secret_ip
mov eax, ebx
ret

12Virtual Machines

mov ecx, [esp+4]
xor eax, eax
mov ebx, 1__secret_ip:
mov edx, eax
add edx, ebx
mov eax, ebx
mov ebx, edx
loop __secret_ip
mov eax, ebx
ret

12Virtual Machines

mov ecx, [esp+4]
xor eax, eax
mov ebx, 1__secret_ip:
mov edx, eax
add edx, ebx
mov eax, ebx
mov ebx, edx
loop __secret_ip
mov eax, ebx
ret

12Virtual Machines

mov ecx, [esp+4]
xor eax, eax
mov ebx, 1__secret_ip:
mov edx, eax
add edx, ebx
mov eax, ebx
mov ebx, edx
loop __secret_ip

made-up instruction set➟__bytecode:
vld r0vpop r1
vld r2
vld r1
vadd r1
vld r2
vpop r0

vld r1
vpop r2
vldi #1
vld r3vsub r3
vld #0veq r3vbr0 #-0E

mov eax, ebx
ret

12Virtual Machines

mov ecx, [esp+4]
xor eax, eax
mov ebx, 1__secret_ip:
push __bytecodecall vm_entry

made-up instruction set➟__bytecode:
db 54 68 69 73 20 64 6f
db 65 73 6e 27 74 20 6c
db 6f 6f 6b 20 6c 69 6b
db 65 20 61 6e 79 74 68
db 69 6e 67 20 74 6f 20
db 6d 65 2e de ad be ef

mov eax, ebx
ret

12Virtual Machines

mov ecx, [esp+4]
xor eax, eax
mov ebx, 1__secret_ip:
push __bytecodecall vm_entry

made-up instruction set➟__bytecode:
db 54 68 69 73 20 64 6f
db 65 73 6e 27 74 20 6c
db 6f 6f 6b 20 6c 69 6b
db 65 20 61 6e 79 74 68
db 69 6e 67 20 74 6f 20
db 6d 65 2e de ad be ef?

mov eax, ebx
ret

12Virtual Machines
Core Components
VM Entry/Exit

Context Switch: native context ⇔ virtual context

VM Dispatcher

Fetch–Decode–Execute loop

Handler Table

Individual VM ISA instruction semantics• Entry

Copy native context (registers, ﬂags) to VM context.

• ExitCopy VM context back to native context.

• Mapping from native to virtual registers is often 1:1.

13

Virtual Machines
Core Components
VM Entry/Exit

Context Switch: native context ⇔ virtual context

VM Dispatcher

Fetch–Decode–Execute loop

Handler Table

Individual VM ISA instruction semantics

1. Fetch and decode instruction
2. Forward virtual instruction pointer3. Look up handler for opcode in handler table
4. Invoke handler

FDE

look uphandle_vpush
handle_vpush
handle_vadd
handle_vadd
handle_vxor
handle_vxor
handle_vexit
handle_vexit
handle_vpop
handle_vpop…

13Virtual Machines
Core Components
VM Entry/Exit

Context Switch: native context ⇔ virtual context

VM Dispatcher

Fetch–Decode–Execute loop

Handler Table

Individual VM ISA instruction semantics• Table of function pointers indexed by opcode• One handler per virtual instruction• Each handler decodes operands andupdates VM context

FDE

look uphandle_vpush
handle_vpush
handle_vadd
handle_vadd
handle_vxor
handle_vxor
handle_vexit
handle_vexit
handle_vpop
handle_vpop…

13Virtual Machines14

Virtual Machines

handle_vpush
handle_vpush
handle_vadd
handle_vadd
handle_vxor
handle_vxor
handle_vexit
handle_vexit
handle_vpop
handle_vpop…

look up
FDE}}

VM Entry
VM Dispatcher (FDE)

Individual Handlers

VM Exit(as handler)

14

Virtual Machines__vm_dispatcher:mov
bl, [rsi]
inc
rsi
movzx rax, bljmp__handler_table[rax * 8]

VM Dispatcher

rsi – virtual instruction pointerrbp – VM context
15

Virtual Machines__vm_dispatcher:mov
bl, [rsi]
inc
rsi
movzx rax, bljmp__handler_table[rax * 8]

VM Dispatcher

rsi – virtual instruction pointerrbp – VM context__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)
15

Virtual Machine HardeningVirtual Machines

Hardening Technique #1 – Obfuscating individual VM components.

• Handlers are conceptually simple.

17

Virtual Machines

Hardening Technique #1 – Obfuscating individual VM components.

• Handlers are conceptually simple.
• Apply traditional code obfuscation transformations:• Substitution (mov rax, rbx ß push rbx; pop rax)
• Opaque Predicates• Junk Code• …

mov eax, dword [rbp]mov ecx, dword [rbp+4]
cmp r11w, r13w
sub rbp, 4
not eaxclc
cmc
cmp rdx, 0x28b105fa
not ecx
cmp r12b, r9b17Virtual Machines

Hardening Technique #2 – Duplicating VM handlers.

• Handler table is typically indexed using one byte (= 256 entries).

18

Virtual Machines

Hardening Technique #2 – Duplicating VM handlers.

• Handler table is typically indexed using one byte (= 256 entries).
• Idea: Duplicate existing handlers to populate full table.
• Use traditional obfuscation techniques to impede code similarity analyses.

Goal: Increase workload of reverse engineer.

18

handle_vpush
handle_vadd
handle_vnor
handle_vpop

handle_vpush
handle_vadd

handle_vpush
handle_vadd
handle_vnor
handle_vpop➟

handle_vnor''handle_vpop
handle_vadd'
handle_vnor
handle_vnor'
handle_vadd''

Virtual Machines

Hardening Technique #3 – No central VM dispatcher.

• A central VM dispatcher allows attacker to easily observe VM execution.
• Idea: Instead of branching to the central dispatcher, inline it into each handler.

Goal: No “single point of failure”.
(Themida, VMProtect Demo)

20

FDE

handle_vnor

handle_…

handle_vnor

handle_…

FDE

FDE

Virtual Machines

Hardening Technique #4 – No explicit handler table.
• An explicit handler table easily reveals all VM handlers.

23

Virtual Machines

Hardening Technique #4 – No explicit handler table.
• An explicit handler table easily reveals all VM handlers.
• Idea:Instead of querying an explicit handler table,
encode the next handler address in the VM instruction itself.

Goal: Hide location of handlers that have not been executed yet.
(VMProtect Full, SolidShield)

23

Virtual Machines

Hardening Technique #4 – No explicit handler table.
• An explicit handler table easily reveals all VM handlers.
• Idea:Instead of querying an explicit handler table,
op 1
op 0
opcodeencode the next handler address in the VM instruction itself.

Goal: Hide location of handlers that have not been executed yet.
(VMProtect Full, SolidShield)

23

Virtual Machines

Hardening Technique #4 – No explicit handler table.
• An explicit handler table easily reveals all VM handlers.
• Idea:Instead of querying an explicit handler table,
op 1
op 0
opcodenext handler addr
encode the next handler address in the VM instruction itself.

Goal: Hide location of handlers that have not been executed yet.
(VMProtect Full, SolidShield)

23

Virtual Machines

Hardening Technique #5 – Blinding VM bytecode.
• Global analyses on the bytecode possible, easy to patch instructions.

25

Virtual Machines

Hardening Technique #5 – Blinding VM bytecode.
• Global analyses on the bytecode possible, easy to patch instructions.
• Idea:• Flow-sensitive instruction decoding (“decryption” based on key register).
• Custom decryption routine per handler, diversiﬁcation.
• Patching requires re-encryption of subsequent bytecode.

Goal: Hinder global analyses of bytecode and patching.
25

operand← [vIP + 0]

context← semantics(context, operand)

next_handler← [vIP + 4]vIP ← vIP + 8
jmp next_handler
26

operand← [vIP + 0]

 operand← unmangle(operand, key)

 key

← unmangle′ (key, operand)

context← semantics(context, operand)

next_handler← [vIP + 4]

 next_handler← unmangle′′ (next_handler, key)

 key

← unmangle′′′ (key, next_handler)vIP ← vIP + 8
jmp next_handler
26

Code Obfuscation Techniques
Mixed Boolean-Arithmetic

Mixed Boolean-Arithmetic

What does this expression compute?

(x ⊕ y) + 2 · (x ∧ y)28

Mixed Boolean-Arithmetic

What does this expression compute?

(x ⊕ y) + 2 · (x ∧ y)
=x+y

28

Mixed Boolean-Arithmetic

What does this expression compute?

(((x ⊕ y) + ((x ∧ y) ≪ 1)) ∨ z) + (((x ⊕ y) + ((x ∧ y) ≪ 1)) ∧ z)28

Mixed Boolean-Arithmetic

What does this expression compute?

(((x ⊕ y) + ((x ∧ y) ≪ 1)) ∨ z) + (((x ⊕ y) + ((x ∧ y) ≪ 1)) ∧ z)
=x+y+z• Boolean identities?
• Arithmetic identities?
• Karnaugh-Veitch maps?

A·0=0
A+B=A·B2

x − y2 = (x + y)(x − y)28Mixed Boolean-Arithmetic

Boolean-arithmetic algebra BA[n](Bn , ∧, ∨, ⊕, ¬, ≤, ≥, >, <, ≤s , ≥s , >s , <s , ̸=, =, ≫s , ≫, ≪, +, −, ·)is a Boolean-arithmetic algebra BA[n], for n > 0, B = {0, 1}.

BA[n] includes, amongst others, both:• Boolean algebra(Bn , ∧, ∨, ¬),• Integer modular ringZ/(2n ).

No techniques to simplify
such expressions easily!

29

Deobfuscation

Symbolic Execution__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)

Symbolic Execution__handle_vnor:• mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)

rcx ← [rbp]Symbolic Execution__handle_vnor:
mov rcx, [rbp]• mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)

rcx ← [rbp]rbx ← [rbp + 4]

Symbolic Execution__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
• not rcx
not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)

rcx ← [rbp]rbx ← [rbp + 4]
rcx ← ¬ rcx = ¬ [rbp]Symbolic Execution__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx• not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)

rcx ← [rbp]rbx ← [rbp + 4]

rcx ← ¬ rcx = ¬ [rbp]rbx ← ¬ rbx = ¬ [rbp + 4]

Symbolic Execution__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx• and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)

rcx ← [rbp]rbx ← [rbp + 4]
rcx ← ¬ rcx = ¬ [rbp]rbx ← ¬ rbx = ¬ [rbp + 4]

rcx ← rcx ∧ rbx= (¬ [rbp]) ∧ (¬ [rbp + 4])

Symbolic Execution__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx• and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)

rcx ← [rbp]rbx ← [rbp + 4]
rcx ← ¬ rcx = ¬ [rbp]rbx ← ¬ rbx = ¬ [rbp + 4]
rcx ← rcx ∧ rbx= (¬ [rbp]) ∧ (¬ [rbp + 4])= [rbp] ↓ [rbp + 4]

Symbolic Execution__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx• mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)

rcx ← [rbp]rbx ← [rbp + 4]
rcx ← ¬ rcx = ¬ [rbp]rbx ← ¬ rbx = ¬ [rbp + 4]
rcx ← rcx ∧ rbx= (¬ [rbp]) ∧ (¬ [rbp + 4])= [rbp] ↓ [rbp + 4]
[rbp + 4] ← rcx = [rbp] ↓ [rbp + 4]

31

Symbolic Execution__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx
mov [rbp + 4], rcx• pushf
pop [rbp]
jmp __vm_dispatcher

rcx ← [rbp]rbx ← [rbp + 4]
rcx ← ¬ rcx = ¬ [rbp]rbx ← ¬ rbx = ¬ [rbp + 4]
rcx ← rcx ∧ rbx= (¬ [rbp]) ∧ (¬ [rbp + 4])= [rbp] ↓ [rbp + 4]
[rbp + 4] ← rcx = [rbp] ↓ [rbp + 4]
rsp ← rsp − 4[rsp] ← flags

Handler performing nor(with ﬂag side-effects)

31Symbolic Execution__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf• pop [rbp]jmp __vm_dispatcher

rcx ← [rbp]rbx ← [rbp + 4]
rcx ← ¬ rcx = ¬ [rbp]rbx ← ¬ rbx = ¬ [rbp + 4]
rcx ← rcx ∧ rbx= (¬ [rbp]) ∧ (¬ [rbp + 4])= [rbp] ↓ [rbp + 4]
[rbp + 4] ← rcx = [rbp] ↓ [rbp + 4]
rsp ← rsp − 4[rsp] ← flags

Handler performing nor(with ﬂag side-effects)[rbp] ← [rsp] = flags
rsp ← rsp + 4
31

Symbolic Execution__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]• jmp __vm_dispatcher

rcx ← [rbp]rbx ← [rbp + 4]
rcx ← ¬ rcx = ¬ [rbp]rbx ← ¬ rbx = ¬ [rbp + 4]
rcx ← rcx ∧ rbx[rbp + 4] ← ([rbp] ↓ [rbp + 4])= (¬ [rbp]) ∧ (¬ [rbp + 4])= [rbp] ↓ [rbp + 4]

[rbp + 4] ← rcx = [rbp] ↓ [rbp + 4]
rsp ← rsp − 4[rsp] ← flags

Handler performing nor(with ﬂag side-effects)[rbp] ← [rsp] = flags
rsp ← rsp + 4
31Virtual Machine Handlermoveax, dword [rbp]movecx, dword [rbp + 4]cmp
r11w, r13w
subrbp, 4
not
eax
clc
cmc
cmp
rdx, 0x28b105fa
not
ecx
cmp
r12b, r9bcmc
andeax, ecx
jmp
0xc239
movword [rbp + 8], eax
pushfqmovzx eax, r10w
andax, dipop
qword [rbp]subrsi, 4shld
rax, rdx, 0x1b
xor
ah, 0x4d
mov
eax, dword [rsi]cmpecx, r11d
test
r10, 0x179708d5
xor
eax, ebx

jmp
0xfffffffffff63380
dec
eax
stc
ror
eax, 1
jmp
0xffffffffffff2a70
dec
eax
clc
bswap eax
test
bp, 0x5124
neg
eax
test
dil, 0xe9
cmpbx, r14w
cmc
push
rbx
sub
bx, 0x49f8
xor
dword [rsp], eax
andbh, 0xaf
pop
rbx
movsxd rax, eax
test
r13b, 0x94
add
rdi, rax
jmp
0xfffffffffffc67c7
learax, [rsp + 0x140]
cmp
rbp, raxja
0x6557bjmp
rdiVirtual Machine Handler

IRDst = ((- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32})[31:32]?((RDI_init+{(- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32}) 0 32, 0xFFFFFFFF 32 64}),(RDI_init+{(- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init
pf = parity(((RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)&0xFF))[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32}) 0 32, 0x0 32 64})))
cf = ((((RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)^(RBP_init+0xFFFFFFFFFFFFFFFC))&((RBP_init+0xFFFFFFFFFFFFFFFC)^(RSP_init+0x140)))^(RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)^(RBP_init+0xFFFFFFFFFFFFFFFC)^(RSP_init+0x140))[63:64]
af =@64[(RBP_init+0xFFFFFFFFFFFFFFFC)] = (((@32[RBP_init]^0xFFFFFFFF)&(@32[(RBP_init+0x4)]^0xFFFFFFFF))?({0x2 0 2, parity(((@32((RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)^(RBP_init+0xFFFFFFFFFFFFFFFC)^(RSP_init+0x140))[4:5][RBP_init]^0xFFFFFFFF)&(@32[(RBP_init+0x4)]^0xFFFFFFFF)&0xFF)) 2 3, 0x0 3 4, (((- R9_init[0:8])+R12_init[0:8])^R12_init[0:8]^R9_init[0:8])[4:5] 4 5, 0x0 5 7, ((@32[RBP_init]^0xFFFFFFFF)&(@32[(RBP_init+0x4)]^0xFFFFFFFF))[31:32] 7 8, tf_init 8 9, i_f_init
9 10, df_init 10 11, 0x0 11 12, iopl_f_init 12 14, nt_init 14 15, 0x0 15 16, rf_init 16 17, vm_init 17 18, ac_init 18 19, vif_init 19 20, vip_init 20 21, i_d_init 21 22, 0x0 22 64},{0x2 0 2, parity(((@32[RBP_init]^0xFFFFFFFF)&(@32[(RBP_init+0x4)]^0xFFFFFFFF)&0xFF)) 2 3, 0x0 3 4, (((- R9_init[0:8])+R12_init[0:8])^R12_init[0:8]^R9_init[0:8])[4:5] 4 5, 0x2 5 7, ((@32[RBP_init]^0xFFFFFFFF)&(@32[(RBP_init+0x4)]^0xFFFFFFFF))[31:32] 7 8, tf_init 8 9, i_f_init 9 10, df_init 10 11, 0x0 11 12,
RAX = (RSP_init+0x140)
of = (((RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)^(RBP_init
iopl_f_init 12 14, nt_init 14 15, 0x0 15 16, rf_init 16 17, vm_init 17 18, ac_init 18 19, vif_init 19 20, vip_init 20 21, i_d_init 21 22, 0x0 22 64}))
RCX = {(@32[(RBP_init+0x4)]^0xFFFFFFFF) 0 32, 0x0 32 64}@32[(RBP_init+0x4)] = ((@32[RBP_init]^0xFFFFFFFF)&(@32[(RBP_init+0x4)]^0xFFFFFFFF))
RBX =+0xFFFFFFFFFFFFFFFC))&((RBP_init+0xFFFFFFFFFFFFFFFC)^(RSP_init+0x140)))[63:64]{((- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init
RBP =+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32})^RBX_init[0:32]) 0 32, RBX_init[32:64] 32 64}
zf = ((RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)?(0x0,0x1))
RSI = (RSI_init+0xFFFFFFFFFFFFFFFC)
RDI = ((- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0(RBP_init+0xFFFFFFFFFFFFFFFC)
8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32})[31:32]?((RDI_init+{(- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32}) 0 32, 0xFFFFFFFF 32 64}),(RDI_init+{(- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init
nf = (RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)[63:64]@32[(RSP_init+0xFFFFFFFFFFFFFFF8)] = ((- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32}) 0 32, 0x0 32 64})))+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)@32[(RSP_init+0xFFFFFFFFFFFFFFFC)] = RBX_init[32:64][8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32})^RBX_init[0:32])

Virtual Machine Handler

IRDst = ((- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32})[31:32]?((RDI_init+{(- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32}) 0 32, 0xFFFFFFFF 32 64}),(RDI_init+{(- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init
pf = parity(((RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)&0xFF))[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32}) 0 32, 0x0 32 64})))
cf = ((((RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)^(RBP_init+0xFFFFFFFFFFFFFFFC))&((RBP_init+0xFFFFFFFFFFFFFFFC)^(RSP_init+0x140)))^(RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)^(RBP_init+0xFFFFFFFFFFFFFFFC)^(RSP_init+0x140))[63:64]
af =@64[(RBP_init+0xFFFFFFFFFFFFFFFC)] = (((@32[RBP_init]^0xFFFFFFFF)&(@32[(RBP_init+0x4)]^0xFFFFFFFF))?({0x2 0 2, parity(((@32((RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)^(RBP_init+0xFFFFFFFFFFFFFFFC)^(RSP_init+0x140))[4:5][RBP_init]^0xFFFFFFFF)&(@32[(RBP_init+0x4)]^0xFFFFFFFF)&0xFF)) 2 3, 0x0 3 4, (((- R9_init[0:8])+R12_init[0:8])^R12_init[0:8]^R9_init[0:8])[4:5] 4 5, 0x0 5 7, ((@32[RBP_init]^0xFFFFFFFF)&(@32[(RBP_init+0x4)]^0xFFFFFFFF))[31:32] 7 8, tf_init 8 9, i_f_init
9 10, df_init 10 11, 0x0 11 12, iopl_f_init 12 14, nt_init 14 15, 0x0 15 16, rf_init 16 17, vm_init 17 18, ac_init 18 19, vif_init 19 20, vip_init 20 21, i_d_init 21 22, 0x0 22 64},{0x2 0 2, parity(((@32[RBP_init]^0xFFFFFFFF)&(@32[(RBP_init+0x4)]^0xFFFFFFFF)&0xFF)) 2 3, 0x0 3 4, (((- R9_init[0:8])+R12_init[0:8])^R12_init[0:8]^R9_init[0:8])[4:5] 4 5, 0x2 5 7, ((@32[RBP_init]^0xFFFFFFFF)&(@32[(RBP_init+0x4)]^0xFFFFFFFF))[31:32] 7 8, tf_init 8 9, i_f_init 9 10, df_init 10 11, 0x0 11 12,
RAX = (RSP_init+0x140)
of = (((RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)^(RBP_init
iopl_f_init 12 14, nt_init 14 15, 0x0 15 16, rf_init 16 17, vm_init 17 18, ac_init 18 19, vif_init 19 20, vip_init 20 21, i_d_init 21 22, 0x0 22 64}))
RCX = {(@32[(RBP_init+0x4)]^0xFFFFFFFF) 0 32, 0x0 32 64}@32[(RBP_init+0x4)] = ((@32[RBP_init]^0xFFFFFFFF)&(@32[(RBP_init+0x4)]^0xFFFFFFFF))
RBX =+0xFFFFFFFFFFFFFFFC))&((RBP_init+0xFFFFFFFFFFFFFFFC)^(RSP_init+0x140)))[63:64]{((- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init
RBP =+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32})^RBX_init[0:32]) 0 32, RBX_init[32:64] 32 64}
zf = ((RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)?(0x0,0x1))
RSI = (RSI_init+0xFFFFFFFFFFFFFFFC)
RDI = ((- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0(RBP_init+0xFFFFFFFFFFFFFFFC)
8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32})[31:32]?((RDI_init+{(- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32}) 0 32, 0xFFFFFFFF 32 64}),(RDI_init+{(- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init
nf = (RBP_init+(- RSP_init)+0xFFFFFFFFFFFFFEBC)[63:64]@32[(RSP_init+0xFFFFFFFFFFFFFFF8)] = ((- {((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32}) 0 32, 0x0 32 64})))+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[24:32] 0 8, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[16:24] 8 16, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)@32[(RSP_init+0xFFFFFFFFFFFFFFFC)] = RBX_init[32:64][8:16] 16 24, ((((@32[(RSI_init+0xFFFFFFFFFFFFFFFC)]^RBX_init[0:32])+0xFFFFFFFF) >>> 0x1)+0xFFFFFFFF)[0:8] 24 32})^RBX_init[0:32])

M1 = (¬M1) ∧ (¬M2)

Mixed Boolean-Arithmetic Expression

int mixed_boolean(int A, int B, int C) {int result;result = (((1438524315 + ((((1438524315 + C) + 1438524315 * ((2956783114 - -1478456685 * C) |(-1478456685 * (1668620215 - A) - 2956783115))) + A) - 1553572265)) + 1438524315 * ((2956783114 -1478456685 * ((((1438524315 + C) + 1438524315 * ((2956783114 - -1478456685 * C) | (-1478456685 *(1668620215 - A) - 2956783115))) + A) - 1553572265)) | (-1478456685 * (1668620215 - B) 2956783115))) - ((1438524315 + (1668620215 - ((((1438524315 + C) + 1438524315 * ((2956783114 -1478456685 * C) | (-1478456685 * (1668620215 - A) - 2956783115))) + A) - 1553572265))) +1438524315 * ((2956783114 - -1478456685 * (1668620215 - ((((1438524315 + C) + 1438524315 *((2956783114 - -1478456685 * C) | (-1478456685 * (1668620215 - A) - 2956783115))) + A) 1553572265))) | (-1478456685 * B - 2956783115)))) + 1553572265;
return -1478456685 * result - 2956783115;}

Mixed Boolean-Arithmetic Expression
RAX = {((((- ((((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+(@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+((((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A))[31:32]?(({(((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32,
0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32,
0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32,
0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A)) 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({(((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32,
0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32,
0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A)) 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0xB9334352)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+(@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+((((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32,
0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A))[31:32]?(({(((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A)) 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({(((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?
(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32,
0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A)) 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0xB9334352) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+(@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 3264}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+((((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A))[31:32]?(({(((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32,
0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A)) 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({(((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),

Mixed Boolean-Arithmetic Expression
RAX = {((((- ((((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+(@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+((((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A))[31:32]?(({(((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32,
0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32,
0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32,
0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A)) 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({(((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32,
0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32,
0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A)) 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0xB9334352)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+(@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+((((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32,
0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A))[31:32]?(({(((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A)) 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({(((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?
(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32,
0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A)) 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0xB9334352) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+(@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 3264}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+((((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A))[31:32]?(({(((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0xFFFFFFFFA7E08A93),({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32,
0x0 32 64}*0xFFFFFFFFA7E08A93)))[0:32])+0xB03CEE0A)|((((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0xFFFFFFFF 32 64}*0x581F756D),({((@32[(RBP_init+0xFFFFFFFFFFFFFFFC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFFC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9) 0 32, 0x0 32 64}*0x581F756D)))[0:32]+0xB03CEE0A)) 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({(((- (((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0x0 32 64}*0x55BE239B)))[0:32]+0x5C99A1A9)[31:32]?(({((@32[(RBP_init+0xFFFFFFFFFFFFFFEC)][31:32]?(({@32[(RBP_init+0xFFFFFFFFFFFFFFEC)] 0 32, 0xFFFFFFFF 32 64}*0x55BE239B),

RAX = (M4 | M0) – M2

Symbolic Execution⊕ Captures full semantics of executed code
⊕ Computer algebra system, some degree of simpliﬁcation⊖ Usability decreases with increasing syntactic complexity• Artiﬁcial complexity (substitution, …)• Algebraic complexity (MBA)34

Symbolic Execution⊕ Captures full semantics of executed code
⊕ Computer algebra system, some degree of simpliﬁcation⊖ Usability decreases with increasing syntactic complexity• Artiﬁcial complexity (substitution, …)• Algebraic complexity (MBA)What if we could reason about semantics only instead of syntax?

34

Program Synthesis

Program Synthesis: A Semantic Approach
We use f as a black-box:
f(x, y, z) := (((x ⊕ y) + ((x ∧ y) · 2)) ∨ z) + (((x ⊕ y) + ((x ∧ y) · 2)) ∧ z)36

Program Synthesis: A Semantic Approach
We use f as a black-box:
f(x, y, z) := (((x ⊕ y) + ((x ∧ y) · 2)) ∨ z) + (((x ⊕ y) + ((x ∧ y) · 2)) ∧ z)

(1,1,1)?

3

36

Program Synthesis: A Semantic Approach
We use f as a black-box:
f(x, y, z) := (((x ⊕ y) + ((x ∧ y) · 2)) ∨ z) + (((x ⊕ y) + ((x ∧ y) · 2)) ∧ z)

(1,1,1)?

(1, 1, 1) → 3

336

Program Synthesis: A Semantic Approach
We use f as a black-box:
f(x, y, z) := (((x ⊕ y) + ((x ∧ y) · 2)) ∨ z) + (((x ⊕ y) + ((x ∧ y) · 2)) ∧ z)

(2,3,1)?

(1, 1, 1) → 3

636

Program Synthesis: A Semantic Approach
We use f as a black-box:
f(x, y, z) := (((x ⊕ y) + ((x ∧ y) · 2)) ∨ z) + (((x ⊕ y) + ((x ∧ y) · 2)) ∧ z)

(2,3,1)?

(1, 1, 1) → 3

6(2, 3, 1) → 6

36

Program Synthesis: A Semantic Approach
We use f as a black-box:
f(x, y, z) := (((x ⊕ y) + ((x ∧ y) · 2)) ∨ z) + (((x ⊕ y) + ((x ∧ y) · 2)) ∧ z)

(0,7,2)?

(1, 1, 1) → 3

9(2, 3, 1) → 6

36

Program Synthesis: A Semantic Approach
We use f as a black-box:
f(x, y, z) := (((x ⊕ y) + ((x ∧ y) · 2)) ∨ z) + (((x ⊕ y) + ((x ∧ y) · 2)) ∧ z)

(0,7,2)?

(1, 1, 1) → 3

9(2, 3, 1) → 6(0, 7, 2) → 9

36

Program Synthesis: A Semantic Approach
We use f as a black-box:
f(x, y, z) := (((x ⊕ y) + ((x ∧ y) · 2)) ∨ z) + (((x ⊕ y) + ((x ∧ y) · 2)) ∧ z)

(1, 1, 1) → 3(2, 3, 1) → 6(0, 7, 2) → 9
We learn a function that has the same I/O behavior:

36

Program Synthesis: A Semantic Approach
We use f as a black-box:
f(x, y, z) := (((x ⊕ y) + ((x ∧ y) · 2)) ∨ z) + (((x ⊕ y) + ((x ∧ y) · 2)) ∧ z)

(1, 1, 1) → 3(2, 3, 1) → 6(0, 7, 2) → 9
We learn a function that has the same I/O behavior:h(x, y, z) := x + y + z
36How to synthesize programs?

Stochastic Program Synthesis• probabilistic optimization problem

global maxima

38

Stochastic Program Synthesis• probabilistic optimization problem

global maxima
0.96

0.71
0.34

0.62

0.11

38

Stochastic Program Synthesis• probabilistic optimization problem• based on Monte Carlo Tree Search (MCTS)
global maxima
0.96

0.71
0.34

0.62

0.11

38

Let’s synthesize: a + b mod 8

Program Generation

U→U+U|U∗U|a|b

40

Program Generation

U→U+U|U∗U|a|b• non-terminal symbol:

U40

Program Generation

U→U+U|U∗U|a|b• non-terminal symbol:

U• input variables:{a, b}

40

Program Generation

U→U+U|U∗U|a|b• non-terminal symbol:

U• input variables:{a, b}• candidate programs:

a, b, a ∗ b, a + b, . . .

40

Program Generation

U→U+U|U∗U|a|b• non-terminal symbol:

U• input variables:{a, b}• candidate programs:

a, b, a ∗ b, a + b, . . .

• intermediate programs:

U + U, U ∗ U, U + b, . . .

40

Monte Carlo Tree SearchU

41

Monte Carlo Tree Search

U
a

41

Monte Carlo Tree Search

U
a
0.64

41

Monte Carlo Tree Search

U
a
0.64

41

Monte Carlo Tree Search

U
a
0.64

b

41

Monte Carlo Tree Search

U
a
0.64

b

0.44

41

Monte Carlo Tree Search

U
a
0.64

b

0.44

41

Monte Carlo Tree Search

U
U*U

a
0.64

b

0.44

41

Monte Carlo Tree Search

U
U*U

a
0.64

b

0.44

(a+a)*(b*a)

41Monte Carlo Tree Search

U
U*U
0.39

a
0.64

b

0.44

41

Monte Carlo Tree Search

U
U*U
0.39

a
0.64

b

0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+U

a
0.64

b

0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+U

a
0.64

b

0.44

a+(b+b)41

Monte Carlo Tree Search

U
U*U
0.39

U+U
0.70

a
0.64

b

0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+U
0.70

a
0.64

b

0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+U
0.70

a
0.64

b

0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+U
0.70

a
0.64

b

0.44

U+(U+U)41

Monte Carlo Tree Search

U
U*U
0.39

U+U
0.70

a
0.64

b

0.44

U+(U+U)(a+a)+((a*b)+b)

41

Monte Carlo Tree Search

U
U*U
0.39

U+U
0.70

a
0.64

b

0.44

U+(U+U)
0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+U
0.70

a
0.64

b

0.44

U+(U+U)
0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+U
0.57

a
0.64

b

0.44

U+(U+U)
0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+U
0.57

a
0.64

b

0.44

U+(U+U)
0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+U
0.57

a
0.64

b

0.44

U+(U+U)
0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+b

U+U
0.57

a
0.64

b

0.44

U+(U+U)
0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+b

U+U
0.57

a
0.64

b

0.44

U+(U+U)
0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.57

a
0.64

b

0.44

U+(U+U)
0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.57

a
0.64

b

0.44

U+(U+U)
0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.62

a
0.64

b

0.44

U+(U+U)
0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.62

a
0.64

b

0.44

U+(U+U)
0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.62

a
0.64

b

0.44

U+(U+U)
0.44

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.62

a
0.64

b

0.44

U+(U*U)41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.62

a
0.64

b

0.44

U+(U*U)41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.62

a
0.64

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.62

a
0.64

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.64

a
0.64

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.64

a
0.64

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.64

a
0.64

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.64

a
0.64

U+a

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.64

a
0.64

U+a

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.64

a
0.64

U+a
0.87

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.64

a
0.64

U+a
0.87

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.69

a
0.64

U+a
0.87

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.69

a
0.64

U+a
0.87

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.69

a
0.64

U+a
0.87

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.69

a
0.64

U+a
0.87

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.69

a
0.64

U+a
0.87

b

0.44

U+(U*U)
0.69(U*U)+a41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U

U+(U+U)
0.44

0.69

a
0.64

U+a
0.87

b

0.44

U+(U*U)
0.69(U*U)+a41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.69

U+(U+U)
0.44

a
0.64

U+a
0.87

b

0.44

U+(U*U)
0.69(U*U)+a0.75

41Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.69

U+(U+U)
0.44

a
0.64

U+a
0.87

b

0.44

U+(U*U)
0.69(U*U)+a0.75

41Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.69

U+(U+U)
0.44

a
0.64

U+a
0.81

b

0.44

U+(U*U)
0.69(U*U)+a0.75

41Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.69

U+(U+U)
0.44

a
0.64

U+a
0.81

b

0.44

U+(U*U)
0.69(U*U)+a0.75

41Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.70

U+(U+U)
0.44

a
0.64

U+a
0.81

b

0.44

U+(U*U)
0.69(U*U)+a0.75

41Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.70

U+(U+U)
0.44

a
0.64

U+a
0.81

b

0.44

U+(U*U)
0.69(U*U)+a0.75

41Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.70

U+(U+U)
0.44

a
0.64

U+a
0.81

b

0.44

U+(U*U)
0.69(U*U)+a0.75

41Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.70

U+(U+U)
0.44

a
0.64

U+a
0.81

b

0.44

U+(U*U)
0.69(U*U)+a0.75

41Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.70

U+(U+U)a+(U+U)

0.44

a
0.64

U+a
0.81

b

0.44

U+(U*U)
0.69(U*U)+a0.75

41Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.70

U+(U+U)a+(U+U)

0.44

a
0.64

U+a
0.81

b

0.44

U+(U*U)
0.69(U*U)+a0.75

41Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.70

U+(U+U)
0.44

a
0.64

U+a
0.81

a+(U+U)(U*U)+a

0.68

0.75

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.70

U+(U+U)
0.44

a
0.64

U+a
0.81

a+(U+U)(U*U)+a

0.68

0.75

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.70

U+(U+U)
0.56

a
0.64

U+a
0.81

a+(U+U)(U*U)+a

0.68

0.75

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.70

U+(U+U)
0.56

a
0.64

U+a
0.81

a+(U+U)(U*U)+a

0.68

0.75

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.69

U+(U+U)
0.56

a
0.64

U+a
0.81

a+(U+U)(U*U)+a

0.68

0.75

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.69

U+(U+U)
0.56

a
0.64

U+a
0.81

a+(U+U)(U*U)+a

0.68

0.75

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.69

U+(U+U)
0.56

a
0.64

U+a
0.81

a+(U+U)(U*U)+a

0.68

0.75

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.69

U+(U+U)
0.56

a
0.64

U+a
0.81

a+(U+U)(U*U)+a

0.68

0.75

b

0.44

U+(U*U)
0.69

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.69

U+(U+U)
0.56

a
0.64

U+a
0.81

a+(U+U)(U*U)+a

0.68

0.75

b

0.44

U+(U*U)
0.69

b+a

41

Monte Carlo Tree Search

U
U*U
0.39

U+b
0.73

U+U
0.69

U+(U+U)
0.56

a
0.64

U+a
0.81

b

0.44

U+(U*U)
0.69

a+(U+U)(U*U)+a

b+a

0.68

0.75

1.00

41

Score Calculation

(2,2)

?
42

Score Calculation

(2,2)

?
4

42

Score Calculation

(2,2)

?
4

6

42

Score Calculation(2,2)
similarity(4, 6)

?
4

=

0.78

6

42

Score Calculation

(5,3)

?

similarity(4, 6)

=

0.78

42

Score Calculation

(5,3)

?

similarity(4, 6)

=

0.78

0

42

Score Calculation(5,3)
similarity(4, 6)

?
0

=

0.78

3

42

Score Calculation

(5,3)

?
0

similarity(4, 6)

=

0.78

similarity(0, 3)

=

0.33

3

42

Score Calculation

(3,0)

?

similarity(4, 6)

=

0.78

similarity(0, 3)

=

0.33

42

Score Calculation

(3,0)

?

similarity(4, 6)

=

0.78

similarity(0, 3)

=

0.33

3

42

Score Calculation

(3,0)

?
3

similarity(4, 6)

=

0.78

similarity(0, 3)

=

0.33

3

42

Score Calculation

(3,0)

?
3

similarity(4, 6)

=

0.78

similarity(0, 3)

=

0.33

similarity(3, 3)

=

1.0

3

42

Score Calculation

(3,0)

?
3

3

similarity(4, 6)

=

0.78

similarity(0, 3)

=

0.33

similarity(3, 3)=

1.0

average score: 0.7042Output Similarity: similarity(O, O′ )11110111100100001000110010000000
11100010000110011110101100000000

Let’s compare:43Output Similarity: similarity(O, O′ )11110111100100001000110010000000
11100010000110011110101100000000

Are they in the same range?
43

Output Similarity: similarity(O, O′ )11110111100100001000110010000000
11100010000110011110101100000000

How many bits are different?
43Output Similarity: similarity(O, O′ )11110111100100001000110010000000
00010101011101101010000110000000
11100010000110011110101100000000

How close are they numerically?
43

DEMO

How to synthesize obfuscated code?

Obtaining Codestatic disassembly46Obtaining Code54 68 69 73 20 64 6f
65 73 6e 27 74 20 6c
6f 6f 6b 20 6c 69 6b
65 20 61 6e 79 74 68
69 6e 67 20 74 6f 20
6d 65 2e de ad be ef

static disassembly

memory dump

46

Obtaining Code54 68 69 73 20 64 6f
65 73 6e 27 74 20 6c
6f 6f 6b 20 6c 69 6b
65 20 61 6e 79 74 68
69 6e 67 20 74 6f 20
6d 65 2e de ad be ef

static disassembly

memory dump

mov
xor
mov
add
mov
mov
mov
mov
add
or
add
mov
or
sub
movzx
xor
add
add
mov
sub
or
or
movzx
xor
mov
add
xor
mov
add

r15, 0x200
r15, 0x800
rbx, rbp
rbx, 0xc0
rbx, qword ptr [rbx]r13, 1
rcx, 0r15, rbp
r15, 0xc0
rcx, 0x88
rbx, 0xb
r15, qword ptr [r15]r12, 0xffffffff80000000
rcx, 0x78
r10, word ptr [rbx]r12, r13
r12, 0xffff
r15, 0r8, rbprcx, 0x10
r12, r12
rcx, 0x800
r11, word ptr [r15]rcx, 0x800
r12, r15
r8, 0
r12, 0xf0
rbx, 0x58
r11, rbp

mov
xor
sub
or
mov
mov
sub
mov
mov
sub
sub
add
add
and
xor
mov
add
sub
add
add
mov
mov
add
xor
add
add
mov
mov
mov

r15, rdx
r10d, dword ptr [r12]r15, 0x800
rdx, 0x400
rsi, 0x200
r14, rbp
rsi, rsi
rdi, rbp
r8, 0x400
rsi, r9
r8, rsi
r14, 0rsi, rax
r8, 0x88
rsi, r14
rsi, rbp
rdi, 0xc0
r8, rdir8, 0x78
rsi, 4rcx, 0x200
rdi, qword ptr [rdi]dword ptr [rsi], 0x254
rcx, 0xf0
rcx, r10
rdi, 6
r8, 0x400
ax, word ptr [rdi]r8, 1

instruction trace46

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx• not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher?

rbx

Handler performing nor(with ﬂag side-effects)
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx• not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

(0,5)

?

rbx

?

-1

Handler performing nor(with ﬂag side-effects)
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx• not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

?

rbx

(0,5)

?

-1

(2,7)

?

-3

Handler performing nor(with ﬂag side-effects)
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx• not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)

?

rbx

(0,5)

?

-1

(2,7)

?

-3

���
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx• not rbx
and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)?

rbx

rbx ← ¬ m0?

-1

?

-3

(0,5)

(2,7)

���
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx• and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher?

rcx

Handler performing nor(with ﬂag side-effects)
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx• and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

(3,6)

?

rcx

?

-8

Handler performing nor(with ﬂag side-effects)
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx• and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

?

rcx

(3,6)

?

-8

(1,1)

?

-2

Handler performing nor(with ﬂag side-effects)
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx• and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)

?

rcx

(3,6)

?

-8

(1,1)

?

-2

���
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx• and rcx, rbx
mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher?

rcx ← ¬ (m0 ∨?m1)

Handler performing nor(with ﬂag side-effects)

(3,6)

(1,1)

?

rcx

-8

-2

���
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx• mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher?

Handler performing nor(with ﬂag side-effects)
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx• mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

?
(0,0)

?

-1

Handler performing nor(with ﬂag side-effects)
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx• mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

?
(0,0)

?

-1

(4,3)

?

-8

Handler performing nor(with ﬂag side-effects)
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx• mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

Handler performing nor(with ﬂag side-effects)

?
(0,0)

?

-1

(4,3)

?

-8

���
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx
not rbx
and rcx, rbx• mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher?

m1 )M0 ← ¬ (m0 ∨?

Handler performing nor(with ﬂag side-effects)

(0,0)

(4,3)

?

-1

-8

���
47

Learning Code Semantics__handle_vnor:
mov rcx, [rbp]mov rbx, [rbp + 4]
not rcx• not rbx
• and rcx, rbx• mov [rbp + 4], rcx
pushf
pop [rbp]
jmp __vm_dispatcher

rbx ← ¬ m0

rcx ← ¬ (m0 ∨ m1 )M0 ← ¬ (m0 ∨ m1 )Handler performing nor(with ﬂag side-effects)
47

I/O Samplingx64dbg

WinDbg

Unicorn<your tool here>

Miasm

angr
Metasm48

Instruction Trace: Forced Executiontruecall checkcmp eax, 0�deadbeef
je��block_a��block_a: …
…

false

��block_b: …
…

49

Instruction Trace: Forced Execution

force

call checkcmp eax, 0�deadbeef
je��block_aignore��block_a: …
…

49

Instruction Trace: Forced Execution

call checkcmp eax, 0�deadbeef
je��block_a

force

ignore��block_b: …
…

49

Syntia• program synthesis framework for code deobfuscation• written in Python• random I/O sampling for assembly code
• MCTS-based program synthesis

https://github.com/RUB-SysSec/syntia

DEMO

Breaking Virtual Machine Obfuscation

Reminder: Virtual Machine Hardening

Hardening Technique #1 – Obfuscating individual VM components.
Hardening Technique #2 – Duplicating VM handlers.
Hardening Technique #3 – No central VM dispatcher.
Hardening Technique #4 – No explicit handler table.
Hardening Technique #5 – Blinding VM bytecode.

53#1: Obfuscating Individual VM Components
movr15, 0x200
xor
r15, 0x800
mov
rbx, rbp
add
rbx, 0xc0
mov
rbx, qword ptr [rbx]movr13, 1movrcx, 0mov
r15, rbp
add
r15, 0xc0
or
rcx, 0x88
add
rbx, 0xb
mov
r15, qword ptr [r15]orr12, 0xffffffff80000000
subrcx, 0x78
movzx r10, word ptr [rbx]xor
r12, r13
add
r12, 0xffff
addr15, 0mov
r8, rbpsubrcx, 0x10
orr12, r12orrcx, 0x800
movzx r11, word ptr [r15]xorrcx, 0x800
mov
r12, r15
add
r8, 0
xor
r12, 0xf0
mov
rbx, 0x58
add
r11, rbp
xor
rbx, 0x800
andr12, 0x20
add
rbx, 0x800
mov
r11, qword ptr [r11]addrbx, 1andr12, r9movrdx, 1xor
r10d, dword ptr [r8]sub
r9, r11
pushfqxor
rbx, 0xf0
xor
rbx, 0x800
andrdx, r8movr12, rbp
xor
rdx, 0x20
subrbx, 4add
r11, 0x2549b044
orrbx, 0x78
andrdx, r10
movrax, 0add
r12, 0x42

mov
xor
sub
or
mov
mov
sub
mov
mov
sub
sub
add
add
and
xor
mov
add
sub
add
add
mov
mov
add
xor
add
add
mov
mov
mov
mov
and
sub
mov
add
or
mov
add
mov
cmp
jbe
and
or
or
mov
or
sub
add
or
add
add

add
r15, rdxor
r10d, dword ptr [r12]add
r15, 0x800
mov
rdx, 0x400
subrsi, 0x200
pop
r14, rbp
movrsi, rsi
addrdi, rbp
mov
r8, 0x400
addrsi, r9
movzx
r8, rsimovr14, 0add
rsi, raxxor
r8, 0x88
andrsi, r14
subrsi, rbp
movrdi, 0xc0
subr8, rdimov
r8, 0x78
orrsi, 4andrcx, 0x200
mov
rdi, qword ptr [rdi]dword ptr [rsi], 0x2549b044 add
movrcx, 0xf0
subrcx, r10
add
rdi, 6
sub
r8, 0x400
add
ax, word ptr [rdi]
mov
r8, 1
or
rsi, rbp
subrcx, 8mov
rcx, 1movrcx, rdiaddrsi, 0x29
subrcx, 8mov
r8, rsiorrcx, 4xor
r13b, byte ptr [rsi]movr13b, 0xd2
add
0x204
sub
r8, r13xor
rcx, r13xor
rcx, 4add
rbx, rbp
movrcx, 4mov
rcx, 0x400
add
rax, rbp
add
rcx, 0x80
xor
rcx, 0x80
mov
rbx, 0x5aor
r14, r14
r8, 1
mov
rax, rbp
r8, 0x78
andrcx, r13
word ptr [rbx], r10w
add
rax, 4r15, raxsub
r8, -0x80000000
r15, raxadd
r13, 0xffff
r9
andrcx, 0x20
rcx, rbp
movr10, rbp
rcx, 0xc0
add
r13, r15
rcx, qword ptr [rcx]add
r14, r8
rcx, 8add
r10, 0x89
r10, word ptr [rcx]xorword ptr [r10], si
r9, rbpxor
rdx, r11
r9, 0
mov
rsi, rbp
r10d, dword ptr [r9]rdx, rbx
rdi, 0xffffffff80000000 sub
andrax, 0x40
r13, 0xf0
or
rbx, 0xf0
rsi, 0add
rsi, 0x5ar13, 0x20
mov
r8, rcx
rbx, rbp
movzx rsi, word ptr [rsi]r13, 0x88
movrax, 0x200
rcx, 8mov
r14, rbp
r8, 0x58
andrax, rdx
rbx, 0xc0
and
rcx, 0x20
rbx, qword ptr [rbx]add
r14, 0x89
rcx, 0x20
orrax, 0x40
rdi, 0x80
xor
si, 0x7a28
r13, 0x10
add
rdx, 0x78
rbx, 8add
rdx, 0x20
si, word ptr [rbx]movzx r14, word ptr [r14]r9, 0xffff
mov
rcx, 0x58
r9, 1
add
rsi, rbp
r9, rbpxor
rax, rdx
r12, 0x58
add
r8, 0x80
r9, 0
mov
r15, rsi
r13, 0x80
add
r14, rbp
r15, r13
add
r8, r15
rcx, r12
movrbx, 0esi, dword ptr [r9]andrdx, 0x10
r10, rbp
mov
r14, qword ptr [r14]r10, 0xcc
add
qword ptr [rsi], r14
r15, 0x20
pushfqesi, dword ptr [r10]xor
r11, r14
r13, 0x90
addr15, r14
rdi, 0x10
mov
r13, 0x12
r14, rsi
movr8, 0rdx, rbp
andr14, 0x88
rdx, 0and
r13, 0x40
dword ptr [rdx], esi
addr13, 1
r12, 1movrdx, rbp
r13, r15

mov
add
add
or
mov
add
add
mov
cmp
je
mov
or
and
xor
add
or
mov
mov
sub
add
or
mov
mov
add
xor
pop
mov
jmp
xor
xor
add
mov
mov
or
and
mov
or
add
xor
and
or
mov
mov
sub
add
mov
xor
mov
xor
mov

r14, 0x200
rdx, 0xc0
r11, r14
r15, 0x88
rdx, qword ptr [rdx]rdx, 0xa
r11, 0x78
r8b, byte ptr [rdx]r8b, 00x49erdx, rbp
r11, 0x40
r15, 1
r11, 0x10
rdx, 0xc0
r14, 4r15, 0x12
rdx, qword ptr [rdx]r11, r8rdx, 4r11, 0x80
r8w, word ptr [rdx]r14, r8
r8, rbp
r13, 4r10
qword ptr [r8], r10
0x4ae
rsi, 0x88
rbx, 0xffffffff80000000
rsi, 0x78
r10b, 0x68
r9, 0x12
rbx, r10
r15, 0x78
r14, rbp
r9, 8
r14, 0x29
rbx, rdi
r15, 0x3f
byte ptr [r14], r10b
rax, 0x58
r8, rbprsi, 0x78
r8, 0x127
rdi, rbx
rbx, 0x3f
r8, qword ptr [r8]rsi, 1rax, rbp

add
or
and
add
add
or
mov
and
add
sub
or
movzx
mov
mov
mov
add
or
add
xor
add
add
mov
or
add
or
add
mov
add
and
or
and
and
mov
add
or
shl
add
or
sub
or
mov
mov
sub
add
add
jmp

r15, 0x3f
r15, 0xffffffff80000000
rsi, r9rax, 0xc0
rdi, r14
rsi, 1rax, qword ptr [rax]rdi, 0x7fffffffrax, 2
rsi, 4rbx, rsi
rax, word ptr [rax]r9, rbp
r13, 0x200
r10, 0x58r9, 0r10, 0x20
eax, dword ptr [r9]r10, 0x40
eax, 0x3f505c07
r15, 0x88
r12, rbp
rdi, 0x90
r12, 0rbx, 0x80
rdi, 0xf0
r13, 0x400
dword ptr [r12], eax
rsi, r8
r10, 8rbx, 0x20
rax, 0xffff
r11, 0r13, r8
rbx, 1rax, 3r8, raxrbx, r15
r15, 0x10
r11, r13
rbx, qword ptr [r8]rdx, rbp
r13, 0x80
rdx, 0xc0
qword ptr [rdx], 0xd
rbx

54#1: Obfuscating Individual VM Components
movr15, 0x200
xor
r15, 0x800
mov
rbx, rbp
add
rbx, 0xc0
mov
rbx, qword ptr [rbx]movr13, 1movrcx, 0mov
r15, rbp
add
r15, 0xc0
or
rcx, 0x88
add
rbx, 0xb
mov
r15, qword ptr [r15]orr12, 0xffffffff80000000
subrcx, 0x78
movzx r10, word ptr [rbx]xor
r12, r13
add
r12, 0xffff
addr15, 0mov
r8, rbpsubrcx, 0x10
orr12, r12orrcx, 0x800
movzx r11, word ptr [r15]xorrcx, 0x800
mov
r12, r15
add
r8, 0
xor
r12, 0xf0
mov
rbx, 0x58
add
r11, rbp
xor
rbx, 0x800
andr12, 0x20
add
rbx, 0x800
mov
r11, qword ptr [r11]addrbx, 1andr12, r9movrdx, 1xor
r10d, dword ptr [r8]sub
r9, r11
pushfqxor
rbx, 0xf0
xor
rbx, 0x800
andrdx, r8movr12, rbp
xor
rdx, 0x20
subrbx, 4add
r11, 0x2549b044
orrbx, 0x78
andrdx, r10
movrax, 0add
r12, 0x42

mov
xor
sub
or
mov
mov
sub
mov
mov
sub
sub
add
add
and
xor
mov
add
sub
add
add
mov
mov
add
xor
add
add
mov
mov
mov
mov
and
sub
mov
add
or
mov
add
mov
cmp
jbe
and
or
or
mov
or
sub
add
or
add
add

add
r15, rdxor
r10d, dword ptr [r12]add
r15, 0x800
mov
rdx, 0x400
subrsi, 0x200
pop
r14, rbp
movrsi, rsi
addrdi, rbp
mov
r8, 0x400
addrsi, r9
movzx
r8, rsimovr14, 0add
rsi, raxxor
r8, 0x88
andrsi, r14
subrsi, rbp
movrdi, 0xc0
subr8, rdimov
r8, 0x78
orrsi, 4andrcx, 0x200
mov
rdi, qword ptr [rdi]dword ptr [rsi], 0x2549b044 add
movrcx, 0xf0
subrcx, r10
add
rdi, 6
sub
r8, 0x400
add
ax, word ptr [rdi]
mov
r8, 1
or
rsi, rbp
subrcx, 8mov
rcx, 1movrcx, rdiaddrsi, 0x29
subrcx, 8mov
r8, rsiorrcx, 4xor
r13b, byte ptr [rsi]movr13b, 0xd2
add
0x204
sub
r8, r13xor
rcx, r13xor
rcx, 4add
rbx, rbp
movrcx, 4mov
rcx, 0x400
add
rax, rbp
add
rcx, 0x80
xor
rcx, 0x80
mov
rbx, 0x5aor
r14, r14
r8, 1
mov
rax, rbp
r8, 0x78
andrcx, r13
word ptr [rbx], r10w
add
rax, 4r15, raxsub
r8, -0x80000000
r15, raxadd
r13, 0xffff
r9
andrcx, 0x20
rcx, rbp
movr10, rbp
rcx, 0xc0
add
r13, r15
rcx, qword ptr [rcx]add
r14, r8
rcx, 8add
r10, 0x89
r10, word ptr [rcx]xorword ptr [r10], si
r9, rbpxor
rdx, r11
r9, 0
mov
rsi, rbp
r10d, dword ptr [r9]rdx, rbx
rdi, 0xffffffff80000000 sub
andrax, 0x40
r13, 0xf0
or
rbx, 0xf0
rsi, 0add
rsi, 0x5ar13, 0x20
mov
r8, rcx
rbx, rbp
movzx rsi, word ptr [rsi]r13, 0x88
movrax, 0x200
rcx, 8mov
r14, rbp
r8, 0x58
andrax, rdx
rbx, 0xc0
and
rcx, 0x20
rbx, qword ptr [rbx]add
r14, 0x89
rcx, 0x20
orrax, 0x40
rdi, 0x80
xor
si, 0x7a28
r13, 0x10
add
rdx, 0x78
rbx, 8add
rdx, 0x20
si, word ptr [rbx]movzx r14, word ptr [r14]r9, 0xffff
mov
rcx, 0x58
r9, 1
add
rsi, rbp
r9, rbpxor
rax, rdx
r12, 0x58
add
r8, 0x80
r9, 0
mov
r15, rsi
r13, 0x80
add
r14, rbp
r15, r13
add
r8, r15
rcx, r12
movrbx, 0esi, dword ptr [r9]andrdx, 0x10
r10, rbp
mov
r14, qword ptr [r14]r10, 0xcc
add
qword ptr [rsi], r14
r15, 0x20
pushfqesi, dword ptr [r10]xor
r11, r14
r13, 0x90
addr15, r14
rdi, 0x10
mov
r13, 0x12
r14, rsi
movr8, 0rdx, rbp
andr14, 0x88
rdx, 0and
r13, 0x40
dword ptr [rdx], esi
addr13, 1
r12, 1movrdx, rbp
r13, r15

mov
add
add
or
mov
add
add
mov
cmp
je
mov
or
and
xor
add
or
mov
mov
sub
add
or
mov
mov
add
xor
pop
mov
jmp
xor
xor
add
mov
mov
or
and
mov
or
add
xor
and
or
mov
mov
sub
add
mov
xor
mov
xor
mov

r14, 0x200
rdx, 0xc0
r11, r14
r15, 0x88
rdx, qword ptr [rdx]rdx, 0xa
r11, 0x78
r8b, byte ptr [rdx]r8b, 00x49erdx, rbp
r11, 0x40
r15, 1
r11, 0x10
rdx, 0xc0
r14, 4r15, 0x12
rdx, qword ptr [rdx]r11, r8rdx, 4r11, 0x80
r8w, word ptr [rdx]r14, r8
r8, rbp
r13, 4r10
qword ptr [r8], r10
0x4ae
rsi, 0x88
rbx, 0xffffffff80000000
rsi, 0x78
r10b, 0x68
r9, 0x12
rbx, r10
r15, 0x78
r14, rbp
r9, 8
r14, 0x29
rbx, rdi
r15, 0x3f
byte ptr [r14], r10b
rax, 0x58
r8, rbprsi, 0x78
r8, 0x127
rdi, rbx
rbx, 0x3f
r8, qword ptr [r8]rsi, 1rax, rbp

u64 res = M13 + M14

add
or
and
add
add
or
mov
and
add
sub
or
movzx
mov
mov
mov
add
or
add
xor
add
add
mov
or
add
or
add
mov
add
and
or
and
and
mov
add
or
shl
add
or
sub
or
mov
mov
sub
add
add
jmp

r15, 0x3f
r15, 0xffffffff80000000
rsi, r9rax, 0xc0
rdi, r14
rsi, 1rax, qword ptr [rax]rdi, 0x7fffffffrax, 2
rsi, 4rbx, rsi
rax, word ptr [rax]r9, rbp
r13, 0x200
r10, 0x58r9, 0r10, 0x20
eax, dword ptr [r9]r10, 0x40
eax, 0x3f505c07
r15, 0x88
r12, rbp
rdi, 0x90
r12, 0rbx, 0x80
rdi, 0xf0
r13, 0x400
dword ptr [r12], eax
rsi, r8
r10, 8rbx, 0x20
rax, 0xffff
r11, 0r13, r8
rbx, 1rax, 3r8, raxrbx, r15
r15, 0x10
r11, r13
rbx, qword ptr [r8]rdx, rbp
r13, 0x80
rdx, 0xc0
qword ptr [rdx], 0xd
rbx

54#2: Duplicating VM Handlers

handle_vpush?
handle_vadd?
handle_vxor?
handle_vexit?
handle_vpop
?
?
?
?
?

…

55

#2: Duplicating VM Handlers

handle_vpush?
vm_add64
handle_vadd
vm_xor32
handle_vxor
handle_vexit?
vm_sub16
handle_vpop
vm_shl16
vm_add8?
vm_add64…

55

#2: Duplicating VM Handlers

handle_vpush?
vm_add64
handle_vadd
vm_xor32
handle_vxor
handle_vexit?
vm_sub16
handle_vpop
vm_shl16
vm_add8?
vm_add64…

55

#5: Blinding VM Bytecodemovr15, 0x200
xor
r15, 0x800
mov
rbx, rbp
add
rbx, 0xc0
mov
rbx, qword ptr [rbx]movr13, 1movrcx, 0mov
r15, rbp
add
r15, 0xc0
or
rcx, 0x88
add
rbx, 0xb
mov
r15, qword ptr [r15]orr12, 0xffffffff80000000
subrcx, 0x78
movzx r10, word ptr [rbx]xor
r12, r13
add
r12, 0xffff
addr15, 0mov
r8, rbpsubrcx, 0x10
orr12, r12orrcx, 0x800
movzx r11, word ptr [r15]xorrcx, 0x800
mov
r12, r15
add
r8, 0
xor
r12, 0xf0
mov
rbx, 0x58
add
r11, rbp
xor
rbx, 0x800
andr12, 0x20
add
rbx, 0x800
mov
r11, qword ptr [r11]addrbx, 1andr12, r9movrdx, 1xor
r10d, dword ptr [r8]sub
r9, r11
pushfqxor
rbx, 0xf0
xor
rbx, 0x800
andrdx, r8movr12, rbp
xor
rdx, 0x20
subrbx, 4add
r11, 0x2549b044
orrbx, 0x78
andrdx, r10
movrax, 0add
r12, 0x42

mov
xor
sub
or
mov
mov
sub
mov
mov
sub
sub
add
add
and
xor
mov
add
sub
add
add
mov
mov
add
xor
add
add
mov
mov
mov
mov
and
sub
mov
add
or
mov
add
mov
cmp
jbe
and
or
or
mov
or
sub
add
or
add
add

r15, rdxadd
r10d, dword ptr [r12]orr15, 0x800
addrdx, 0x400
mov
rsi, 0x200
sub
r14, rbp
pop
rsi, rsimovrdi, rbp
add
r8, 0x400
mov
rsi, r9
add
r8, rsimovzx
r14, 0movrsi, raxadd
r8, 0x88
xor
rsi, r14andrsi, rbp
subrdi, 0xc0
mov
r8, rdisub
r8, 0x78
movrsi, 4orrcx, 0x200
andrdi, qword ptr [rdi]movdword ptr [rsi], 0x2549b044 add
rcx, 0xf0
mov
rcx, r10
subrdi, 6add
r8, 0x400
sub
ax, word ptr [rdi]
add
r8, 1
mov
rsi, rbp
orrcx, 8sub
rcx, 1movrcx, rdimovrsi, 0x29
add
rcx, 8sub
r8, rsimovrcx, 4or
r13b, byte ptr [rsi]xor
r13b, 0xd2
mov
0x204
add
r8, r13sub
rcx, r13xor
rcx, 4xor
rbx, rbp
add
rcx, 4mov
rcx, 0x400
mov
rax, rbp
add
rcx, 0x80
add
rcx, 0x80
xor
rbx, 0x5a
movor
r14, r14
r8, 1
mov
rax, rbp
r8, 0x78
andrcx, r13
word ptr [rbx], r10w
add
rax, 4r15, raxsub
r8, -0x80000000
r15, raxadd
r13, 0xffff
r9
andrcx, 0x20
rcx, rbp
movr10, rbp
rcx, 0xc0
add
r13, r15
rcx, qword ptr [rcx]add
r14, r8
rcx, 8add
r10, 0x89
r10, word ptr [rcx]xorword ptr [r10], si
r9, rbpxor
rdx, r11
r9, 0
mov
rsi, rbp
r10d, dword ptr [r9]rdx, rbx
rdi, 0xffffffff80000000 sub
andrax, 0x40
r13, 0xf0
or
rbx, 0xf0
rsi, 0add
rsi, 0x5ar13, 0x20
mov
r8, rcx
rbx, rbp
movzx rsi, word ptr [rsi]r13, 0x88
movrax, 0x200
rcx, 8mov
r14, rbp
r8, 0x58
andrax, rdx
rbx, 0xc0
and
rcx, 0x20
rbx, qword ptr [rbx]add
r14, 0x89
rcx, 0x20
orrax, 0x40
rdi, 0x80
xor
si, 0x7a28
r13, 0x10
add
rdx, 0x78
rbx, 8add
rdx, 0x20
si, word ptr [rbx]movzx r14, word ptr [r14]r9, 0xffff
mov
rcx, 0x58
r9, 1
add
rsi, rbp
r9, rbpxor
rax, rdx
r12, 0x58
add
r8, 0x80
r9, 0
mov
r15, rsi
r13, 0x80
add
r14, rbp
r15, r13
add
r8, r15
rcx, r12
movrbx, 0esi, dword ptr [r9]andrdx, 0x10
r10, rbp
mov
r14, qword ptr [r14]r10, 0xcc
add
qword ptr [rsi], r14
r15, 0x20
pushfqesi, dword ptr [r10]xor
r11, r14
r13, 0x90
addr15, r14
rdi, 0x10
mov
r13, 0x12
r14, rsi
movr8, 0rdx, rbp
andr14, 0x88
rdx, 0and
r13, 0x40
dword ptr [rdx], esi
addr13, 1
r12, 1movrdx, rbp
r13, r15

mov
add
add
or
mov
add
add
mov
cmp
je
mov
or
and
xor
add
or
mov
mov
sub
add
or
mov
mov
add
xor
pop
mov
jmp
xor
xor
add
mov
mov
or
and
mov
or
add
xor
and
or
mov
mov
sub
add
mov
xor
mov
xor
mov

r14, 0x200
rdx, 0xc0
r11, r14
r15, 0x88
rdx, qword ptr [rdx]rdx, 0xa
r11, 0x78
r8b, byte ptr [rdx]r8b, 00x49erdx, rbp
r11, 0x40
r15, 1
r11, 0x10
rdx, 0xc0
r14, 4r15, 0x12
rdx, qword ptr [rdx]r11, r8rdx, 4r11, 0x80
r8w, word ptr [rdx]r14, r8
r8, rbp
r13, 4r10
qword ptr [r8], r10
0x4ae
rsi, 0x88
rbx, 0xffffffff80000000
rsi, 0x78
r10b, 0x68
r9, 0x12
rbx, r10
r15, 0x78
r14, rbp
r9, 8
r14, 0x29
rbx, rdi
r15, 0x3f
byte ptr [r14], r10b
rax, 0x58
r8, rbprsi, 0x78
r8, 0x127
rdi, rbx
rbx, 0x3f
r8, qword ptr [r8]rsi, 1rax, rbp

add
or
and
add
add
or
mov
and
add
sub
or
movzx
mov
mov
mov
add
or
add
xor
add
add
mov
or
add
or
add
mov
add
and
or
and
and
mov
add
or
shl
add
or
sub
or
mov
mov
sub
add
add
jmp

r15, 0x3f
r15, 0xffffffff80000000
rsi, r9rax, 0xc0
rdi, r14
rsi, 1rax, qword ptr [rax]rdi, 0x7fffffffrax, 2
rsi, 4rbx, rsi
rax, word ptr [rax]r9, rbp
r13, 0x200
r10, 0x58r9, 0r10, 0x20
eax, dword ptr [r9]r10, 0x40
eax, 0x3f505c07
r15, 0x88
r12, rbp
rdi, 0x90
r12, 0rbx, 0x80
rdi, 0xf0
r13, 0x400
dword ptr [r12], eax
rsi, r8
r10, 8rbx, 0x20
rax, 0xffff
r11, 0r13, r8
rbx, 1rax, 3r8, raxrbx, r15
r15, 0x10
r11, r13
rbx, qword ptr [r8]rdx, rbp
r13, 0x80
rdx, 0xc0
qword ptr [rdx], 0xd
rbx

56

#5: Blinding VM Bytecodemovr15, 0x200
xor
r15, 0x800
mov
rbx, rbp
add
rbx, 0xc0
mov
rbx, qword ptr [rbx]movr13, 1movrcx, 0mov
r15, rbp
add
r15, 0xc0
or
rcx, 0x88
add
rbx, 0xb
mov
r15, qword ptr [r15]orr12, 0xffffffff80000000
subrcx, 0x78
movzx r10, word ptr [rbx]xor
r12, r13
add
r12, 0xffff
addr15, 0mov
r8, rbpsubrcx, 0x10
orr12, r12orrcx, 0x800
movzx r11, word ptr [r15]xorrcx, 0x800
mov
r12, r15
add
r8, 0
xor
r12, 0xf0
mov
rbx, 0x58
add
r11, rbp
xor
rbx, 0x800
andr12, 0x20
add
rbx, 0x800
mov
r11, qword ptr [r11]addrbx, 1andr12, r9movrdx, 1xor
r10d, dword ptr [r8]sub
r9, r11
pushfqxor
rbx, 0xf0
xor
rbx, 0x800
andrdx, r8movr12, rbp
xor
rdx, 0x20
subrbx, 4add
r11, 0x2549b044
orrbx, 0x78
andrdx, r10
movrax, 0add
r12, 0x42

mov
xor
sub
or
mov
mov
sub
mov
mov
sub
sub
add
add
and
xor
mov
add
sub
add
add
mov
mov
add
xor
add
add
mov
mov
mov
mov
and
sub
mov
add
or
mov
add
mov
cmp
jbe
and
or
or
mov
or
sub
add
or
add
add

r15, rdxadd
r10d, dword ptr [r12]orr15, 0x800
addrdx, 0x400
mov
rsi, 0x200
sub
r14, rbp
pop
rsi, rsimovrdi, rbp
add
r8, 0x400
mov
rsi, r9
add
r8, rsimovzx
r14, 0movrsi, raxadd
r8, 0x88
xor
rsi, r14andrsi, rbp
subrdi, 0xc0
mov
r8, rdisub
r8, 0x78
movrsi, 4orrcx, 0x200
andrdi, qword ptr [rdi]movdword ptr [rsi], 0x2549b044 add
rcx, 0xf0
mov
rcx, r10
subrdi, 6add
r8, 0x400
sub
ax, word ptr [rdi]
add
r8, 1
mov
rsi, rbp
orrcx, 8sub
rcx, 1movrcx, rdimovrsi, 0x29
add
rcx, 8sub
r8, rsimovrcx, 4or
r13b, byte ptr [rsi]xor
r13b, 0xd2
mov
0x204
add
r8, r13sub
rcx, r13xor
rcx, 4xor
rbx, rbp
add
rcx, 4mov
rcx, 0x400
mov
rax, rbp
add
rcx, 0x80
add
rcx, 0x80
xor
rbx, 0x5a
mov

mov
…
add
…
add
…
add
…
mov
…
add
add

or
r14, r14
r8, 1
mov
rax, rbp
r8, 0x78
andrcx, r13
word ptr [rbx], r10w
add
rax, 4r15, raxsub
r8, -0x80000000
r15, raxadd
r13, 0xffff
r9
andrcx, 0x20
rcx, rbp
movr10, rbp
rcx, 0xc0
add
r13, r15
rcx, qword ptr [rcx]add
r14, r8
rcx, 8add
r10, 0x89
r10, word ptr [rcx]xorword ptr [r10], si
r9, rbpxor
rdx, r11
r9, 0
mov
rsi, rbp
r10d, dword ptr [r9]rdx, rbx
rdi, 0xffffffff80000000 sub
andrax, 0x40
r13, 0xf0
or
rbx, 0xf0
rsi, 0add
rsi, 0x5ar13, 0x20
mov
r8, rcx
rbx, rbp
movzx rsi, word ptr [rsi]r13, 0x88
movrax, 0x200
rcx, 8mov
r14, rbp
r8, 0x58
andrax, rdx
rbx, 0xc0
and
rcx, 0x20
rbx, qword ptr [rbx]add
r14, 0x89
rcx, 0x20
orrax, 0x40
rdi, 0x80
xor
si, 0x7a28
r13, 0x10
add
rdx, 0x78
rbx, 8add
rdx, 0x20
si, word ptr [rbx]movzx r14, word ptr [r14]r9, 0xffff
mov
rcx, 0x58
r9, 1
add
rsi, rbp
r9, rbpxor
rax, rdx
r12, 0x58
add
r8, 0x80
r9, 0
mov
r15, rsi
r13, 0x80
add
r14, rbp
r15, r13
add
r8, r15
rcx, r12
movrbx, 0esi, dword ptr [r9]andrdx, 0x10
r10, rbp
mov
r14, qword ptr [r14]r10, 0xcc
add
qword ptr [rsi], r14
r15, 0x20
pushfqesi, dword ptr [r10]xor
r11, r14
r13, 0x90
addr15, r14
rdi, 0x10
mov
r13, 0x12
r14, rsi
movr8, 0rdx, rbp
andr14, 0x88
rdx, 0and
r13, 0x40
dword ptr [rdx], esi
addr13, 1
r12, 1movrdx, rbp
r13, r15

r9, rbp
r9, 0

eax, dword ptr [r9]eax, 0x3f505c07

r12, rbp

r12, 0dword ptr [r12], eax

mov
add
add
or
mov
add
add
mov
cmp
je
mov
or
and
xor
add
or
mov
mov
sub
add
or
mov
mov
add
xor
pop
mov
jmp
xor
xor
add
mov
mov
or
and
mov
or
add
xor
and
or
mov
mov
sub
add
mov
xor
mov
xor
mov

r14, 0x200
rdx, 0xc0
r11, r14
r15, 0x88
rdx, qword ptr [rdx]rdx, 0xa
r11, 0x78
r8b, byte ptr [rdx]r8b, 00x49erdx, rbp
r11, 0x40
r15, 1
r11, 0x10
rdx, 0xc0
r14, 4r15, 0x12
rdx, qword ptr [rdx]r11, r8rdx, 4r11, 0x80
r8w, word ptr [rdx]r14, r8
r8, rbp
r13, 4r10
qword ptr [r8], r10
0x4ae
rsi, 0x88
rbx, 0xffffffff80000000
rsi, 0x78
r10b, 0x68
r9, 0x12
rbx, r10
r15, 0x78
r14, rbp
r9, 8
r14, 0x29
rbx, rdi
r15, 0x3f
byte ptr [r14], r10b
rax, 0x58
r8, rbprsi, 0x78
r8, 0x127
rdi, rbx
rbx, 0x3f
r8, qword ptr [r8]rsi, 1rax, rbp

add
or
and
add
add
or
mov
and
add
sub
or
movzx
mov
mov
mov
add
or
add
xor
add
add
mov
or
add
or
add
mov
add
and
or
and
and
mov
add
or
shl
add
or
sub
or
mov
mov
sub
add
add
jmp

r15, 0x3f
r15, 0xffffffff80000000
rsi, r9rax, 0xc0
rdi, r14
rsi, 1rax, qword ptr [rax]rdi, 0x7fffffffrax, 2
rsi, 4rbx, rsi
rax, word ptr [rax]r9, rbp
r13, 0x200
r10, 0x58r9, 0r10, 0x20
eax, dword ptr [r9]r10, 0x40
eax, 0x3f505c07
r15, 0x88
r12, rbp
rdi, 0x90
r12, 0rbx, 0x80
rdi, 0xf0
r13, 0x400
dword ptr [r12], eax
rsi, r8
r10, 8rbx, 0x20
rax, 0xffff
r11, 0r13, r8
rbx, 1rax, 3r8, raxrbx, r15
r15, 0x10
r11, r13
rbx, qword ptr [r8]rdx, rbp
r13, 0x80
rdx, 0xc0
qword ptr [rdx], 0xd
rbx

56

#5: Blinding VM Bytecodemovr15, 0x200
xor
r15, 0x800
mov
rbx, rbp
add
rbx, 0xc0
mov
rbx, qword ptr [rbx]movr13, 1movrcx, 0mov
r15, rbp
add
r15, 0xc0
or
rcx, 0x88
add
rbx, 0xb
mov
r15, qword ptr [r15]orr12, 0xffffffff80000000
subrcx, 0x78
movzx r10, word ptr [rbx]xor
r12, r13
add
r12, 0xffff
addr15, 0mov
r8, rbpsubrcx, 0x10
orr12, r12orrcx, 0x800
movzx r11, word ptr [r15]xorrcx, 0x800
mov
r12, r15
add
r8, 0
xor
r12, 0xf0
mov
rbx, 0x58
add
r11, rbp
xor
rbx, 0x800
andr12, 0x20
add
rbx, 0x800
mov
r11, qword ptr [r11]addrbx, 1andr12, r9movrdx, 1xor
r10d, dword ptr [r8]sub
r9, r11
pushfqxor
rbx, 0xf0
xor
rbx, 0x800
andrdx, r8movr12, rbp
xor
rdx, 0x20
subrbx, 4add
r11, 0x2549b044
orrbx, 0x78
andrdx, r10
movrax, 0add
r12, 0x42

mov
xor
sub
or
mov
mov
sub
mov
mov
sub
sub
add
add
and
xor
mov
add
sub
add
add
mov
mov
add
xor
add
add
mov
mov
mov
mov
and
sub
mov
add
or
mov
add
mov
cmp
jbe
and
or
or
mov
or
sub
add
or
add
add

r15, rdxadd
r10d, dword ptr [r12]orr15, 0x800
addrdx, 0x400
mov
rsi, 0x200
sub
r14, rbp
pop
rsi, rsimovrdi, rbp
add
r8, 0x400
mov
rsi, r9
add
r8, rsimovzx
r14, 0movrsi, raxadd
r8, 0x88
xor
rsi, r14andrsi, rbp
subrdi, 0xc0
mov
r8, rdisub
r8, 0x78
movrsi, 4orrcx, 0x200
andrdi, qword ptr [rdi]movdword ptr [rsi], 0x2549b044 add
rcx, 0xf0
mov
rcx, r10
subrdi, 6add
r8, 0x400
sub
ax, word ptr [rdi]
add
r8, 1
mov
rsi, rbp
orrcx, 8sub
rcx, 1movrcx, rdimovrsi, 0x29
add
rcx, 8sub
r8, rsimovrcx, 4or
r13b, byte ptr [rsi]xor
r13b, 0xd2
mov
0x204
add
r8, r13sub
rcx, r13xor
rcx, 4xor
rbx, rbp
add
rcx, 4mov
rcx, 0x400
mov
rax, rbp
add
rcx, 0x80
add
rcx, 0x80
xor
rbx, 0x5a
mov

mov
…
add
…
add
…
add
…
mov
…
add
add

or
r14, r14
r8, 1
mov
rax, rbp
r8, 0x78
andrcx, r13
word ptr [rbx], r10w
add
rax, 4r15, raxsub
r8, -0x80000000
r15, raxadd
r13, 0xffff
r9
andrcx, 0x20
rcx, rbp
movr10, rbp
rcx, 0xc0
add
r13, r15
rcx, qword ptr [rcx]add
r14, r8
rcx, 8add
r10, 0x89
r10, word ptr [rcx]xorword ptr [r10], si
r9, rbpxor
rdx, r11
r9, 0
mov
rsi, rbp
r10d, dword ptr [r9]rdx, rbx
rdi, 0xffffffff80000000 sub
andrax, 0x40
r13, 0xf0
or
rbx, 0xf0
rsi, 0add
rsi, 0x5ar13, 0x20
mov
r8, rcx
rbx, rbp
movzx rsi, word ptr [rsi]r13, 0x88
movrax, 0x200
rcx, 8mov
r14, rbp
r8, 0x58
andrax, rdx
rbx, 0xc0
and
rcx, 0x20
rbx, qword ptr [rbx]add
r14, 0x89
rcx, 0x20
orrax, 0x40
rdi, 0x80
xor
si, 0x7a28
r13, 0x10
add
rdx, 0x78
rbx, 8add
rdx, 0x20
si, word ptr [rbx]movzx r14, word ptr [r14]r9, 0xffff
mov
rcx, 0x58
r9, 1
add
rsi, rbp
r9, rbpxor
rax, rdx
r12, 0x58
add
r8, 0x80
r9, 0
mov
r15, rsi
r13, 0x80
add
r14, rbp
r15, r13
add
r8, r15
rcx, r12
movrbx, 0esi, dword ptr [r9]andrdx, 0x10
r10, rbp
mov
r14, qword ptr [r14]r10, 0xcc
add
qword ptr [rsi], r14
r15, 0x20
pushfqesi, dword ptr [r10]xor
r11, r14
r13, 0x90
addr15, r14
rdi, 0x10
mov
r13, 0x12
r14, rsi
movr8, 0rdx, rbp
andr14, 0x88
rdx, 0and
r13, 0x40
dword ptr [rdx], esi
addr13, 1
r12, 1movrdx, rbp
r13, r15

r9, rbp
r9, 0

eax, dword ptr [r9]eax, 0x3f505c07

mov
add
add
or
mov
add
add
mov
cmp
je
mov
or
and
xor
add
or
mov
mov
sub
add
or
mov
mov
add
xor
pop
mov
jmp
xor
xor
add
mov
mov
or
and
mov
or
add
xor
and
or
mov
mov
sub
add
mov
xor
mov
xor
mov

r14, 0x200
rdx, 0xc0
r11, r14
r15, 0x88
rdx, qword ptr [rdx]rdx, 0xa
r11, 0x78
r8b, byte ptr [rdx]r8b, 00x49erdx, rbp
r11, 0x40
r15, 1
r11, 0x10
rdx, 0xc0
r14, 4r15, 0x12
rdx, qword ptr [rdx]r11, r8rdx, 4r11, 0x80
r8w, word ptr [rdx]r14, r8
r8, rbp
r13, 4r10
qword ptr [r8], r10
0x4ae
rsi, 0x88
rbx, 0xffffffff80000000
rsi, 0x78
r10b, 0x68
r9, 0x12
rbx, r10
r15, 0x78
r14, rbp
r9, 8
r14, 0x29
rbx, rdi
r15, 0x3f
byte ptr [r14], r10b
rax, 0x58
r8, rbprsi, 0x78
r8, 0x127
rdi, rbx
rbx, 0x3f
r8, qword ptr [r8]rsi, 1rax, rbp

add
or
and
add
add
or
mov
and
add
sub
or
movzx
mov
mov
mov
add
or
add
xor
add
add
mov
or
add
or
add
mov
add
and
or
and
and
mov
add
or
shl
add
or
sub
or
mov
mov
sub
add
add
jmp

r15, 0x3f
r15, 0xffffffff80000000
rsi, r9rax, 0xc0
rdi, r14
rsi, 1rax, qword ptr [rax]rdi, 0x7fffffffrax, 2
rsi, 4rbx, rsi
rax, word ptr [rax]r9, rbp
r13, 0x200
r10, 0x58r9, 0r10, 0x20
eax, dword ptr [r9]r10, 0x40
eax, 0x3f505c07
r15, 0x88
r12, rbp
rdi, 0x90
r12, 0rbx, 0x80
rdi, 0xf0
r13, 0x400
dword ptr [r12], eax
rsi, r8
r10, 8rbx, 0x20
rax, 0xffff
r11, 0r13, r8
rbx, 1rax, 3r8, raxrbx, r15
r15, 0x10
r11, r13
rbx, qword ptr [r8]rdx, rbp
r13, 0x80
rdx, 0xc0
qword ptr [rdx], 0xd
rbx

r12, rbp
No inﬂuence on underlyingcode’s semantics
r12, 0dword ptr [r12], eax

56

#3: No Central VM Dispatchermovr15, 0x200
xor
r15, 0x800
mov
rbx, rbp
add
rbx, 0xc0
mov
rbx, qword ptr [rbx]movr13, 1movrcx, 0mov
r15, rbp
add
r15, 0xc0
or
rcx, 0x88
add
rbx, 0xb
mov
r15, qword ptr [r15]orr12, 0xffffffff80000000
subrcx, 0x78
movzx r10, word ptr [rbx]xor
r12, r13
add
r12, 0xffff
addr15, 0mov
r8, rbpsubrcx, 0x10
orr12, r12orrcx, 0x800
movzx r11, word ptr [r15]xorrcx, 0x800
mov
r12, r15
add
r8, 0
xor
r12, 0xf0
mov
rbx, 0x58
add
r11, rbp
xor
rbx, 0x800
andr12, 0x20
add
rbx, 0x800
mov
r11, qword ptr [r11]addrbx, 1andr12, r9movrdx, 1xor
r10d, dword ptr [r8]sub
r9, r11
pushfqxor
rbx, 0xf0
xor
rbx, 0x800
andrdx, r8movr12, rbp
xor
rdx, 0x20
subrbx, 4add
r11, 0x2549b044
orrbx, 0x78
andrdx, r10
movrax, 0add
r12, 0x42

mov
xor
sub
or
mov
mov
sub
mov
mov
sub
sub
add
add
and
xor
mov
add
sub
add
add
mov
mov
add
xor
add
add
mov
mov
mov
mov
and
sub
mov
add
or
mov
add
mov
cmp
jbe
and
or
or
mov
or
sub
add
or
add
add

add
r15, rdxor
r10d, dword ptr [r12]add
r15, 0x800
mov
rdx, 0x400
subrsi, 0x200
pop
r14, rbp
movrsi, rsi
addrdi, rbp
mov
r8, 0x400
addrsi, r9
movzx
r8, rsimovr14, 0add
rsi, raxxor
r8, 0x88
andrsi, r14
subrsi, rbp
movrdi, 0xc0
subr8, rdimov
r8, 0x78
orrsi, 4andrcx, 0x200
mov
rdi, qword ptr [rdi]dword ptr [rsi], 0x2549b044 add
movrcx, 0xf0
subrcx, r10
add
rdi, 6
sub
r8, 0x400
add
ax, word ptr [rdi]
mov
r8, 1
or
rsi, rbp
subrcx, 8mov
rcx, 1movrcx, rdiaddrsi, 0x29
subrcx, 8mov
r8, rsiorrcx, 4xor
r13b, byte ptr [rsi]movr13b, 0xd2
add
0x204
sub
r8, r13xor
rcx, r13xor
rcx, 4add
rbx, rbp
movrcx, 4mov
rcx, 0x400
add
rax, rbp
add
rcx, 0x80
xor
rcx, 0x80
mov
rbx, 0x5aor
r14, r14
r8, 1
mov
rax, rbp
r8, 0x78
andrcx, r13
word ptr [rbx], r10w
add
rax, 4r15, raxsub
r8, -0x80000000
r15, raxadd
r13, 0xffff
r9
andrcx, 0x20
rcx, rbp
movr10, rbp
rcx, 0xc0
add
r13, r15
rcx, qword ptr [rcx]add
r14, r8
rcx, 8add
r10, 0x89
r10, word ptr [rcx]xorword ptr [r10], si
r9, rbpxor
rdx, r11
r9, 0
mov
rsi, rbp
r10d, dword ptr [r9]rdx, rbx
rdi, 0xffffffff80000000 sub
andrax, 0x40
r13, 0xf0
or
rbx, 0xf0
rsi, 0add
rsi, 0x5ar13, 0x20
mov
r8, rcx
rbx, rbp
movzx rsi, word ptr [rsi]r13, 0x88
movrax, 0x200
rcx, 8mov
r14, rbp
r8, 0x58
andrax, rdx
rbx, 0xc0
and
rcx, 0x20
rbx, qword ptr [rbx]add
r14, 0x89
rcx, 0x20
orrax, 0x40
rdi, 0x80
xor
si, 0x7a28
r13, 0x10
add
rdx, 0x78
rbx, 8add
rdx, 0x20
si, word ptr [rbx]movzx r14, word ptr [r14]r9, 0xffff
mov
rcx, 0x58
r9, 1
add
rsi, rbp
r9, rbpxor
rax, rdx
r12, 0x58
add
r8, 0x80
r9, 0
mov
r15, rsi
r13, 0x80
add
r14, rbp
r15, r13
add
r8, r15
rcx, r12
movrbx, 0esi, dword ptr [r9]andrdx, 0x10
r10, rbp
mov
r14, qword ptr [r14]r10, 0xcc
add
qword ptr [rsi], r14
r15, 0x20
pushfqesi, dword ptr [r10]xor
r11, r14
r13, 0x90
addr15, r14
rdi, 0x10
mov
r13, 0x12
r14, rsi
movr8, 0rdx, rbp
andr14, 0x88
rdx, 0and
r13, 0x40
dword ptr [rdx], esi
addr13, 1
r12, 1movrdx, rbp
r13, r15

mov
add
add
or
mov
add
add
mov
cmp
je
mov
or
and
xor
add
or
mov
mov
sub
add
or
mov
mov
add
xor
pop
mov
jmp
xor
xor
add
mov
mov
or
and
mov
or
add
xor
and
or
mov
mov
sub
add
mov
xor
mov
xor
mov

r14, 0x200
rdx, 0xc0
r11, r14
r15, 0x88
rdx, qword ptr [rdx]rdx, 0xa
r11, 0x78
r8b, byte ptr [rdx]r8b, 00x49erdx, rbp
r11, 0x40
r15, 1
r11, 0x10
rdx, 0xc0
r14, 4r15, 0x12
rdx, qword ptr [rdx]r11, r8rdx, 4r11, 0x80
r8w, word ptr [rdx]r14, r8
r8, rbp
r13, 4r10
qword ptr [r8], r10
0x4ae
rsi, 0x88
rbx, 0xffffffff80000000
rsi, 0x78
r10b, 0x68
r9, 0x12
rbx, r10
r15, 0x78
r14, rbp
r9, 8
r14, 0x29
rbx, rdi
r15, 0x3f
byte ptr [r14], r10b
rax, 0x58
r8, rbprsi, 0x78
r8, 0x127
rdi, rbx
rbx, 0x3f
r8, qword ptr [r8]rsi, 1rax, rbp

add
or
and
add
add
or
mov
and
add
sub
or
movzx
mov
mov
mov
add
or
add
xor
add
add
mov
or
add
or
add
mov
add
and
or
and
and
mov
add
or
shl
add
or
sub
or
mov
mov
sub
add
add
jmp

r15, 0x3f
r15, 0xffffffff80000000
rsi, r9rax, 0xc0
rdi, r14
rsi, 1rax, qword ptr [rax]rdi, 0x7fffffffrax, 2
rsi, 4rbx, rsi
rax, word ptr [rax]r9, rbp
r13, 0x200
r10, 0x58r9, 0r10, 0x20
eax, dword ptr [r9]r10, 0x40
eax, 0x3f505c07
r15, 0x88
r12, rbp
rdi, 0x90
r12, 0rbx, 0x80
rdi, 0xf0
r13, 0x400
dword ptr [r12], eax
rsi, r8
r10, 8rbx, 0x20
rax, 0xffff
r11, 0r13, r8
rbx, 1rax, 3r8, raxrbx, r15
r15, 0x10
r11, r13
rbx, qword ptr [r8]rdx, rbp
r13, 0x80
rdx, 0xc0
qword ptr [rdx], 0xd
rbx

57#3: No Central VM Dispatchermovr15, 0x200
xor
r15, 0x800
mov
rbx, rbp
add
rbx, 0xc0
mov
rbx, qword ptr [rbx]movr13, 1movrcx, 0mov
r15, rbp
add
r15, 0xc0
or
rcx, 0x88
add
rbx, 0xb
mov
r15, qword ptr [r15]orr12, 0xffffffff80000000
subrcx, 0x78
movzx r10, word ptr [rbx]xor
r12, r13
add
r12, 0xffff
addr15, 0mov
r8, rbpsubrcx, 0x10
orr12, r12orrcx, 0x800
movzx r11, word ptr [r15]xorrcx, 0x800
mov
r12, r15
add
r8, 0
xor
r12, 0xf0
mov
rbx, 0x58
add
r11, rbp
xor
rbx, 0x800
andr12, 0x20
add
rbx, 0x800
mov
r11, qword ptr [r11]addrbx, 1andr12, r9movrdx, 1xor
r10d, dword ptr [r8]sub
r9, r11
pushfqxor
rbx, 0xf0
xor
rbx, 0x800
andrdx, r8movr12, rbp
xor
rdx, 0x20
subrbx, 4add
r11, 0x2549b044
orrbx, 0x78
andrdx, r10
movrax, 0add
r12, 0x42

mov
xor
sub
or
mov
mov
sub
mov
mov
sub
sub
add
add
and
xor
mov
add
sub
add
add
mov
mov
add
xor
add
add
mov
mov
mov
mov
and
sub
mov
add
or
mov
add
mov
cmp
jbe
and
or
or
mov
or
sub
add
or
add
add

add
r15, rdxor
r10d, dword ptr [r12]add
r15, 0x800
mov
rdx, 0x400
subrsi, 0x200
pop
r14, rbp
movrsi, rsi
addrdi, rbp
mov
r8, 0x400
addrsi, r9
movzx
r8, rsimovr14, 0add
rsi, raxxor
r8, 0x88
andrsi, r14
subrsi, rbp
movrdi, 0xc0
subr8, rdimov
r8, 0x78
orrsi, 4andrcx, 0x200
mov
rdi, qword ptr [rdi]dword ptr [rsi], 0x2549b044 add
movrcx, 0xf0
subrcx, r10
add
rdi, 6
sub
r8, 0x400
add
ax, word ptr [rdi]
mov
r8, 1
or
rsi, rbp
subrcx, 8mov
rcx, 1movrcx, rdiaddrsi, 0x29
subrcx, 8mov
r8, rsiorrcx, 4xor
r13b, byte ptr [rsi]movr13b, 0xd2
add
0x204
sub
r8, r13xor
rcx, r13xor
rcx, 4add
rbx, rbp
movrcx, 4mov
rcx, 0x400
add
rax, rbp
add
rcx, 0x80
xor
rcx, 0x80
mov
rbx, 0x5a

or
shl
add
or
sub
or
mov
mov
sub
add
add
jmp

or
r14, r14
r8, 1
mov
rax, rbp
r8, 0x78
andrcx, r13
word ptr [rbx], r10w
add
rax, 4r15, raxsub
r8, -0x80000000
r15, raxadd
r13, 0xffff
r9
andrcx, 0x20
rcx, rbp
movr10, rbp
rcx, 0xc0
add
r13, r15
rcx, qword ptr [rcx]add
r14, r8
rcx, 8add
r10, 0x89
r10, word ptr [rcx]xorword ptr [r10], si
r9, rbpxor
rdx, r11
r9, 0
mov
rsi, rbp
r10d, dword ptr [r9]rdx, rbx
rdi, 0xffffffff80000000 sub
andrax, 0x40
r13, 0xf0
or
rbx, 0xf0
rsi, 0add
rsi, 0x5ar13, 0x20
mov
r8, rcx
rbx, rbp
movzx rsi, word ptr [rsi]r13, 0x88
movrax, 0x200
rcx, 8mov
r14, rbp
r8, 0x58
andrax, rdx
rbx, 0xc0
and
rcx, 0x20
rbx, qword ptr [rbx]add
r14, 0x89
rcx, 0x20
orrax, 0x40
rdi, 0x80
xor
si, 0x7a28
r13, 0x10
add
rdx, 0x78
rbx, 8add
rdx, 0x20
si, word ptr [rbx]movzx r14, word ptr [r14]r9, 0xffff
mov
rcx, 0x58
r9, 1
add
rsi, rbp
r9, rbpxor
rax, rdx
r12, 0x58
add
r8, 0x80
r9, 0
mov
r15, rsi
r13, 0x80
add
r14, rbp
r15, r13
add
r8, r15
rcx, r12
movrbx, 0esi, dword ptr [r9]andrdx, 0x10
r10, rbp
mov
r14, qword ptr [r14]r10, 0xcc
add
qword ptr [rsi], r14
r15, 0x20
pushfqesi, dword ptr [r10]xor
r11, r14
r13, 0x90
addr15, r14
rdi, 0x10
mov
r13, 0x12
r14, rsi
movr8, 0rdx, rbp
andr14, 0x88
rdx, 0and
r13, 0x40
dword ptr [rdx], esi
addr13, 1
r12, 1movrdx, rbp
r13, r15

rbx, 1rax, 3r8, raxrbx, r15
r15, 0x10
r11, r13
rbx, qword ptr [r8]rdx, rbp
r13, 0x80
rdx, 0xc0
qword ptr [rdx], 0xd
rbx

mov
add
add
or
mov
add
add
mov
cmp
je
mov
or
and
xor
add
or
mov
mov
sub
add
or
mov
mov
add
xor
pop
mov
jmp
xor
xor
add
mov
mov
or
and
mov
or
add
xor
and
or
mov
mov
sub
add
mov
xor
mov
xor
mov

r14, 0x200
rdx, 0xc0
r11, r14
r15, 0x88
rdx, qword ptr [rdx]rdx, 0xa
r11, 0x78
r8b, byte ptr [rdx]r8b, 00x49erdx, rbp
r11, 0x40
r15, 1
r11, 0x10
rdx, 0xc0
r14, 4r15, 0x12
rdx, qword ptr [rdx]r11, r8rdx, 4r11, 0x80
r8w, word ptr [rdx]r14, r8
r8, rbp
r13, 4r10
qword ptr [r8], r10
0x4ae
rsi, 0x88
rbx, 0xffffffff80000000
rsi, 0x78
r10b, 0x68
r9, 0x12
rbx, r10
r15, 0x78
r14, rbp
r9, 8
r14, 0x29
rbx, rdi
r15, 0x3f
byte ptr [r14], r10b
rax, 0x58
r8, rbprsi, 0x78
r8, 0x127
rdi, rbx
rbx, 0x3f
r8, qword ptr [r8]rsi, 1rax, rbp

add
or
and
add
add
or
mov
and
add
sub
or
movzx
mov
mov
mov
add
or
add
xor
add
add
mov
or
add
or
add
mov
add
and
or
and
and
mov
add
or
shl
add
or
sub
or
mov
mov
sub
add
add
jmp

r15, 0x3f
r15, 0xffffffff80000000
rsi, r9rax, 0xc0
rdi, r14
rsi, 1rax, qword ptr [rax]rdi, 0x7fffffffrax, 2
rsi, 4rbx, rsi
rax, word ptr [rax]r9, rbp
r13, 0x200
r10, 0x58r9, 0r10, 0x20
eax, dword ptr [r9]r10, 0x40
eax, 0x3f505c07
r15, 0x88
r12, rbp
rdi, 0x90
r12, 0rbx, 0x80
rdi, 0xf0
r13, 0x400
dword ptr [r12], eax
rsi, r8
r10, 8rbx, 0x20
rax, 0xffff
r11, 0r13, r8
rbx, 1rax, 3r8, raxrbx, r15
r15, 0x10
r11, r13
rbx, qword ptr [r8]rdx, rbp
r13, 0x80
rdx, 0xc0
qword ptr [rdx], 0xd
rbx

57#3: No Central VM Dispatchermovr15, 0x200
xor
r15, 0x800
mov
rbx, rbp
add
rbx, 0xc0
mov
rbx, qword ptr [rbx]movr13, 1movrcx, 0mov
r15, rbp
add
r15, 0xc0
or
rcx, 0x88
add
rbx, 0xb
mov
r15, qword ptr [r15]orr12, 0xffffffff80000000
subrcx, 0x78
movzx r10, word ptr [rbx]xor
r12, r13
add
r12, 0xffff
addr15, 0mov
r8, rbpsubrcx, 0x10
orr12, r12orrcx, 0x800
movzx r11, word ptr [r15]xorrcx, 0x800
mov
r12, r15
add
r8, 0
xor
r12, 0xf0
mov
rbx, 0x58
add
r11, rbp
xor
rbx, 0x800
andr12, 0x20
add
rbx, 0x800
mov
r11, qword ptr [r11]addrbx, 1andr12, r9movrdx, 1xor
r10d, dword ptr [r8]sub
r9, r11
pushfqxor
rbx, 0xf0
xor
rbx, 0x800
andrdx, r8movr12, rbp
xor
rdx, 0x20
subrbx, 4add
r11, 0x2549b044
orrbx, 0x78
andrdx, r10
movrax, 0add
r12, 0x42

mov
xor
sub
or
mov
mov
sub
mov
mov
sub
sub
add
add
and
xor
mov
add
sub
add
add
mov
mov
add
xor
add
add
mov
mov
mov
mov
and
sub
mov
add
or
mov
add
mov
cmp
jbe
and
or
or
mov
or
sub
add
or
add
add

add
r15, rdxor
r10d, dword ptr [r12]add
r15, 0x800
mov
rdx, 0x400
subrsi, 0x200
pop
r14, rbp
movrsi, rsi
addrdi, rbp
mov
r8, 0x400
addrsi, r9
movzx
r8, rsimovr14, 0add
rsi, raxxor
r8, 0x88
andrsi, r14
subrsi, rbp
movrdi, 0xc0
subr8, rdimov
r8, 0x78
orrsi, 4andrcx, 0x200
mov
rdi, qword ptr [rdi]dword ptr [rsi], 0x2549b044 add
movrcx, 0xf0
subrcx, r10
add
rdi, 6
sub
r8, 0x400
add
ax, word ptr [rdi]
mov
r8, 1
or
rsi, rbp
subrcx, 8mov
rcx, 1movrcx, rdiaddrsi, 0x29
subrcx, 8mov
r8, rsiorrcx, 4xor
r13b, byte ptr [rsi]movr13b, 0xd2
add
0x204
sub
r8, r13xor
rcx, r13xor
rcx, 4add
rbx, rbp
movrcx, 4mov
rcx, 0x400
add
rax, rbp
add
rcx, 0x80
xor
rcx, 0x80
mov
rbx, 0x5a

or
shl
add
or
sub
or
mov
mov
sub
add
add
jmp

or
r14, r14
r8, 1
mov
rax, rbp
r8, 0x78
andrcx, r13
word ptr [rbx], r10w
add
rax, 4r15, raxsub
r8, -0x80000000
r15, raxadd
r13, 0xffff
r9
andrcx, 0x20
rcx, rbp
movr10, rbp
rcx, 0xc0
add
r13, r15
rcx, qword ptr [rcx]add
r14, r8
rcx, 8add
r10, 0x89
r10, word ptr [rcx]xorword ptr [r10], si
r9, rbpxor
rdx, r11
r9, 0
mov
rsi, rbp
r10d, dword ptr [r9]rdx, rbx
rdi, 0xffffffff80000000 sub
andrax, 0x40
r13, 0xf0
or
rbx, 0xf0
rsi, 0add
rsi, 0x5ar13, 0x20
mov
r8, rcx
rbx, rbp
movzx rsi, word ptr [rsi]r13, 0x88
movrax, 0x200
rcx, 8mov
r14, rbp
r8, 0x58
andrax, rdx
rbx, 0xc0
and
rcx, 0x20
rbx, qword ptr [rbx]add
r14, 0x89
rcx, 0x20
orrax, 0x40
rdi, 0x80
xor
si, 0x7a28
r13, 0x10
add
rdx, 0x78
rbx, 8add
rdx, 0x20
si, word ptr [rbx]movzx r14, word ptr [r14]r9, 0xffff
mov
rcx, 0x58
r9, 1
add
rsi, rbp
r9, rbpxor
rax, rdx
r12, 0x58
add
r8, 0x80
r9, 0
mov
r15, rsi
r13, 0x80
add
r14, rbp
r15, r13
add
r8, r15
rcx, r12
movrbx, 0esi, dword ptr [r9]andrdx, 0x10
r10, rbp
mov
r14, qword ptr [r14]r10, 0xcc
add
qword ptr [rsi], r14
r15, 0x20
pushfqesi, dword ptr [r10]xor
r11, r14
r13, 0x90
addr15, r14
rdi, 0x10
mov
r13, 0x12
r14, rsi
movr8, 0rdx, rbp
andr14, 0x88
rdx, 0and
r13, 0x40
dword ptr [rdx], esi
addr13, 1
r12, 1movrdx, rbp
r13, r15

rbx, 1rax, 3r8, raxrbx, r15
r15, 0x10
r11, r13
rbx, qword ptr [r8]rdx, rbp
r13, 0x80
rdx, 0xc0
qword ptr [rdx], 0xd
rbx

mov
add
add
or
mov
add
add
mov
cmp
je
mov
or
and
xor
add
or
mov
mov
sub
add
or
mov
mov
add
xor
pop
mov
jmp
xor
xor
add
mov
mov
or
and
mov
or
add
xor
and
or
mov
mov
sub
add
mov
xor
mov
xor
mov

r14, 0x200
rdx, 0xc0
r11, r14
r15, 0x88
rdx, qword ptr [rdx]rdx, 0xa
r11, 0x78
r8b, byte ptr [rdx]r8b, 00x49erdx, rbp
r11, 0x40
r15, 1
r11, 0x10
rdx, 0xc0
r14, 4r15, 0x12
rdx, qword ptr [rdx]r11, r8rdx, 4r11, 0x80
r8w, word ptr [rdx]r14, r8
r8, rbp
r13, 4r10
qword ptr [r8], r10
0x4ae
rsi, 0x88
rbx, 0xffffffff80000000
rsi, 0x78
r10b, 0x68
r9, 0x12
rbx, r10
r15, 0x78
r14, rbp
r9, 8
r14, 0x29
rbx, rdi
r15, 0x3f
byte ptr [r14], r10b
rax, 0x58
r8, rbprsi, 0x78
r8, 0x127
rdi, rbx
rbx, 0x3f
r8, qword ptr [r8]rsi, 1rax, rbp

Split at indirect control-ﬂow transfers

add
or
and
add
add
or
mov
and
add
sub
or
movzx
mov
mov
mov
add
or
add
xor
add
add
mov
or
add
or
add
mov
add
and
or
and
and
mov
add
or
shl
add
or
sub
or
mov
mov
sub
add
add
jmp

r15, 0x3f
r15, 0xffffffff80000000
rsi, r9rax, 0xc0
rdi, r14
rsi, 1rax, qword ptr [rax]rdi, 0x7fffffffrax, 2
rsi, 4rbx, rsi
rax, word ptr [rax]r9, rbp
r13, 0x200
r10, 0x58r9, 0r10, 0x20
eax, dword ptr [r9]r10, 0x40
eax, 0x3f505c07
r15, 0x88
r12, rbp
rdi, 0x90
r12, 0rbx, 0x80
rdi, 0xf0
r13, 0x400
dword ptr [r12], eax
rsi, r8
r10, 8rbx, 0x20
rax, 0xffff
r11, 0r13, r8
rbx, 1rax, 3r8, raxrbx, r15
r15, 0x10
r11, r13
rbx, qword ptr [r8]rdx, rbp
r13, 0x80
rdx, 0xc0
qword ptr [rdx], 0xd
rbx

57#4: No Explicit Handler Table58

#4: No Explicit Handler Table58

#4: No Explicit Handler Table

vm_nor32
vm_add64

vm_add64

vm_add64

vm_mul32

vm_mul32

vm_nor32
vm_nor32
vm_nor32

58

Conclusion

Take Aways

1. syntactic complexity insigniﬁcant60

Take Aways

1. syntactic complexity insigniﬁcant
2. semantic complexity low within speciﬁed boundaries

60

Take Aways

1. syntactic complexity insigniﬁcant
2. semantic complexity low within speciﬁed boundaries
3. learn underlying code’s semantics despite obfuscation

60

Take Aways

1. syntactic complexity insigniﬁcant
2. semantic complexity low within speciﬁed boundaries
3. learn underlying code’s semantics despite obfuscation

Program Synthesis as an orthogonal approach to traditional techniques60

Limitations

Implementation Shortcomings
choosing meaningful code window boundaries(x ⊕ y) + 2 · (x ∧ y)vs.

(x ⊕ y) + 2

constants
x + 15324326921

control-ﬂow operations
x ? y : z62

Limitations

(1,1)

(1,1)

?
?

2

4

non-determinism

63

Limitations

(1,1)

(1,1)

?
?

2

4

AES

non-determinism
semantic complexity
63Limitations

(1,1)

(1,1)

?
?

x

2

{

1,
0,

x �� constantotherwise0

point functions

4

AES

non-determinism
semantic complexity
63

Do try it at home!

Summary• obfuscation techniques (opaque predicates, VM, MBA)• symbolic execution for syntactic deobfuscation• program synthesis for semantic deobfuscation

https://github.com/RUB-SysSec/syntia

65