dimanche 21 septembre 2014

CSAW 2014 Exploit 500 writeup : xorcise

The CSAW 2014 Exploit500 challenge was a Linux 32-bit network service for which the executable and the source code were provided (I saved a copy of the source code here). The service accepts packets defined by the structure cipher_data and first applies a decryption loop to the received data.

struct cipher_data
    uint8_t length;
    uint8_t key[8];
    uint8_t bytes[128];
typedef struct cipher_data cipher_data;

The service provides  multiple commands, however the 2 interesting ones, read_file and system, require your packet to be authenticated. The authentication verification is done in is_authenticated() and computes an authentication checksum based on a password read from the local file 'password.txt'. This check does not seem to be vulnerable.

My teammate EiNSTeiN_ discovered that there is a flaw in the decipher() method that does the decryption of the data. The function allocates a buffer buf which will contain the decrypted data, the allocated size is MAX_BLOCKS * BLOCK_SIZE which is 128 bytes. The copy of the packet bytes to the buffer is done safely with memcpy.

#define BLOCK_SIZE 8
#define MAX_BLOCKS 16
memcpy(buf, data->bytes, sizeof(buf));

There is also a check to ensure that the decryption loop does not process more than the size of the buffer buf[].

    if ((data->length / BLOCK_SIZE) > MAX_BLOCKS)
        data->length = BLOCK_SIZE * MAX_BLOCKS;

But this check is flawed, we can pass a value of 135 which will pass the check (135 / 8 equals 16 which is not bigger than MAX_BLOCKS). The decryption loop is applied by blocks of 8 bytes, so we are able to apply it to 8 bytes outside of buf[].

    for (loop = 0; loop < data->length; loop += 8)
        for (block_index = 0; block_index < 8; ++block_index)

If we look at the stack layout of decipher() we see that those 8 bytes are the variables xor_mask, block_index and the first 3 bytes of loop.

-00000095 buf             db 128 dup(?)
-00000015 xor_mask        db ?
-00000014 block_index     dd ?
-00000010 loop            dd ?

The strategy I went for is to modify the value of loop to make it point on the return address of decipher() and modify it's 2 first bytes to make it return somewhere else. Hopefully we can find an interesting place to jump to.

Let's go through the modification of the bytes one at a time. The first one is xor_mask. At this point block_index equals 0. We know 2 of the values in the decryption (xor_mask = 0x8F and buf[loop+block_index] = 0x8F), so we can set key[block_index] to get the output value we want, let's set xor_mask to 0 to make the next steps easier. 0x8F ^ 0x8F ^ 0x00 equals 0x00, so this is the value we will put at key[0].

variable          : prev_val   block_index  new_val key_value    
xor_mask       : 0x8F       0            0x00    key[0] = 0x00     

Next up is the first byte of block_index, at this point it is equal to 1. We will keep it's value at 1 so the decryption loop continues normally. As we have modified xor_mask to 0x00, the computation is now 0x01 ^ 0x01 ^ 0x00 which equals 0x00, we put this value in key[1]. We will also leave the other bytes of block_index unchanged. Here is the status of our table so far :

variable : prev_val block_index new_val key_value xor_mask : 0x8F 0 0x00 key[0] = 0x00 block_index[0] : 0x01 1 0x01 key[1] = 0x00 block_index[1] : 0x00 2 0x00 key[2] = 0x00 block_index[2] : 0x00 3 0x00 key[3] = 0x00 block_index[3] : 0x00 4 0x00 key[4] = 0x00

We can now modify the first byte of loop. It's current value is 0x80 (128), the value we need to make buf[loop+block_index] modify the return address at this point is 0x93, so that will give us key[5] = 0x13.

variable       : prev_val   block_index  new_val key_value  
loop[0]        : 0x80       5            0x93    key[5] = 0x13 

We are now able to modify the return address of decipher(), we're making good progress. So where do we want to make the program jump? There is a call to read_file()in process_connection(), this command reads the content of a file and sends its content back to us, we could use it to read the content of 'password.txt'.

.text:08049279                 mov     eax, [ebp+var_10]
.text:0804927C                 add     eax, 8
.text:0804927F                 sub     esp, 8
.text:08049282                 push    eax
.text:08049283                 push    offset aReadFileReques ; "Read File Request: %s\n"
.text:08049288                 call    _printf
.text:0804928D                 add     esp, 10h
.text:08049290                 mov     eax, [ebp+var_10]
.text:08049293                 add     eax, 8
.text:08049296                 sub     esp, 8
.text:08049299                 push    eax             ; filename
.text:0804929A                 push    [ebp+fd]        ; fd
.text:0804929D                 call    read_file

There is a little detail to keep in mind, there is a stack adjustment after the call to decipher(), as we are hijacking the return address the stack will not be properly readjusted.

.text:0804918F                 call    decipher
.text:08049194                 add     esp, 10h
;274     packet = (request *)&decrypted;
.text:08049197                 lea     eax, [ebp+var_11D]

.text:0804919D                 mov     [ebp+var_10], eax

My first thought was to jump at 0804928D which does the same stack adjustment and then sets the correct parameters for the call to read_file(). However this approach does not work as the value of var_10 is set only after the call to decipher(). Bummer.

I then noticed that the address of filename is passed via eax at 0x08049299 and it happens that at the end of decipher() eax points inside buf[]. So the last thing I needed to do was to adjust the initial packet content so that it contained 'password.txt\x00' XOR 0x8F XOR the key. Here is the final content of the variable smashing table.

