HAI DOMO. This post is for 武蔵野 Advent Calendar 2017 and also for CTF Advent Calendar 2017.

Introduction

In May this year, I participated in DEF CON CTF Qualifier 2017 as a member of a certain 武蔵野-related team. Actually, I’m not a top-tier CTF player, but I did my best and solved 4 challenges:

  • crackme1
  • beatmeonthedl
  • enlightenment
  • Pepperidge Farm

Write-ups already exist except for Pepperidge Farm. So I decided to write about it. FYI: The binaries are available at legitbs/quals-2017.

Pepperidge Farm

Pepperidge Farm is categorized into Reverse Engineering. The problem statement is below:

Remember when the first CTF was run with a custom architecture? Pepperidge Farm remembers:
https://github.com/JonathanSalwan/VMNDH-2k12

pepperidge-farm_edb4ad2f103a9efde038346d2cd86a1e.quals.shallweplayaga.me:2012

Files
https://2017.notmalware.ru/8a45cf7171e89594cfd1d51671fef0bec3f24d9d/pepperidge_farm

It seems like a keygenning challenge on the custom virtual machine–VMNDH-2k12.

1
2
3
$ ./vmndh -file pepperidge_farm
Enter your registration code: 31337
Code does not match any known registered users

VMNDH-2k12

VMNDH-2k12 is the VM built for Nuit du Hack CTF Quals 2012 as its name suggests. The architecture is described in shell-storm | Useless emulator for fun (VMNDH-2k12). This VM parses given serialized binary and repeats fetch, decode and execution.

Writing IDA loader/processor module is a common way to analyze VM-based obfuscated binary. The modules for VMNDH-2k12 and for modified version VMNDH-2k13 already exist:

Note that when you try to solve this challenge with above-mentioned processor modules with IDA Pro 7.0, the backward-compatibility issue will occur. For example, you have to change self.regFirstSreg toself.reg_first_sreg in a module.

Also, the Binary Ninja plugin has been released after quals:

But in this post, I describe a solution without both IDA Pro and Binary Ninja. Because VMNDH-2k12 is open-sourced and easy to modify.

Surface Analysis

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
$ ./vmndh -debug -file pepperidge_farm
[Console]#> help
<enter> Execute next instruction
run Run program
bp <addr> Set breakpoint
info bp Display info breakpoint
info reg Display registers
show sp Display SP memory
show pc Display PC memory
dis <addr>:<size> Disassembly X bytes from ADDR
x/x <addr>:<size> Print X bytes from ADDR
x/s <addr> Print string addr
set reg=value Set value in register
syscall Execute 'syscall' instruction
help Display this help
quit Quit console debugging
[Console]#> dis
Error: Set addr between 0x8000 and 0x882a
[Console]#> dis 0x8000:82a
0x8000: jmpl 0x0720
0x8003: push r2
0x8007: .byte 0x00
0x8008: nop
...

Yes, the VM has own debugger and disassembler.

Modifying the Disassembler

However, there are pitfalls here.

Because it is a unique architecture, the destination of the control flow instructions are different from it shown on the disassembly dump. For example, take a look at src_vm/op_call.c:

1
2
3
4
5
6
7
8
9
10
11
12
static void op_call_dir16(void)
{
uint16_t operande;
operande = *(uint16_t *)(core.memory.vmem + core.memory.pc + 2);
if (core.flagmode.noverbose == 0)
fprintf(stdout, "%s0x%4.x%s > call 0x%.2x\n", RED, core.memory.pc, ENDC, operande);
core.memory.sp -= 2; /* sub sp */
*(uint16_t *)(core.memory.vmem + core.memory.sp) = core.memory.pc + 4;
core.memory.pc = core.memory.pc + operande + 4;
}

Acording to this, I modified the dissassembler in src_vm/disass.c:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
@@ -532,6 +537,7 @@
uint16_t operande;
uint8_t reg;
char flag;
+ uint16_t dst;
flag = *(core.memory.vmem + addr + 1);
switch (flag)
@@ -543,7 +549,8 @@
case OP_FLAG_DIRECT16:
operande = *(uint16_t *)(core.memory.vmem + addr + 2);
- fprintf(stdout, "%s0x%.4x%s: call 0x%.4x\n", RED, addr, ENDC, operande);
+ dst = addr + operande + 4;
+ fprintf(stdout, "%s0x%.4x%s: call 0x%.4x\n", RED, addr, ENDC, dst);
return (addr + 4);
default:

This makes it possible to correctly display the address of the call destination in the disassembly dump. In addition, jump instructions need to be modified. In the case of jnz:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
@@ -463,10 +470,11 @@
static uint16_t dis_jnz(uint16_t addr)
{
- uint16_t operande;
+ uint16_t operande, dst;
operande = *(uint16_t *)(core.memory.vmem + addr + 1);
- fprintf(stdout, "%s0x%.4x%s: jnz 0x%.4x\n", RED, addr, ENDC, operande);
+ dst = addr + operande + 3;
+ fprintf(stdout, "%s0x%.4x%s: jnz 0x%.4x\n", RED, addr, ENDC, dst);
return (addr + 3);
}

