In this first article, we will take a look at Z3, a very useful tool built by Microsoft Research. While it has been made as a powerful theorem prover, I am presenting it only from a reverse engineering perspective, specifically to solve a crack-me.

The main goal of this article is to present how Z3 can be used to generate a valid serial number given a known checking algorithm. I will go through a simple example and let you then browse the official documentation and other references for more advanced use cases.

For the story, Z3 helped me solving a crack-me that was part of an interview process. A win64 binary asking me for a serial number. Having spent a few hours on IDA , I came up with the checking algorithm along with one question :

Cool, I reversed the thing, now what?

Because I knew the algorithm responsible for checking, I knew what a satisfying serial must look like, a.k.a the constraints. Not being patient enough, I couldn’t wait for my broken PRNG-based brute-force to find a valid serial and fortunately I assisted an internal presentation on Z3 from a colleague a few days earlier. Enough story..

Installation

First thing first, you can find the tool on github on the Z3 Prover repository. As explained there, you’ll need to build it for your platform. Now you should be provided with several bindings including Python’s.

Problem set

Let’s say it’s Saturday morning around 3:42am, you are at Insomni’hack playing the CTF and finally done reversing that binary that could take you from the 40th to the 26th position on the score board (well you’ll do better next year). Good job, but the flag is like

INS{ANY_VALID_SERIAL}

(If you want to play with the challenge by yourself, you can just download the crackme from here.)

First, let’s break out the algorithm into simple constraints. The serial must :

  1. Be in the format XXXXXXXXXXXXXXXX (to make thing easier to follow, let’s call them groups of numbers, there are 4 groups right?)
  2. Where X is an int between [0..9]
    1. except for fourth_group where it must be in [3..8]
  3. fourth_group will be used as a cheksum
    1. its sum must be equal to the average of the first 3 groups
    2. its average must be equal to the sum of first_group
  4. sum of first_group must be different to sum of second_group
  5. first_group and fourth_group can’t have a similar value at the same index
  6. second_group and third_group can’t have a similar int at the same index

Screen Shot 2016-02-16 at 00.28.40

You could brute-force it, but you want to be sure you make it before 4:00am and brute-forcing is cheating.

Z3 constraint solvers

We’ll be using Python to get our thing done, but as long as you know any programming language I don’t think you would need to have a Python background to understand. However, if you want a quick refresh/intro, there we go Learn X in Y minutes, and come back in 5 minutes.

Also, you could read the basic example provided on the github if you want to have an idea of Z3.

Writing the constraints

Z3 comes with a few types, such as Int, Float, IntVector, etc.. Here I decided to use an IntVector for each group of four. First argument is the Z3 variable name, second the vector size. The Z3 variable name is used later to access the values from the generated model(s).

from z3 import *

first = IntVector(‘a’, 4)
second = IntVector(‘b’, 4)
third = IntVector(‘c’, 4)
fourth = IntVector(‘d’, 4)

The solver will be responsible for applying the constraints and getting the model(s).

# creating the solver
s = Solver()

Because we will need to play with sums and averages we calculate and store those values already. Remember we used the fourth group only for checksum.

# do the sums
sum_first = first[0]+first[1]+first[2]+first[3]
sum_second = second[0]+second[1]+second[2]+second[3]
sum_third = third[0]+third[1]+third[2]+third[3]
sum_fourth = fourth[0]+fourth[1]+fourth[2]+fourth[3]

# average of groups, excluding the 4th (checksum)
avg_sums = (sum_first+sum_second+sum_third)/3

Now that we have these values ready, let’s add the constraints, simply using add() from our solver instance.

#constraint #2 (using a custom function)
addConstraintBetweenXandY(s, first, 0, 9)
addConstraintBetweenXandY(s, second, 0, 9)
addConstraintBetweenXandY(s, third, 0, 9)
addConstraintBetweenXandY(s, fourth, 3, 8)

#constraint #3.1
s.add(sum_fourth == avg_sums)

#constraint #3.2
s.add(sum_first == sum_fourth/4)

#constaint #4
s.add(sum_first != sum_second)

#constraint #5
addConstraintNotEq(s, first, fourth)

#constraint #6
addConstraintNotEq(s, second, third)

Here are the two simple custom functions I used above addConstraintBetweenXandY and addConstraintNotEq.

def addConstraintBetweenXandY(solver, group, x, y):
for i in range(0, len(group)):
solver.add(group[i] >= x, group[i] < y)

def addConstraintNotEq(solver, g1, g2):
for i in range(0,4):
solver.add(g1[i] != g2[i])

 Getting the serial

Now that we are done with the constraints, we are ready to get our model. Before printing the model it is necessary to call check() to make sure there is at least a satisfying one and also because it is responsible for the model to be available.

if s.check():
m = s.model()
print m

The output should be as follow :

[a__1 = 0,
a__0 = 4,
c__1 = 8,
b__3 = 0,
a__2 = 0,
a__3 = 0,
d__3 = 7,
b__0 = 7,
d__1 = 3,
d__0 = 3,
c__2 = 7,
b__2 = 6,
c__0 = 8,
c__3 = 1,
b__1 = 7,
d__2 = 3]

Here you have the full raw output. Remember the variables we declared at the beginning? So now we have our serial in the form [variableName__index = value, …] which is quite enough to solve the challenge. But let’s just format them. To do so, you want to access the values using the index (a__0, a__1, …). Those can be retrieved through the model using the Python variable as an index.

for g in [first, second, third, fourth]:
print “{}{}{}{}”.format(m[g[0]], m[g[1]], m[g[2]], m[g[3]]),

There we go with the serial :

4000 7760 8871 3337

Conclusion

Z3 is a powerful tool capable of much more than what we’ve done in this post. As long as you are able to express the problem in the form of an equation this tool can help you.

In a similar use-case we could also brute-force the program, and you actually should if it could be run offline or if being noisy is not a matter. While writing this z3 script may take you a few minutes, what if your brute-force attack is successful before you finish? Worth a try at least. Just let it run and go do your things.

You can download the full Python script and the source of the crackme to play with. Also, tons of great examples are there in 0vercl0k’s Z3 playground.

Other resources

“Using Z3 to solve crackme”, Julien Bachman(milkmix_)

“Z3 101”, Axel Souchet(@0vercl0k)

Advertisements