variable       : prev_val   block_index  new_val key_value    
xor_mask       : 0x8F       0            0x00    key[0] = 0x00        
block_index[0] : 0x01       1            0x01    key[1] = 0x00 
block_index[1] : 0x00       2            0x00    key[2] = 0x00
block_index[2] : 0x00       3            0x00    key[3] = 0x00
block_index[3] : 0x00       4            0x00    key[4] = 0x00
loop[0]        : 0x80       5            0x93    key[5] = 0x13
at this point buf[loop+block_index] overwrites retaddr

retaddr[1]     : 0x94       6            0x99    key[6] = 0x0d
retaddr[2]     : 0x91       7            0x92    key[7] = 0x03

And below is the source code of my exploit, I used the pwntools python library by Gallopsled which saved me a ton of time for other challenges, definitely check it out.

And finally the exploit in action :

[ekse@xubuntu] : ~/csaw/exploit500 $ python client.py 
[+] Opening connection to on port 24001: OK
[*] Switching to interactive mode
[*] Got EOF while reading in interactive

So the password was 'pass123', I was kind of depressing to have worked so much for such a weaksauce password, the CSAW CTF organizers really are a bunch of trolls. Now we could implement the packet authentication and call the system command to list the files on the server, but I guessed the flag was probably in 'flag.txt' and used the exploit to read that file instead :-)

The flag was flag{code_exec>=crypto_break}.

Thanks to drraid for this great challenge to the CSAW organizers for such a great CTF!

dimanche 10 août 2014

Solving picoCTF 2013 Harder Serial with Z3

In the past weeks I have been watching LiveCTF, a project to livestream speedruns of wargames and CTF challenges. This is a great learning tool as you get to see the thought process of the caster as well as the tools and tricks they use to solve the challenges. 

I also recently learned about picoCTF, a capture the flag game made for high school teams organized by PPP.  I have been playing the 2013 edition in the last few days and it is actually really well made, for someone new to CTF I would definitely recommend starting with this one. It also has interesting challenges even for seasoned CTF players, you can play the 2013 edition by registering here.

I decided to try to speedrun picoCTF and focus on optimizing my work process when going through the challenges. In this post I will show how to solve the 'Harder Serial' challenge using Z3.

The challenge
Harder Serial comes in the form of a Python script, we need to find a working serial for the RoboCorpIntergalactic software. The full script code is below.

As we can see the program expects a 20 digits serial and the check_serial() function checks a number of conditions on the values of the digits with simple operations. It probably can be solved by hand but it is a perfect use case for Z3. In short, Z3 is an open-source theorem prover than allows us to define conditions to be met and will output if the conditions are satisfiable as well a set of values that meet all those conditions. The inner workings of Z3 and SMT solvers are a complex topic but Z3 itself is actually easy to use.

I will now go through my solution code, if you prefer to see the full script you can find it here. Z3 uses its own syntax but luckily there are Python bindings which will make it easy to define the conditions. We start by importing z3 and defining integer variables for the serial digits.

Then we create an instance of the solver and add our conditions to it. The first set of conditions define the serial digits as values between 0 and 9.

Then we add the conditions from the serial_check() function. To save time I used a couple of search and replace in a text editor to avoid typing them manually.

We add a condition to make s[3] different than zero because one of the conditions divides by it, Z3 will accept 0 as a valid value but Python will throw an exception. Finally we call solver.check() which will determine if the solver is able to meet the conditions and solver.model() which will return a set of values that meet those conditions.

>python break_serial.py
[s[8] = 5,
 s[4] = 3,
 s[19] = 2,
 s[17] = 8,
 s[16] = 8,
 s[2] = 8,
 s[9] = 7,
 s[1] = 2,
 s[3] = 1,
 s[15] = 7,
 s[11] = 0,
 s[10] = 9,
 s[12] = 3,
 s[18] = 1,
 s[0] = 4,
 s[14] = 5,
 s[7] = 4,
 s[6] = 2,
 s[5] = 7,
 s[13] = 9]

Again with a bit of search/replace and some python we can get our serial.
>>> s = [0] * 20
>>> s[8] = 5
>>> s[4] = 3
>>> s[19] = 2
>>> s[17] = 8
>>> s[16] = 8
>>> s[2] = 8
>>> s[9] = 7
>>> s[1] = 2
>>> s[3] = 1
>>> s[15] = 7
>>> s[11] = 0
>>> s[10] = 9
>>> s[12] = 3
>>> s[18] = 1
>>> s[0] = 4
>>> s[14] = 5
>>> s[7] = 4
>>> s[6] = 2
>>> s[5] = 7
>>> s[13] = 9
>>> "".join([str(x) for x in s])

We validate that our key is accepted :

> python harder_serial.py 42813724579039578812
Please enter a valid serial number from your RoboCorpIntergalactic purchase

Thank you! Your product has been verified!

This was a rather simple use of Z3, for examples of advanced use of Z3 for reverse engineering see the following articles:

Breaking Kryptonite's Obfuscation: A Static Analysis Approach Relying on Symbolic Execution by Axel Souchet and
Concolic execution - Taint analysis with Valgrind and constraints path solver with Z3 by Jonathan Salwan.

As always feel free to leave a comment or send me a message on Twitter if you have questions or comments!