Monday, July 13, 2015

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

1 comment :