Olympic CTF 2014 - Welcome To Forensics (500)

"Welcome To Forensics" or WTF for short (and believe us when we say that the name is most fitting) was a stegano/forensics/crackme challenge on the Olympic CTF Sochi 2014, which was organized by the MSLC. On behalf of the Dragon Sector this task was solved by gynvael and mak.

We were given a 46KB WTF.BIN file which looked like nothing in particular:

And let's be honest by saying that we had no idea what to do with it until a hint was published some hours later.

The hint basically said "look at 0x4525". At that offset there were three characters that basically revealed what this task is about:

<?#

Yes, this is PHP.

While it seems hard to believe, running this binary randomness in the PHP interpreter doesn't throw any errors (just noticed; note: in php.ini the short_open_tags needs to be enabled). Looking deeper into it one starts to notice a schema - everything is separated into lines and each line has some PHP code which is followed by a line comment sign (either # or //) and a lot of binary trash. The funny thing is that the PHP code also looks like binary randomness since PHP allows names to be non-ASCII and even promotes some of them to constant strings. For example (yellow = PHP code, violet = comment start):

Please note that the markings might be incorrect, but it should give you the general idea.

Instead of trying to deobfuscate this we decided to start with a trace using Xdebug's trace options and asked it to dump the parameters of called functions as well as the returned values. We got the following output:

So this basically gave us a BASIC-looking-but-still-PHP crackme (see Appendix A at the bottom for full source).

To find the answer we used Z3 (see Appendix B) which quickly found that the flag is:

QB4SIC_f0rever!!

To sum up, starting was the hard part in this task - the rest was rather simple if one had the correct tools (Xdebug, Z3).

Appendix A - crackme

eval('FUNCTION FUNCTI0N($PARAMETER) { 
/* ' OMFG A FUNCTION !!! */ 
IF (STRLEN($PARAMETER) <> 16): 
RETURN FALSE; 
ENDIF; 
DIM; $ARRAY = ARRAY(); 
FOR ($I = 1; $I <= STRLEN($PARAMETER); $I++): 
$ARRAY[$I] = ORD(SUBSTR($PARAMETER, $I - 1, 1)); 
ENDFOR; 
IF ((($ARRAY[3] * $ARRAY[6]) ^ ($ARRAY[2] * $ARRAY[2])) - 7320): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[11] * $ARRAY[14]) ^ ($ARRAY[9] * $ARRAY[11])) - 15882): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[14] * $ARRAY[15]) ^ ($ARRAY[11] * $ARRAY[4])) - 11789): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[1] * $ARRAY[9]) ^ ($ARRAY[8] * $ARRAY[9])) - 7184): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[13] * $ARRAY[16]) ^ ($ARRAY[7] * $ARRAY[11])) - 10366): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[9] * $ARRAY[4]) ^ ($ARRAY[4] * $ARRAY[2])) - 6902): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[13] * $ARRAY[15]) ^ ($ARRAY[11] * $ARRAY[16]))): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[14] * $ARRAY[6]) ^ ($ARRAY[6] * $ARRAY[1])) - 2277): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[10] * $ARRAY[9]) ^ ($ARRAY[16] * $ARRAY[15])) - 4385): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[2] * $ARRAY[7]) ^ ($ARRAY[1] * $ARRAY[10])) - 15468): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[3] * $ARRAY[14]) ^ ($ARRAY[6] * $ARRAY[15])) - 8075): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[6] * $ARRAY[3]) ^ ($ARRAY[5] * $ARRAY[10])) - 11550): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[5] * $ARRAY[3]) ^ ($ARRAY[9] * $ARRAY[8])) - 7668): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[13] * $ARRAY[12]) ^ ($ARRAY[12] * $ARRAY[1])) - 3032): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[7] * $ARRAY[4]) ^ ($ARRAY[8] * $ARRAY[13])) - 14067): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[6] * $ARRAY[3]) ^ ($ARRAY[7] * $ARRAY[7])) - 11997): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[12] * $ARRAY[11]) ^ ($ARRAY[5] * $ARRAY[8])) - 13208): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[5] * $ARRAY[16]) ^ ($ARRAY[7] * $ARRAY[13])) - 11282): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[2] * $ARRAY[12]) ^ ($ARRAY[13] * $ARRAY[2])) - 1126): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[8] * $ARRAY[15]) ^ ($ARRAY[9] * $ARRAY[2])) - 326): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[5] * $ARRAY[11]) ^ ($ARRAY[15] * $ARRAY[12])) - 5115): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[16] * $ARRAY[2]) ^ ($ARRAY[15] * $ARRAY[7])) - 1213): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[13] * $ARRAY[12]) ^ ($ARRAY[1] * $ARRAY[16])) - 9471): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[6] * $ARRAY[16]) ^ ($ARRAY[1] * $ARRAY[3])) - 6359): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[16] * $ARRAY[5]) ^ ($ARRAY[14] * $ARRAY[9])) - 7177): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[14] * $ARRAY[10]) ^ ($ARRAY[10] * $ARRAY[1])) - 5846): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[4] * $ARRAY[3]) ^ ($ARRAY[13] * $ARRAY[12])) - 15954): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[8] * $ARRAY[8]) ^ ($ARRAY[1] * $ARRAY[14])) - 3254): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[4] * $ARRAY[15]) ^ ($ARRAY[7] * $ARRAY[8])) - 12137): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[3] * $ARRAY[10]) ^ ($ARRAY[5] * $ARRAY[4])) - 131): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[5] * $ARRAY[4]) ^ ($ARRAY[6] * $ARRAY[10])) - 2685): 
RETURN FALSE; 
ENDIF; 
IF ((($ARRAY[11] * $ARRAY[12]) ^ ($ARRAY[10] * $ARRAY[14])) - 7242): 
RETURN FALSE; 
ENDIF; 
RETURN "YES, $PARAMETER"; 
} 

