CONFidence CTF 2015: Reversing 400 "Deobfuscate Me" writeup
A delegation of the H4x0rPsch0rr team spent a weekend in the awesome city of Kraków and participated in the even more awesome CONFidence CTF organized by the DragonSector team (thanks for the invitation!). Out of the numerous challenges that were opened up during the CTF, no team was able to solve a reversing task called “Deobfuscate Me” which was worth 400 points.
After the competition task authors presented their sample solutions which, in case of this task, consisted of incrementally measuring differences in the execution traces of the challenge depending on the user input. However, we wanted to show that it was also possible to leverage symbolic execution in combination with a SMT solver to solve the challenge. Our (somewhat tedious) approach is described in this writeup.
The challenge is a classical reversing task which simply asks the user for input, performs several checks on it and finally outputs whether the input was correct. Of course, the correct input would then be the flag.
julian@TPT440p ~/CTF/2015_05_CONFidence/rev400 % ./DeobfuscateMe.elf
Flag: DrgnS{I_have_no_idea_what_to_put_here}
Nope :(
As you can see from the dummy input the flag format was known a priori, a fact that decreased the time needed to solve several tasks substantially. The same applies to this challenge, as we will see later.
Firing up Hex-Rays yields the following straight-forward code for main:
int main(int argc, const char **argv, const char **envp)
{
char uinput[64];
printf("Flag: ");
scanf("%63s", uinput);
if (check(uinput) == 0)
puts("Nice, that was the flag!");
else
puts("Nope :(");
return 0;
}
Removing a first layer of obfuscation
The interesting part is the function check, where the binary verifies the user
input. We quickly associate the name of the task with what we are presented with
by check:
.text:080484E0 ; =============== S U B R O U T I N E ===============
.text:080484E0
.text:080484E0
.text:080484E0 public _check
.text:080484E0 _check proc far ; CODE XREF: main+3C
.text:080484E0
.text:080484E0 arg_41B496AE = dword ptr 41B496B6h
.text:080484E0
.text:080484E0 xchg edx, ebx
.text:080484E2 xor eax, 0FFFFFFFFh
.text:080484E5 xchg ebx, ecx
.text:080484E7 jmp loc_804EC31
<% --- snip --- %>
.text:0804865E loc_804865E: ; CODE XREF: _check+5D34
.text:0804865E or edx, 0A869CBC9h
.text:08048664 xchg ebx, edx
.text:08048666 jmp loc_805ACEE
<% --- snip --- %>
.text:0804E211 loc_804E211: ; CODE XREF: _check+6754
.text:0804E211 shl edx, 1Bh
.text:0804E214 jmp loc_804865E
<% --- snip --- %>
.text:0804EC31 loc_804EC31: ; CODE XREF: _check+7
.text:0804EC31 xchg ecx, edx
.text:0804EC33 xchg eax, edx
.text:0804EC34 jmp loc_804E211
<% --- snip --- %>
.text:0805ACEE loc_805ACEE: ; CODE XREF: _check+186
.text:0805ACEE sub ebx, ebp
.text:0805ACF0 jmp loc_805724C
The code is heavily scattered. Assuming that the chain of jmp instructions
continues in this pattern and that all code snippets are position independent
(i.e. do not reference constants or strings relative to their own position),
this is nothing a small python script and
Capstone cannot deal with:
#!/usr/bin/python2.7
from capstone import *
from capstone.x86 import *
md = Cs(CS_ARCH_X86, CS_MODE_32)
md.detail = True
c = open('DeobfuscateMe.elf', 'rb').read()
# virtual address base of the binary
vdiff = 0x08048000
# file offset of the target function
rip = 0x080484E0 - vdiff
# this buffer will store the function excluding the jumps
buf = b''
d = 0
op = [ None, None, None ]
while True:
# disassemble one instruction
i = md.disasm(c[rip:rip+16], rip + vdiff)
i = next(i)
# increase rip
rip += i.size
for x in range(len(i.operands)):
op[x] = i.operands[x]
# Follow jump, omit output to buf
if i.id == X86_INS_JMP:
rip = op[0].imm - vdiff
continue
# We're done, break
elif i.id == X86_INS_RET:
buf += i.bytes
print("0x%x:\t%s\t%s" %(i.address, i.mnemonic, i.op_str))
break
# Any other instruction is appended to the output buf
buf += i.bytes
print("0x%x:\t%s\t%s" %(i.address, i.mnemonic, i.op_str))
# dump jmp-free version to file
open('deobfuscated.raw', 'wb').write(buf)
By quickly patching the deobfuscated blob into the original binary using dd
and executing the patched binary we see that apparently we didn’t break it too
badly:
julian@TPT440p ~/CTF/2015_05_CONFidence/rev400 % ./Deobfuscated.elf
Flag: DrgnS{I_still_have_no_clue}
Nope :(
40k instructions till complete failure
Okay, let’s reinvestigate the check function in IDA:
.text:080484E0 public _check
.text:080484E0 _check proc near ; CODE XREF: main+3Cp
.text:080484E0
.text:080484E0 arg_4 = dword ptr 8
.text:080484E0
.text:080484E0 xchg edx, ebx
.text:080484E2 xor eax, 0FFFFFFFFh
.text:080484E5 xchg ebx, ecx
.text:080484E7 xchg ecx, edx
.text:080484E9 xchg eax, edx
.text:080484EA shl edx, 1Bh
.text:080484ED or edx, 0A869CBC9h
.text:080484F3 xchg ebx, edx
.text:080484F5 sub ebx, ebp
.text:080484F7 add ecx, eax
.text:080484F9 sub ebx, ebp
.text:080484FB xor ebx, ebx
.text:080484FD add ebx, eax
.text:080484FF xchg ebx, edx
.text:08048501 xchg eax, ecx
.text:08048502 xchg edx, ebx
.text:08048504 neg ebx
.text:08048506 add eax, ebx
.text:08048508 xchg edx, ebx
.text:0804850A xchg eax, ebx
.text:0804850B xor edx, edx
.text:0804850D add edx, 0FFBB4586h
.text:08048513 sub edx, 81622B0Fh
.text:08048519 add edx, 2276E2FAh
.text:0804851F xchg eax, ecx
.text:08048520 xor edx, edx
.text:08048522 xchg ebx, ecx
.text:08048524 xchg eax, ebx
.text:08048525 xchg eax, ecx
.text:08048526 xchg ebx, ecx
.text:08048528 sub edx, 0D51EAFBFh
.text:0804852E xchg edx, ecx
.text:08048530 xchg eax, edx
.text:08048531 add ecx, 0C6538058h
.text:08048537 xchg ebx, ecx
.text:08048539 xchg eax, ecx
.text:0804853A xchg edx, ecx
.text:0804853C rol ebx, 7
.text:0804853F xchg eax, ecx
.text:08048540 xchg eax, ebx
.text:08048541 xchg edx, ecx
.text:08048543 xchg eax, edx
.text:08048544 xchg eax, ecx
.text:08048545 push ebp
.text:08048546 xchg eax, ebx
.text:08048547 xchg eax, ebx
.text:08048548 xor ebp, 0FFFFFFFFh
.text:0804854B xor ebp, 0FFFFFFFFh
.text:0804854E add ebp, 0A10FA35Fh
.text:08048554 xchg ebx, edx
.text:08048556 add ebp, 421A5649h
.text:0804855C sub ebp, 6411B5D9h
.text:08048562 add ebp, 5F1EE010h
.text:08048568 sub ebp, 6CE7BCF1h
.text:0804856E add ebp, 7BF9A346h
.text:08048574 add ebp, 1AE87B85h
<% --- snip --- %>
.text:08052103 xchg eax, ecx
.text:08052104 xchg ebx, edx
.text:08052106 xchg eax, ecx
.text:08052107 mov esi, edx
.text:08052109 xchg ebx, ecx
.text:0805210B neg esi
.text:0805210D mov ebp, esi
.text:0805210F neg ebp
.text:08052111 add ebx, ebp
.text:08052113 xchg edx, ebx
.text:08052115 xchg ecx, ebx
.text:08052117 xchg eax, edx
.text:08052118 xchg eax, ebx
.text:08052119 xchg edx, ecx
.text:0805211B xchg eax, edx
.text:0805211C xchg eax, ecx
.text:0805211D xchg eax, ebx
.text:0805211E xchg edx, ebx
.text:08052120 xchg eax, edx
.text:08052121 xchg edx, ebx
.text:08052123 mov ebp, esi
.text:08052125 and ebp, 72EDEC3Ch
.text:0805212B xor esi, 72EDEC3Ch
.text:08052131 xor esi, ebp
.text:08052133 xor edi, 0FFFFFFFFh
.text:08052136 xchg eax, ecx
.text:08052137 xchg edx, ebx
.text:08052139 xchg ebx, ecx
.text:0805213B xchg ecx, ebx
.text:0805213D pop ebp
.text:0805213E sub edi, ecx
.text:08052140 xchg ecx, ebx
.text:08052142 add edi, ebx
.text:08052144 retn
.text:08052144 _check endp ; sp-analysis failed
.text:08052144
.text:08052144 ; -------------------------------------------------------
Aaaaargh. Even though we’ve seemingly successfully removed the jumps the code
still is close to impossible to read. We see tons of xchg instructions, many of
which are garbage (the actual user input resides on the stack, the
function nevertheless starts to immediately read undefined registers), and lots of
arithmetic operations using cryptic constants. The return value should in theory
be written to eax in the function epilogue but, again, the xchg instructions
make it impossible to track the final value back through the remaining 40k of
machine code.
But hey, decompilers are quite advanced these days, so Hex-Rays’ liveliness analysis plus the built-in constant folding mechanism should remove most of the garbage automatically, right?
Well, to make things even worse, the small sp-analysis failed message at the
bottom of the function tells us that there will be no decompiler to call for
rescue as IDA hadn’t been able to reconstruct the stack frame of the function.
Quickly inspecting the function yields tons of statements that assign arbitrary
constants to both the ebp and the esp registers. Considering the 400 points
of the challenge I’d allege that this is intentional to prevent an easy
“decompiler-only” solution. At this point we considered rewriting all
instructions that use either ebp or esp to use some other operand but as
there is no spare register (we’re operating in 32bit mode and all
e(abcd)x|e(sd)i registers are used by the calculation) a simple renaming of
the offending instruction’s operands is also not feasible. Possibly replacing
each instruction that uses ebp or esp by an opcode sequence that pushes one
of the used registers and then uses fixed memory locations instead of ebp and
esp would have worked but then simply relying on the hidden features of the
Hex-Rays black box seemed like a pretty long shot. This was the point where we
moved to a different challenge during the competition. Now we’re back to fulfill
our duty.
Symbolic Execution and SMT solvers to the rescue
One property of the assembly code is extremely useful: The function is
completely linear, i.e. after patching out (see above) the unconditional jmp
instructions there are no instructions left that could alter the control flow of
the check function in any way. This led to the following idea: Due to the
linearity of the target function it can be seen as one giant basic block. As
basic blocks are branch-free, the operations that the instructions contained by
the block perform on the registers can be translated to one formula per
register. Remember that the function needs to return 0 in eax for the main
procedure to print the success message. Translating the whole block to a formula,
it should be possible to solve the equation eax == 0 for the user-supplied
input variables residing on the stack. Therefore, we need to take two steps to
calculate the solution:
- Translate the function to a formula using symbolic execution
- Solve the resulting equation for
eaxto be zero using a SMT solver
That having said, we found OpenREIL on top of which Dmytro Oleksiuk wrote a simple symbolic execution engine which he used in combination with z3 to solve a crackme. Adopting Dmytro’s approach we came up with the following python script that uses OpenREIL and z3 to solve the challenge (continuation of the python script above):
from pyopenreil.REIL import *
from pyopenreil.utils import asm
from pyopenreil.symbolic import *
import pyopenreil.VM as VM
import struct
import z3
reader = ReaderRaw(ARCH_X86, buf)
tr = CodeStorageTranslator(reader)
bb = tr.get_bb(0)
cpu = Cpu(ARCH_X86)
abi = VM.Abi(cpu, tr, no_reset = True)
ret = 0x41414141
indata = 0x13370000
# IMPORTANT: Patch in the first 4 bytes of the (known) flag format to make the
# solution unique!
cpu.mem.store(indata, U32, Val(struct.unpack("<I", b'Drgn')[0], U32))
# Mark all other input dwords as symbolic
for i in range(1, 16):
cpu.mem.store(indata + i * 4, U32, Val(exp = SymVal('FLAG_{}'.format(i), U32)))
# create stack with pointer to symbolic arguments for check()
stack = abi.pushargs([Val(indata)])
# dummy return address
stack.push(Val(ret))
# initialize emulator's registers (not needed but speeds up the execution)
cpu.reg('esp', Val(stack.top, U32))
cpu.reg('eax', Val(0, U32))
cpu.reg('ebp', Val(0, U32))
cpu.reg('ebx', Val(0, U32))
cpu.reg('ecx', Val(0, U32))
cpu.reg('edx', Val(0, U32))
cpu.reg('edi', Val(0, U32))
cpu.reg('esi', Val(0, U32))
# run until stop
try: cpu.run(tr, 0, stop_at = [0 + len(buf) - 1])
#except VM.CpuStop as e:
# solve in any case, even if an error occurs
except:
print 'STOP at', hex(cpu.reg('eip').get_val())
# get Z3 expressions list for current CPU state
state = cpu.to_z3()
# in theory we only need to solve for 'eax' but if execution ends
# prematurely we at least obtain some parts of the flag
# solving the equation isn't the most expensive operation in this script,
# anyway
for reg in ['eax', 'ebx', 'ecx' , 'edx', 'esi', 'edi', 'ebp']:
print(reg)
# create SMT solver
solver = z3.Solver()
# add constraint for return value
solver.add(0 == cpu.reg(reg).val.to_z3(state, U32))
check = solver.check()
if check == z3.sat:
model = solver.model()
for s in sorted(list(model), key = lambda x: int(x.name()[len('FLAG_'):])):
print(s, hex(model[s].as_long()))
sys.stdout.write('Drgn')
for s in sorted(list(model), key = lambda x: int(x.name()[len('FLAG_'):])):
# prefix solution with the bytes we chose for FLAG_0
try:
sys.stdout.write(struct.pack("<L", model[s].as_long()).decode('ascii'))
except: pass
print('')
And indeed, running the script finally yields the flag (notice the execution time, though):
STOP at 0xa1f0L
eax
(FLAG_1, '0x30797b53')
(FLAG_2, '0x68735f75')
(FLAG_3, '0x646c7530')
(FLAG_4, '0x7634685f')
(FLAG_5, '0x54695f33')
(FLAG_6, '0x3130735f')
(FLAG_7, '0x5f646576')
(FLAG_8, '0x685f7962')
(FLAG_9, '0x21646e34')
(FLAG_10, '0x7d2121')
DrgnS{y0u_sh0uld_h4v3_iT_s01ved_by_h4nd!!!}
ebx
ecx
edx
esi
edi
ebp
./solve.py 6748,65s user 3,27s system 99% cpu 1:52:35,37 total
Feed it into the original binary to confirm:
julian@TPT440p ~/CTF/2015_05_CONFidence/rev400 % ./DeobfuscateMe.elf
Flag: DrgnS{y0u_sh0uld_h4v3_iT_s01ved_by_h4nd!!!}
Nice, that was the flag!