Herewith,

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
0x86a1: jnz 0x0076
0x86a4: mov r0, r2
0x86a8: call 0xfdc5
0x86ac: test r0, r0
0x86af: jnz 0x0068
0x86b2: mov r0, r2
0x86b6: call 0xfddf
0x86ba: test r0, r0
0x86bd: jnz 0x005a
0x86c0: mov r0, r2
0x86c4: call 0xfe17
0x86c8: test r0, r0
0x86cb: jnz 0x004c
0x86ce: mov r0, r2
0x86d2: call 0xfe2c
0x86d6: test r0, r0
...

becomes:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
0x86a1: jnz 0x871a
0x86a4: mov r0, r2
0x86a8: call 0x8471
0x86ac: test r0, r0
0x86af: jnz 0x871a
0x86b2: mov r0, r2
0x86b6: call 0x8499
0x86ba: test r0, r0
0x86bd: jnz 0x871a
0x86c0: mov r0, r2
0x86c4: call 0x84df
0x86c8: test r0, r0
0x86cb: jnz 0x871a
0x86ce: mov r0, r2
0x86d2: call 0x8502
0x86d6: test r0, r0
...

Good.

Also, after 0x8759 it looks like a data section.

1
2
3
4
5
6
0x8759: .byte 0x45 (E)
0x875a: .byte 0x6e (n)
0x875b: .byte 0x74 (t)
0x875c: .byte 0x65 (e)
0x875d: .byte 0x72 (r)
...

However, parts such as 0x87e8 are misinterpreted as codes.

1
0x87e8: inc r82

The data section was not obfuscated.

