Monday, February 10, 2014

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()

4 comments:

  1. what's z3 and what does it do?
    Cheers,

    ReplyDelete
  2. @michee
    It's a SAT/SMT solver from Microsoft. You basically throw an equation at it and it tries to determine whether it's solvable + get one solution for you.
    In this case we basically gave it the equations from PHP.
    s.add(something) means "AND the equation must be true for this expression". Please note that the argument of s.add is not a value; all the * ^ and == operations there are overloaded, and what is past to that function is the expression tree (equation) itself.
    Finally you do s.check() and it checks if it's solvable; and in the end you get the one solution (model).
    What I've written might be not accurate in all places, but that's the general idea. It's a good thing to have for crypto/keygenme-like tasks.

    Link: http://z3.codeplex.com/

    ReplyDelete