RETURN TRUE;')

Appendix B (z3 solution by mak)

from z3 import *
array = [ BitVec('a%i'%i,8) for i in range(0,17)]


s = Solver()
s.add(((array[3] * array[6]) ^ (array[2] * array[2])) == 7320)
s.add(((array[11] * array[14]) ^ (array[9] * array[11])) == 15882)
s.add(((array[14] * array[15]) ^ (array[11] * array[4])) == 11789) 
s.add(((array[1] * array[9]) ^ (array[8] * array[9])) == 7184) 
s.add(((array[13] * array[16]) ^ (array[7] * array[11])) == 10366) 
s.add(((array[9] * array[4]) ^ (array[4] * array[2])) == 6902)          
s.add(((array[13] * array[15]) ^ (array[11] * array[16])) == 0)
s.add(((array[14] * array[6]) ^ (array[6] * array[1])) == 2277) 
s.add(((array[10] * array[9]) ^ (array[16] * array[15])) == 4385) 
s.add(((array[2] * array[7]) ^ (array[1] * array[10])) == 15468) 
s.add(((array[3] * array[14]) ^ (array[6] * array[15])) == 8075) 
s.add(((array[6] * array[3]) ^ (array[5] * array[10])) == 11550) 
s.add(((array[5] * array[3]) ^ (array[9] * array[8])) == 7668) 
s.add(((array[13] * array[12]) ^ (array[12] * array[1])) == 3032) 
s.add(((array[7] * array[4]) ^ (array[8] * array[13])) == 14067) 
s.add(((array[6] * array[3]) ^ (array[7] * array[7])) == 11997) 
s.add(((array[12] * array[11]) ^ (array[5] * array[8])) == 13208) 
s.add(((array[5] * array[16]) ^ (array[7] * array[13])) == 11282) 
s.add(((array[2] * array[12]) ^ (array[13] * array[2])) == 1126) 
s.add(((array[8] * array[15]) ^ (array[9] * array[2])) == 326) 
s.add(((array[5] * array[11]) ^ (array[15] * array[12])) == 5115) 
s.add(((array[16] * array[2]) ^ (array[15] * array[7])) == 1213) 
s.add(((array[13] * array[12]) ^ (array[1] * array[16])) == 9471) 
s.add(((array[6] * array[16]) ^ (array[1] * array[3])) == 6359) 
s.add(((array[16] * array[5]) ^ (array[14] * array[9])) == 7177) 
s.add(((array[14] * array[10]) ^ (array[10] * array[1])) == 5846) 
s.add(((array[4] * array[3]) ^ (array[13] * array[12])) == 15954) 
s.add(((array[8] * array[8]) ^ (array[1] * array[14])) == 3254) 
s.add(((array[4] * array[15]) ^ (array[7] * array[8])) == 12137) 
s.add(((array[3] * array[10]) ^ (array[5] * array[4])) == 131) 
s.add(((array[5] * array[4]) ^ (array[6] * array[10])) == 2685) 
s.add(((array[11] * array[12]) ^ (array[10] * array[14])) == 7242) 

for i in range(1,17):
    s.add(array[i] >= 32 and array[i] <= 126)

print s.check()
print s.model()