1
2
3
4
5
00007e0: 6c61 6700 3ce3 5a9e 9113 8c05 e42e 0a52 lag.<.Z........R
00007f0: 3dd8 7cf5 9f4b 9f06 d7a8 e9a0 a636 a649 =.|..K.......6.I
0000800: 3136 9308 eb70 ebbf df28 500d 7be8 96fa 16...p...(P.{...
0000810: e8b7 a5df c24d f0b8 3b78 6272 b748 1697 .....M..;xbr.H..
0000820: f019 2d6b 085b 9f94 4987 e624 3752 efb8 ..-k.[..I..$7R..

So I gave first aid to src_vm/disass.c:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
@@ -322,8 +322,15 @@
static uint16_t dis_inc(uint16_t addr)
{
uint8_t operande;
+ char OP, OP2;
+ OP = *(core.memory.vmem + addr);
+ OP2 = *(core.memory.vmem + addr + 1);
operande = *(core.memory.vmem + addr + 1);
+ if(addr > 0x8759)
+ fprintf(stdout, "%s0x%.4x%s: [DEBUG] .byte 0x%.2x\n", RED, addr, ENDC, (unsigned char)OP);
+ fprintf(stdout, "%s0x%.4x%s: [DEBUG] .byte 0x%.2x\n", RED, addr + 1, ENDC, (unsigned char)OP2);
+
fprintf(stdout, "%s0x%.4x%s: inc r%d\n", RED, addr, ENDC, operande);
return (addr + 2);

Awful… who cares?

1
2
3
4
0x87e8: [DEBUG] .byte 0x0a
0x87e9: [DEBUG] .byte 0x52
0x87e8: inc r82
0x87ea: .byte 0x3d (=)

First Attempt With KLEE

This is a failure case.

As we have seen so far, VMNDH-2k12 is open-sourced. So I tried to solve the challenge with source code-based symbolic execution tool–KLEE.

I modified src_vm/syscall_write.c for assertion:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
@@ -18,6 +18,8 @@
*/
#include "vmndh.h"
+#include <klee/klee.h>
+#include <string.h>
void syscall_write(void)
{
@@ -32,7 +34,12 @@
if (core.flagmode.noverbose == 0)
write(1, txt, strlen(txt));
+
+ if (strstr(arg2, "Thank") != NULL)
+ klee_assert(0);
+
core.regs.r0 = write(arg1, arg2, arg3);
+
if (core.flagmode.noverbose == 0)
write(1, "\n", 1);
}

Here is a modified Makefile:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
@@ -17,14 +17,15 @@
## Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
##
-DEBUG = no
+DEBUG = yes
RM = rm -f
INCLUDE = ./includes
SRC_DIR = ./src_vm
+KLEE_PATH = ../klee_src/include
NAME = vmndh
ifeq ($(DEBUG),yes)
- CFLAGS = -c -ggdb3 -Wextra -Wall -D _BSD_SOURCE -I$(INCLUDE)
+ CFLAGS = -c -ggdb3 -Wextra -Wall -D _BSD_SOURCE -I$(INCLUDE) -I$(KLEE_PATH) -emit-llvm -g
LDFLAGS =
CC = clang
else

I’d left all of it to KLEE and get to bed…

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
$ make
$ llvm-link src_vm/*.o -o vmndh.bc
$ klee --optimize --emit-all-errors --libc=uclibc --write-smt2s --posix-runtime vmndh.bc -file pepperidge_farm -sym-stdin 65
KLEE: NOTE: Using klee-uclibc : /home/klee/klee_build/klee/Release+Debug+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/klee/klee_build/klee/Release+Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/klee/VMNDH-2k12/klee-out-1"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "__user_main" has inline asm
KLEE: WARNING ONCE: function "syscall_accept" has inline asm
KLEE: WARNING ONCE: function "syscall_bind" has inline asm
KLEE: WARNING ONCE: function "syscall_listen" has inline asm
KLEE: WARNING ONCE: function "syscall_recv" has inline asm
KLEE: WARNING ONCE: function "syscall_send" has inline asm
KLEE: WARNING ONCE: function "syscall_socket" has inline asm
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 44258832) at /home/klee/klee_src/runtime/POSIX/fd.c:1044
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
Enter your registration code: KLEE: WARNING ONCE: calling external: vprintf(57126208, 46345808) at /home/klee/klee_build/klee-uclibc/libc/stdio/fprintf.c:36
[SYSCALL output]: 64
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
...
KLEE: WARNING: killing 175 states (over memory cap)
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
Code does not match any known registered users
...
Code does not match any known registered users
KLEE: done: total instructions = 5117896332
KLEE: done: completed paths = 81092
KLEE: done: generated tests = 81092

… It’s not going to be easy.

I also wrote solver with angr. Which symbolizes stdin, but… let’s not talk about it.

An example of insufficient SMTLIB2 representations is:

1
2
3
4
5
6
7
(set-logic QF_AUFBV )
(declare-fun model_version () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun stdin () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun stdin-stat () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (let ( (?B1 (select stdin (_ bv25 32) ) ) (?B2 (select stdin (_ bv31 32) ) ) (?B3 (select stdin (_ bv18 32) ) ) (?B4 (select stdin (_ bv40 32) ) ) (?B5 (select stdin (_ bv36 32) ) ) (?B6 (select stdin (_ bv23 32) ) ) (?B7 (select stdin (_ bv27 32) ) ) (?B8 (select stdin (_ bv33 32) ) ) (?B9 (select stdin (_ bv6 32) ) ) (?B10 (select stdin (_ bv8 32) ) ) ) (let ( (?B13 ((_ zero_extend 16) ((_ zero_extend 8) ?B7 ) ) ) (?B14 ((_ zero_extend 16) ((_ zero_extend 8) ?B8 ) ) ) (?B12 ((_ zero_extend 16) ((_ zero_extend 8) ?B2 ) ) ) (?B11 ((_ zero_extend 16) ((_ zero_extend 8) ?B1 ) ) ) ) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= false (= (_ bv0 64) (bvand (concat (select stdin-stat (_ bv15 32) ) (concat (select stdin-stat (_ bv14 32) ) (concat (select stdin-stat (_ bv13 32) ) (concat (select stdin-stat (_ bv12 32) ) (concat (select stdin-stat (_ bv11 32) ) (concat (select stdin-stat (_ bv10 32) ) (concat (select stdin-stat (_ bv9 32) ) (select stdin-stat (_ bv8 32) ) ) ) ) ) ) ) ) (_ bv2147483647 64) ) ) ) (bvult (concat (select stdin-stat (_ bv63 32) ) (concat (select stdin-stat (_ bv62 32) ) (concat (select stdin-stat (_ bv61 32) ) (concat (select stdin-stat (_ bv60 32) ) (concat (select stdin-stat (_ bv59 32) ) (concat (select stdin-stat (_ bv58 32) ) (concat (select stdin-stat (_ bv57 32) ) (select stdin-stat (_ bv56 32) ) ) ) ) ) ) ) ) (_ bv65536 64) ) ) (= (_ bv1 32) (concat (select model_version (_ bv3 32) ) (concat (select model_version (_ bv2 32) ) (concat (select model_version (_ bv1 32) ) (select model_version (_ bv0 32) ) ) ) ) ) ) (= (_ bv48 8) (select stdin (_ bv0 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv1 32) ) ) ) (= (_ bv57 8) (select stdin (_ bv2 32) ) ) ) (= (_ bv70 8) (select stdin (_ bv3 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv4 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv5 32) ) ) ) (= false (= (_ bv48 8) ?B9 ) ) ) (= false (bvult (_ bv48 32) ((_ zero_extend 16) ((_ zero_extend 8) ?B9 ) ) ) ) ) (= false (= (_ bv48 8) ?B10 ) ) ) (= false (bvult (_ bv48 32) ((_ zero_extend 16) ((_ zero_extend 8) ?B10 ) ) ) ) ) (= (_ bv48 8) (select stdin (_ bv12 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv13 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv14 32) ) ) ) (= (_ bv57 8) (select stdin (_ bv15 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv16 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv17 32) ) ) ) (= false (= (_ bv48 8) ?B3 ) ) ) (= false (bvult (_ bv48 32) ((_ zero_extend 16) ((_ zero_extend 8) ?B3 ) ) ) ) ) (= (_ bv48 8) (select stdin (_ bv20 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv21 32) ) ) ) (= (_ bv57 8) (select stdin (_ bv22 32) ) ) ) (= false (= (_ bv48 8) ?B6 ) ) ) (= false (bvult (_ bv48 32) ((_ zero_extend 16) ((_ zero_extend 8) ?B6 ) ) ) ) ) (= (_ bv48 8) (select stdin (_ bv24 32) ) ) ) (= false (= (_ bv48 8) ?B1 ) ) ) (bvult (_ bv48 32) ?B11 ) ) (= false (= (_ bv57 8) ?B1 ) ) ) (= false (bvult (_ bv57 32) ?B11 ) ) ) (= (_ bv48 8) (select stdin (_ bv26 32) ) ) ) (= false (= (_ bv48 8) ?B7 ) ) ) (bvult (_ bv48 32) ?B13 ) ) (= false (= (_ bv57 8) ?B7 ) ) ) (= false (bvult (_ bv57 32) ?B13 ) ) ) (= (_ bv48 8) (select stdin (_ bv28 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv29 32) ) ) ) (= (_ bv48 8) (select stdin (_ bv30 32) ) ) ) (= false (= (_ bv48 8) ?B2 ) ) ) (bvult (_ bv48 32) ?B12 ) ) (= false (= (_ bv57 8) ?B2 ) ) ) (= false (bvult (_ bv57 32) ?B12 ) ) ) (= (_ bv48 8) (select stdin (_ bv32 32) ) ) ) (= false (= (_ bv48 8) ?B8 ) ) ) (bvult (_ bv48 32) ?B14 ) ) (= false (= (_ bv57 8) ?B8 ) ) ) (bvult (_ bv57 32) ?B14 ) ) (= false (= (_ bv70 8) ?B8 ) ) ) (bvult (_ bv70 32) ?B14 ) ) (= false (= (_ bv48 8) ?B5 ) ) ) (= false (bvult (_ bv48 32) ((_ zero_extend 16) ((_ zero_extend 8) ?B5 ) ) ) ) ) (= false (= (_ bv48 8) ?B4 ) ) ) (= false (bvult (_ bv48 32) ((_ zero_extend 16) ((_ zero_extend 8) ?B4 ) ) ) ) ) ) ) )
(check-sat)
(exit)

Solution With Z3

Since there is no choice, I read all the disassembly. After some twists and turn, I realized that:

  • Pepperidge Farm checks character codes against transformed 0x20 bytes values.
  • 0x8247(x, y) returns x * 100 + y.

Now Z3 time. For example, subroutine 0x8269:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
0x8269: push r1
0x826d: pop r2
0x826f: mov r7, r0
0x8273: addb r0, #00
0x8277: call 0x8247
0x827b: mov r1, r0
0x827f: mov r0, r7
0x8283: addb r0, #14
0x8287: call 0x8247
0x828b: mov r2, r0
0x828f: movl r0, #0x87ec
0x8294: call 0x8247
0x8298: xorl r1, #4936
0x829d: add r1, r2
0x82a1: xor r0, r1
0x82a5: pop r2
0x82a7: pop r1
0x82a9: ret
...
0x87ec: .byte 0x7c (|)
0x87ed: .byte 0xf5

becomes:

1
s.add(((sub_8247(0) ^ 0x4936) + sub_8247(0x14)) ^ 0x7cf5 == 0)

This is satisfiable. But not enough. We need to add rest of constraints.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
#!/usr/bin/env python
#coding: utf-8
import telnetlib, sys
from z3 import *
REMOTE = len(sys.argv) >= 2 and sys.argv[1] == 'r'
if REMOTE:
host = 'pepperidge-farm_edb4ad2f103a9efde038346d2cd86a1e.quals.shallweplayaga.me'
port = 2012
else:
host = '127.0.0.1'
port = 4000
values = [BitVec('x%d' % i, 8) for i in range(0x20)]
def sub_8247(x): return ZeroExt(8, values[x]) << 8 | ZeroExt(8, values[x + 1])
s = Solver()
# sub_8269
s.add(((sub_8247(0) ^ 0x4936) + sub_8247(0x14)) ^ 0x7cf5 == 0)
# sub_82aa
s.add(sub_8247(6) * sub_8247(8) * (sub_8247(2) ^ 0xfdf) ^ 0x3dd8 == 0)
# sub_8304
s.add(((sub_8247(4) ^ 0xc7df) + sub_8247(0xe) * sub_8247(0xc)) ^ 0xeb70 == 0)
# sub_835e
s.add(((sub_8247(6) ^ 0xc5db) + 0x14aa) ^ 0x500d == 0)
# sub_838b
s.add(sub_8247(8) * sub_8247(0x1e) ^ 0x7be8 == 0)
# sub_83c7
s.add((sub_8247(0xa) + sub_8247(6) + sub_8247(0xC)) ^ 0xdf28 == 0)
# sub_841c
s.add(((sub_8247(0xC) + 0x5432) | 0x3008) ^ 0x3b78 == 0)
# sub_8449
s.add((sub_8247(0xE) + 0x1212) ^ 0x1697 == 0)
# sub_8471
s.add((sub_8247(0x10) ^ 0x8703) ^ 0x3136 == 0)
# sub_8499
s.add(((sub_8247(0x12) + 0x4004) + (sub_8247(0x14) ^ 0xA52)) ^ 0x6272 == 0)
# sub_84df
s.add()
# sub_8502
s.add((sub_8247(0x16) + sub_8247(0x10)) ^ 0x9308 == 0)
# sub_853e
s.add(sub_8247(0x18) ^ 0x085b == 0)
# sub_8561
s.add(((sub_8247(0x1a) ^ 0x863c) + 0x1234) ^ 0x9113 == 0)
# sub_858e
s.add((sub_8247(0x1c) + sub_8247(8) + sub_8247(0x12)) ^ 0xf0b8 == 0)
# sub_85e3
s.add(((sub_8247(0x1e) & 0x0f00) + sub_8247(0)) ^ 0x9f94 == 0)
print s.check()
print s.model()
input = ''
for i in range(0x20):
try:
input += '%02x' % s.model()[values[i]].as_long()
except:
input += '??'
input = input.upper()
print input
t = telnetlib.Telnet(host, port)
t.write(input + '\n')
t.interact()

Even with halfway constraints, the process proceeds. So inscount with Pin or other dynamic binary instrumentation tools might be helpful.

Finally I got:

1
2
3
4
Enter your registration code: 90940C6017E5FEB82083F932E73E0485B635796DA353DCD3085BF8E356C87FF8
Thank you for your patronage!
Your username is: pepperidge
This is the flag: th0s3_wh0_l0ok_0nly_to_th3_p4stur3_ar3_cert4in_t0_miss_th3_futur3

The conclusive SMTLIB2 representation is:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
; benchmark
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun x1 () (_ BitVec 8))
(declare-fun x0 () (_ BitVec 8))
(declare-fun x31 () (_ BitVec 8))
(declare-fun x30 () (_ BitVec 8))
(declare-fun x19 () (_ BitVec 8))
(declare-fun x18 () (_ BitVec 8))
(declare-fun x9 () (_ BitVec 8))
(declare-fun x8 () (_ BitVec 8))
(declare-fun x29 () (_ BitVec 8))
(declare-fun x28 () (_ BitVec 8))
(declare-fun x27 () (_ BitVec 8))
(declare-fun x26 () (_ BitVec 8))
(declare-fun x25 () (_ BitVec 8))
(declare-fun x24 () (_ BitVec 8))
(declare-fun x17 () (_ BitVec 8))
(declare-fun x16 () (_ BitVec 8))
(declare-fun x23 () (_ BitVec 8))
(declare-fun x22 () (_ BitVec 8))
(declare-fun x21 () (_ BitVec 8))
(declare-fun x20 () (_ BitVec 8))
(declare-fun x15 () (_ BitVec 8))
(declare-fun x14 () (_ BitVec 8))
(declare-fun x13 () (_ BitVec 8))
(declare-fun x12 () (_ BitVec 8))
(declare-fun x7 () (_ BitVec 8))
(declare-fun x6 () (_ BitVec 8))
(declare-fun x11 () (_ BitVec 8))
(declare-fun x10 () (_ BitVec 8))
(declare-fun x5 () (_ BitVec 8))
(declare-fun x4 () (_ BitVec 8))
(declare-fun x3 () (_ BitVec 8))
(declare-fun x2 () (_ BitVec 8))
(assert
(let ((?x206 (bvand (bvor (bvshl ((_ zero_extend 8) x30) (_ bv8 16)) ((_ zero_extend 8) x31)) (_ bv3840 16))))
(let ((?x209 (bvxor (bvadd ?x206 (bvor (bvshl ((_ zero_extend 8) x0) (_ bv8 16)) ((_ zero_extend 8) x1))) (_ bv40852 16))))
(let (($x210 (= ?x209 (_ bv0 16))))
(let ((?x82 (bvor (bvshl ((_ zero_extend 8) x8) (_ bv8 16)) ((_ zero_extend 8) x9))))
(let ((?x200 (bvadd (bvor (bvshl ((_ zero_extend 8) x28) (_ bv8 16)) ((_ zero_extend 8) x29)) ?x82)))
(let ((?x201 (bvadd ?x200 (bvor (bvshl ((_ zero_extend 8) x18) (_ bv8 16)) ((_ zero_extend 8) x19)))))
(let (($x204 (= (bvxor ?x201 (_ bv61624 16)) (_ bv0 16))))
(let ((?x190 (bvxor (bvor (bvshl ((_ zero_extend 8) x26) (_ bv8 16)) ((_ zero_extend 8) x27)) (_ bv34364 16))))
(let (($x195 (= (bvxor (bvadd ?x190 (_ bv4660 16)) (_ bv37139 16)) (_ bv0 16))))
(let ((?x183 (bvxor (bvor (bvshl ((_ zero_extend 8) x24) (_ bv8 16)) ((_ zero_extend 8) x25)) (_ bv2139 16))))
(let (($x184 (= ?x183 (_ bv0 16))))
(let ((?x174 (bvadd (bvor (bvshl ((_ zero_extend 8) x22) (_ bv8 16)) ((_ zero_extend 8) x23)) (bvor (bvshl ((_ zero_extend 8) x16) (_ bv8 16)) ((_ zero_extend 8) x17)))))
(let (($x177 (= (bvxor ?x174 (_ bv37640 16)) (_ bv0 16))))
(let ((?x165 (bvxor (bvor (bvshl ((_ zero_extend 8) x20) (_ bv8 16)) ((_ zero_extend 8) x21)) (_ bv2642 16))))
(let ((?x163 (bvadd (bvor (bvshl ((_ zero_extend 8) x18) (_ bv8 16)) ((_ zero_extend 8) x19)) (_ bv16388 16))))
(let (($x169 (= (bvxor (bvadd ?x163 ?x165) (_ bv25202 16)) (_ bv0 16))))
(let ((?x154 (bvxor (bvor (bvshl ((_ zero_extend 8) x16) (_ bv8 16)) ((_ zero_extend 8) x17)) (_ bv34563 16))))
(let (($x157 (= (bvxor ?x154 (_ bv12598 16)) (_ bv0 16))))
(let ((?x145 (bvadd (bvor (bvshl ((_ zero_extend 8) x14) (_ bv8 16)) ((_ zero_extend 8) x15)) (_ bv4626 16))))
(let (($x148 (= (bvxor ?x145 (_ bv5783 16)) (_ bv0 16))))
(let ((?x107 (bvor (bvshl ((_ zero_extend 8) x12) (_ bv8 16)) ((_ zero_extend 8) x13))))
(let (($x143 (= (bvxor (bvor (bvadd ?x107 (_ bv21554 16)) (_ bv12296 16)) (_ bv15224 16)) (_ bv0 16))))
(let ((?x78 (bvor (bvshl ((_ zero_extend 8) x6) (_ bv8 16)) ((_ zero_extend 8) x7))))
(let ((?x132 (bvadd (bvor (bvshl ((_ zero_extend 8) x10) (_ bv8 16)) ((_ zero_extend 8) x11)) ?x78)))
(let (($x136 (= (bvxor (bvadd ?x132 ?x107) (_ bv57128 16)) (_ bv0 16))))
(let ((?x124 (bvmul ?x82 (bvor (bvshl ((_ zero_extend 8) x30) (_ bv8 16)) ((_ zero_extend 8) x31)))))
(let (($x127 (= (bvxor ?x124 (_ bv31720 16)) (_ bv0 16))))
(let (($x119 (= (bvxor (bvadd (bvxor ?x78 (_ bv50651 16)) (_ bv5290 16)) (_ bv20493 16)) (_ bv0 16))))
(let ((?x108 (bvmul (bvor (bvshl ((_ zero_extend 8) x14) (_ bv8 16)) ((_ zero_extend 8) x15)) ?x107)))
(let ((?x109 (bvadd (bvxor (bvor (bvshl ((_ zero_extend 8) x4) (_ bv8 16)) ((_ zero_extend 8) x5)) (_ bv51167 16)) ?x108)))
(let (($x112 (= (bvxor ?x109 (_ bv60272 16)) (_ bv0 16))))
(let ((?x90 (bvmul (bvmul ?x78 ?x82) (bvxor (bvor (bvshl ((_ zero_extend 8) x2) (_ bv8 16)) ((_ zero_extend 8) x3)) (_ bv4063 16)))))
(let (($x93 (= (bvxor ?x90 (_ bv15832 16)) (_ bv0 16))))
(let ((?x50 (bvadd (bvxor (bvor (bvshl ((_ zero_extend 8) x0) (_ bv8 16)) ((_ zero_extend 8) x1)) (_ bv18742 16)) (bvor (bvshl ((_ zero_extend 8) x20) (_ bv8 16)) ((_ zero_extend 8) x21)))))
(let (($x54 (= (bvxor ?x50 (_ bv31989 16)) (_ bv0 16))))
(and $x54 $x93 $x112 $x119 $x127 $x136 $x143 $x148 $x157 $x169 $x177 $x184 $x195 $x204 $x210)))))))))))))))))))))))))))))))))))))
(check-sat)

Final Words

I enjoyed this challenge. It seems to be easy or medium-easy difficulty rating. If only I could have solved more difficult Reverse Engineering challenges during quals–liberty, godzilla, and so on.

Recently I read T. Blazytko et al. USENIX Security’17. The paper says the system named Syntia automatically deobfuscate binaries with program synthesis. Program synthesis is a method to synthesize some pieces of program from given I/O samples and possible operators–like this:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
#!/usr/bin/env python
#coding: utf-8
from z3 import *
x, y, h = BitVecs(['x', 'y', 'h'], 8)
# I/O samples
t1 = And(x == 1, y == 2)
t2 = And(x == 2, y == 4)
t3 = And(x == 3, y == 6)
phi_1 = Or(t1, t2, t3)
# h is subject to synthesize
phi_2 = y == x << h
s = Solver()
s.add(ForAll([x, y], Implies(phi_1, phi_2)))
print s.check() # sat
print s.model() # [h = 2]

This is just a simple example. In practical, program slicing and path pruning will be needed. Both symbolic execution and program synthesis depend on SMT solver, but according to the paper, program synthesis is more suitable for deobfuscation tasks… really? I’ll investigate further.

Introduction

As you know, IDAPython is quite useful. And Triton concolic execution engine has python binding. Then… why not integrate them? I tried to stand on the shoulders of giants.

Backward Program Slicing

Roughly speaking, program slicing is a method to extract subset of program which is relevant to given statement. Here is an excerpt from M. Weiser. ICSE’81:

Starting from a subset of a program’s behavior, slicing reduces that program to a minimal form which still produces that behavior. The reduced program, called a “slice”, is an independent program guaranteed to faithfully represent the original program within the domain of the specified subset of behavior.

Kudos to Jonathan Salwan, we can easily apply backward program slicing to binary analysis process with minor modification of backward_slicing.py and proving_opaque_predicates.py. I wrote a simple, tiny glue between Triton and IDA Pro:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
#!/usr/bin/env python
#coding: utf-8
from idc import *
from idaapi import *
from triton import *
ctx = TritonContext()
regs = {
'eax': REG.X86.EAX,
'ebx': REG.X86.EBX,
'ecx': REG.X86.ECX,
'edx': REG.X86.EDX,
}
def symbolization_init():
Triton.convertRegisterToSymbolicVariable(Triton.registers.eax)
Triton.convertRegisterToSymbolicVariable(Triton.registers.ebx)
Triton.convertRegisterToSymbolicVariable(Triton.registers.ecx)
Triton.convertRegisterToSymbolicVariable(Triton.registers.edx)
return
def opaque_predicate_detection(pc):
ctx.setArchitecture(ARCH.X86)
ctx.setAstRepresentationMode(AST_REPRESENTATION.PYTHON)
symbolization_init()
ast_ctx = ctx.getAstContext()
while True:
instruction = Instruction()
instruction.setAddress(pc)
opcode = GetManyBytes(pc, ItemSize(pc)) # Disassemble with IDA Pro
instruction.setOpcode(opcode)
ctx.processing(instruction) # Emulate instruction without Pintool
for se in instruction.getSymbolicExpressions():
se.setComment(str(instruction))
if str(instruction.getDisassembly()).split()[0] == 'cmp': # if instruction.isCompare():
reg = str(instruction.getOperands()[0]).split(':')[0] # Get first operand
if reg in regs:
Expr = ctx.getSymbolicRegisters()[regs[reg]]
slicing = ctx.sliceExpressions(Expr)
for k, v in sorted(slicing.items()):
print v.getComment()
print instruction
elif instruction.isBranch():
print instruction
if instruction.isConditionTaken():
print 'branch will taken'
else:
print 'branch will not taken'
break
pc = NextHead(pc)
print '-' * 50
def main():
ea = ScreenEA() # Get address corresponding to cursor
opaque_predicate_detection(ea)
if __name__ == '__main__':
view = main()

Showcase

The snippet extracts subset of program which is relevant to branch condition. We can run this from File -> Script file in IDA Pro menu.

Conditional Branch

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
.text:004074DD loc_4074DD:
.text:004074DD 040 mov dword ptr [edi+18h], 0Ah
.text:004074E4 040 mov dword ptr [edi+14h], 0
.text:004074EB 040 mov word ptr [edi+8], 8235h
.text:004074F1 040 mov dword ptr [edi+0Ch], 3E8h
.text:004074F8 040 mov dword ptr [edi+10h], 0BB8h
.text:004074FF 040 sub esp, 4
.text:00407502 044 mov [esp+40h+Memory], 0B8h ; Size ; cursor
.text:00407509 044 call ??2@YAPAXI@Z ; operator new(uint)
.text:0040750E 044 add esp, 4
.text:00407511 040 mov [esi+18h], eax
.text:00407514 040 mov eax, dword_591EE4
.text:00407519 040 mov ecx, dword_591EE0
.text:0040751F 040 imul eax, eax
.text:00407522 040 imul edx, eax, 7
.text:00407525 040 dec edx
.text:00407526 040 mov eax, ecx
.text:00407528 040 imul eax, eax
.text:0040752B 040 cmp edx, eax
.text:0040752D 040 jz short loc_407538

becomes:

1
2
3
4
5
6
7
0x407514: mov eax, dword ptr [0x591ee4]
0x40751f: imul eax, eax
0x407522: imul edx, eax, 7
0x407525: dec edx
0x40752b: cmp edx, eax
0x40752d: je 0x407538
branch will not taken

Unconditional Branch

1
2
3
4
5
6
7
8
9
.text:004078C3 loc_4078C3:
.text:004078C3 000 mov esp, edi ; cursor
.text:004078C5 000 mov eax, dword_591EAC
.text:004078CA 000 lea ecx, [eax+4]
.text:004078CD 000 mov edx, eax
.text:004078CF 000 sar edx, cl
.text:004078D1 000 lea eax, [eax+edx*2]
.text:004078D4 000 mov dword_591EAC, eax
.text:004078D9 000 jmp short loc_4

becomes:

1
2
0x4078d9: jmp 0x40789a
branch will taken

Looks nice.

Last Words

Triton’s emulation iteration is compatible to IDAPython manner. Therefore, The combination of IDA Pro and Triton is pretty good.

Cheers,

Introduction

IDAPython is a powerful feature of IDA Pro, and there are many open-sourced IDAPython projects. However, we cannot use every GUI-based IDAPython script due to some Qt-related breaking changes between IDA Pro 6.8 and 6.9 or later. The main problem is about migrating no longer supported PySide code to PyQt5.

Recently I ported PySide code within idasec–one of the most sophisticated deobfuscation frameworks, which tackles opaque predicates and call stack tampering in terms of infeasibility questions, by utilizing Backward-Bounded Dynamic Symbolic Execution proposed in the remarkably well written paper S. Bardin et al. IEEE S&P’17–to PyQt5.

That’s why I decided to write this blog post for a note to self and for someone trying to do similar thing.

Related Work

There are 2 guidances to migrate PySide code to PyQt5:

Please read them before. I only give supplemental information in addition to predecessors.

How to Migrate

Now let’s get started.

Change QtGui methods to QtWidgets

Most methods in QtGui migrated to QtWidgets. Therefore,

1
from PySide import QtGui, QtCore

becomes:

1
from PyQt5 import QtCore, QtGui, QtWidgets

As an example, QTextEdit described in Hex Blog. In additions, the methods to be rewritten are as follows:

  • QtWidgets.QLayout
  • QtWidgets.QVBoxLayout
  • QtWidgets.QHBoxLayout
  • QtWidgets.QWidget
  • QtWidgets.QTableWidget
  • QtWidgets.QListWidget
  • QtWidgets.QTabWidget
  • QtWidgets.QDockWidget
  • QtWidgets.QTreeWidget
  • QtWidgets.QTreeWidgetItem
  • QtWidgets.QPushButton
  • QtWidgets.QRadioButton
  • QtWidgets.QToolButton
  • QtWidgets.QButtonGroup
  • QtWidgets.QGroupBox
  • QtWidgets.QSpinBox
  • QtWidgets.QCheckBox
  • QtWidgets.QComboBox
  • QtWidgets.QTextEdit
  • QtWidgets.QLineEdit
  • QtWidgets.QApplication
  • QtWidgets.QLabel
  • QtWidgets.QSizePolicy
  • QtWidgets.QMenu
  • QtWidgets.QFrame
  • QtWidgets.QProgressBar
  • QtWidgets.QStyle
  • QtWidgets.QSpacerItem
  • QtWidgets.QScrollArea
  • QtWidgets.QSplitter
  • There might be more…

My experience says that other than the following 3 methods may be rewritten:

  • QtGui.QPixmap
  • QtGui.QIcon
  • QtGui.QFont

idacute may overwrite all of QtGui methods, so I think there still needs to be manual works.

Overwrite _fromUtf8

We also need to overwrite _fromUtf8.

1
2
3
4
try:
_fromUtf8 = QtCore.QString.fromUtf8
except AttributeError:
    _fromUtf8 = lambda s: s

Others

These issues are described by predecessors:

  • Handling SIGNAL
  • Change FormToPySideWidget to FormToPyQtWidget
  • Change setResizeMode to setSectionResizeMode

Conclusion

This time, I was able to run idasec on IDA Pro 7.0 with some bug fixes and dirty patches – like this cool video:

If you are an IDA Pro 7.0 user, note that other backward-compatibility issue described in IDA: IDAPython backward-compatibility with 6.95 APIs will occur.

Enjoy!

HAI DOMO VIRTUAL YOUTUBER KIZUNA AI DESU. I’m still working on my English.

Xming

 XmingはWindows向けX Window System実装で,WindowsでX11 Forwardingをする場合のデファクトスタンダード.さて,日本語版のWindowsでXmingを利用していると,時折勝手に入力言語が英語に変わってしまうことがある.でまあOSSなのでソースコードを書き換えればいいんだけど,バイナリを読んだほうが早そう,ということでそのようにした.

原因

 IDA Proでキーボード関連のAPIの呼び出し元を眺めると,LoadKeyboardLayoutのロケールID引数を英語 (0x0409) に設定していることがわかる.これを日本語 (0x0411) にすればよい.

 素直に.rdataセクションに載っているので,そのまま書き換えられる.

 紀元前のバイナリパッチ方式で書くと下記の通り:

1
2
3
4
19AFAA: 30 31
19AFAB: 39 31
19AFB5: 55 4A
19AFB6: 53 50

 はい.

追記 (2016.11.07)

 XmingのバージョンはPublic Domain Releases 6.9.0.31で,より新しい有償版で修正されているのかどうかは知らない.で,6.9.0.31の当該ソースコード (xc/programs/Xserver/hw/xwin/winconfig.c) にはなにやら不吉なコメントが記されているが,見なかったことにする.うちの環境では,レジストリ設定でCaps LockをCtrlに入れ替えてるし.

1
2
3
4
5
6
7
8
9
10
if (keyboardType == 7)
{
/* Japanese layouts have problems with key event messages
such as the lack of WM_KEYUP for Caps Lock key.
Loading US layout fixes this problem. */
if (LoadKeyboardLayout("00000409", KLF_ACTIVATE) != NULL)
winMsg (X_INFO, "Loading US keyboard layout.\n");
else
winMsg (X_ERROR, "LoadKeyboardLaout failed.\n");
}

 ご自身の責任でやっていってください.