PoliCTF RE350 – JOHN THE PACKER – PIN + Z3

The 32bit ELF is a self modyfing code. So I decided to use PIN for futher analysis.

$ pin -t obj-ia32/exectrace.so -- ./re350 flag{ABCDEFGHIJKLMNOPQRTSUVWXYZ0}

0x80488f8 : cmp eax, 0x21
0x80488f8 : [0x21] [0x21]

$ ltrace -i ./re350 flag{ABCDEFGHIJKLMNOPQRTSUVWXYZ0}
[0x80488f5] strlen("flag{ABCDEFGHIJKLMNOPQRTSUVWXYZ0"...) = 33
Length of flag is 33 bytes
Once the length is know, lets search for other interesting stuffs from the PIN trace

0x8048a84 : cmp ebx, eax
0x8048a84 : [0x41] [0x70] -> A is compared with p

$ pin -t obj-ia32/exectrace.so -- ./re350 flag{pBCDEFGHIJKLMNOPQRTSUVWXYZ0}

0x8048a96 : cmp eax, dword ptr [ebp-0x10]
0x8048a96 : [0x1] [0x6]
--
0x8048a84 : cmp ebx, eax
0x8048a84 : [0x70] [0x70] -> p is a valid comparison
--
0x8048a96 : cmp eax, dword ptr [ebp-0x10]
0x8048a96 : [0x2] [0x6]
--
0x8048a84 : cmp ebx, eax -> B is compared to a
0x8048a84 : [0x42] [0x61]
The first 6 unknown bytes are compared directly, which could be retrieved as 'packer'. Going further we could see this:

0x804892f : cmp ebx, eax
0x804892f : [0x16] [0x21]
--
0x8048953 : xor eax, ecx
0x8048953 : [0x50] [0x10] := [0x40]
--
0x804896f : cmp al, byte ptr [ebp-0xe]
0x804896f : [0x40] [0x51]
User supplied 'P' ^ 0x10 == User supplied 'Q'. On futher analysis, the algo looks like this

key[20] ^ 0x10 == key[21]
key[21] ^ 0x44 == key[22]
......
......
key[31] ^ 0x00 == key[32]
There are multiple inputs which satisfies these constraints. Using Z3 one can quickly find all the ascii printables satisfying the condition. Below is the solver:


#!/usr/bin/env python

from z3 import *

def get_models(s):
# from 0vercl0k's z3tools.py
while s.check() == sat:
m = s.model()
yield m
s.add(Or([sym() != m[sym] for sym in m.decls()]))

s = Solver()
a, b, c, d, e, f, g, h, i, j, k, l = BitVecs('a b c d e f g h i j k l', 8)

# ascii printables
s.add(And(0x20 < a, a < 0x7f))
s.add(And(0x20 < b, b < 0x7f))
s.add(And(0x20 < c, c < 0x7f))
s.add(And(0x20 < d, d < 0x7f))
s.add(And(0x20 < e, e < 0x7f))
s.add(And(0x20 < f, f < 0x7f))
s.add(And(0x20 < g, g < 0x7f))
s.add(And(0x20 < h, h < 0x7f))
s.add(And(0x20 < i, i < 0x7f))
s.add(And(0x20 < j, j < 0x7f))
s.add(And(0x20 < k, k < 0x7f))
s.add(And(0x20 < l, l < 0x7f))

# from PIN trace
s.add(a ^ 0x10 == b)
s.add(b ^ 0x44 == c)
s.add(c ^ 0x07 == d)
s.add(d ^ 0x43 == e)
s.add(e ^ 0x59 == f)
s.add(f ^ 0x1c == g)
s.add(g ^ 0x5b == h)
s.add(h ^ 0x1e == i)
s.add(i ^ 0x19 == j)
s.add(j ^ 0x47 == k)
s.add(k ^ 0x00 == l)

for m in get_models(s):
serial = [m[a].as_long(), m[b].as_long(), m[c].as_long(), m[d].as_long(),
m[e].as_long(), m[f].as_long(), m[g].as_long(), m[h].as_long(),
m[i].as_long(), m[j].as_long(), m[k].as_long(), m[l].as_long()]

