Google CTF 2016 - Audio visual receiver by ret2libc

I worked on this challenge with @hanyone and @castor91, but at the end @rpaleari solved it with the old but gold (smart) brute force.

The program is very simple: it has 6 functions named up, down, left, right, a, b that change in some ways a global state variable and a check one. Moreover, the a function is the one that outputs the final flag.

The binary asks for one character at a time, calling up if the char is ‘u’, down if the char is ‘d’ and so on. On each inserted char the value of the state variable is inserted in a global buffer. That’s the same buffer that is XORed with the encrypted flag. So we just need to find the right sequence of functions that changes the state in the right way.

Let’s see what those functions look like:

def up(state, check, pos, cross_pos):
	check ^= state
	buffer[pos] = state
	pos = (pos + 1) % 33
	state *= 3 # each function changes the state in a different way
	return (state, check, pos, cross_pos)


def a(state, check, pos, cross_pos):
	check ^= state
	buffer[pos] = state
	pos = (pos + 1) % 33
	state = (state * 16) | (state >> 4)
	if cross[cross_pos] == check:
		check = 0
		cross_pos += 1
		if pos > 29:
			return print_flag()

First thing I thought was to use Z3. How to write the right constraints? We can think about it as an array of check variables and an array of state variables that represent the check/state variable at the i-th char.

check changes (almost) always in the same way:

xor_check = check[i] == check[i - 1] ^ state[i - 1]

Instead state can be changed in 6 different ways, depending on the character you write (u, d, l, r, a, b):

state[i] == (state[i-1] * 3) # up
state[i] == (state[i-1] >> 1) * 8) - (state[i-1] >> 1) # down
state[i] == (state[i-1] * 2) # left
state[i] == (state[i-1] >> 3)) | (state[i-1]*32) # right
state[i] == (state[i-1] * 16) | (state[i-1] >> 4) # a
state[i] == ~(state[i-1]) # b

cross_ptr always remains the same as the previous value, except in some cases when you press ‘a’, in particular when the check cross[cross_pos] == check is satisfied.

Notice that state[i] ^ flag[i] should give us our real flag, so we can add some constraints to make this value printable and also specify that the first four chars have to be “CTF{“ and the last one “}”. We can also specify that the last function to be executed has to be ‘a’, by specifying what should be the value of state[len(flag)].

At this point I ran my script expecting to find the flag soon, but I had many problems… I spent a lot of time trying to debug it, giving up after a while. Luckily another member of our team was able to solve the chal by bruteforcing.

After the competition I’ve chosen to look again at my approach and I’ve rewritten and rechecked all constraints again, but still nothing. Only after a while I have realized what a big mistake I made… Looking at the disassembly of the functions you can see that many of them are using the SHR instruction, which is a logical shift to the right. Python and z3 use, instead, the arithmetical right shift.

Indeed, fixing my constraints (and my python script) to use the logical shift, I was able to get the flag quickly.

Files for this challenge can be found here.

Written on April 30, 2016