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
solving...
sat
[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])
'42813724579039578812'

We validate that our key is accepted :

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

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!

Aucun commentaire:

Publier un commentaire