key = ''
for _ in serial: key += chr(_)
print key

# probable solution =-in-th3-4ss
The most matching characters looked like '=-in-th3-4ss'. Thats 12 bytes of flag. Now we have flag{packerXXXXXXXXX=-in-th3-4ss}. After this, there wasn't much details in the trace file [I didn't trace floating point operations]. We need to find how the middle part of flag is validated

The ltrace had few calls to pow() function. Lets see, if there is anything related to this. Self modyfing code might cause issue with breakpoints.

2681 [0x80487b3] pow(0, 0x40180000, 0, 0x40080000) = 1
2681 [0x80487e0] pow(0, 0x40180000, 0, 0x40000000) = 1
2681 [0x8048843] pow(0, 0x40000000, 0, 0x40504000) = 1

gdb-peda$ break *0x8048843
Breakpoint 1 at 0x8048843

gdb-peda$ run flag{packerAAAAAAAAA=-in-th3-4ss}

gdb-peda$ generate-core-file
Now, lets analyze the core. Function at 0x08048AA5 has some 7 checks. With little debugging one can find the 5th check is the one that validates the missing parts of flag


.text:08048B67 push eax
.text:08048B68 push 26h
.text:08048B6D push offset check_five
.text:08048B72 call call_mprotect
.text:08048B77 add esp, 10h
.text:08048B7A add [ebp+check_count], eax
.text:08048B7D mov eax, [ebp+arg]
check_five validates key[11] - key[21]. It futher calls a function 0x08048813 to perform some floating point operations. The return value of the floating point operation is compared to validate the flag. Note that the comparison is done sequentially. So for each valid byte, more code is executed. One can use PIN to count instructions and check if a byte is valid or not.


.text:080489F9 push offset floating_point
.text:080489FE call call_mprotect
.text:08048A03 add esp, 20h
.text:08048A06 test eax, eax
.text:08048A08 jnz short success ; flag byte passes first check
.text:08048A0A mov eax, 0 ; failure - invalid flag byte
.text:08048A0F jmp short ret
.text:08048A11 ; ---------------------------------------------------------------------------
.text:08048A11
.text:08048A11 success: ; CODE XREF: check_five+5Fj
.text:08048A11 mov eax, [ebp+flag]
.text:08048A14 add eax, 17
.text:08048A17 movzx eax, byte ptr [eax]
.text:08048A1A movsx eax, al
.text:08048A1D and eax, 1
.text:08048A20 test eax, eax
.text:08048A22 jnz short inc ; flag byte [17] passes second check
.text:08048A24 mov eax, 0
.text:08048A29 jmp short ret
.text:08048A2B ; ---------------------------------------------------------------------------
.text:08048A2B
.text:08048A2B inc: ; CODE XREF: check_five+79j
.text:08048A2B add [ebp+counter], 1
.text:08048A2F
.text:08048A2F loop: ; CODE XREF: check_five+25j
.text:08048A2F cmp [ebp+counter], 0Ah
.text:08048A33 jle short loop_body
.text:08048A35 mov eax, 1
.text:08048A3A
.text:08048A3A ret: ; CODE XREF: check_five+66j
.text:08048A3A ; check_five+80j
Using these information retrieve other bytes. Make sure to count only instructions from main executable.

#!/usr/bin/env python

import subprocess

start = "flag{packer"
end = "=-in-th3-4ss}"

for c in range(33, 127):
trial = start + chr(c) + "A"*8 + end
msg = subprocess.check_output(['pin', '-t', 'obj-ia32/count.so', '--' , './re350', trial])
count = msg.strip()[-3:]
print chr(c), count

$ python counter.py

* 774
+ 774
, 774
- 825
. 774
/ 774
0 774
1 774
2 774
We choose '-' as valid input. The binary accepts multiple solutions. One may have to manually pick up chars to get a meaningful key. If count is same for all possible chars at a particular index, it could be that all chars are valid. Finally, flag for the challenge is

$ ./re350 flag{packer-15-4-?41=-in-th3-4ss}
You got the flag: flag{packer-15-4-?41=-in-th3-4ss}
I arrived at this solution few minutes after the CTF ended :D