Using Z3

Microsoft's Theorem Prover

What is Z3?

Z3 is an SMT Solver, a program that can test whether a set of conditions can hold or not, and eventually find a valid solution. This is super helpful in the context of reverse engineering, where you sometimes want to find a valid input or reverse engineer a checker function.

Installing Z3

``````\$ git clone https://github.com/Z3Prover/z3
\$ cd z3
\$ python3 scripts/mk_make.py
\$ cd build
\$ make
\$ sudo make install``````

Wait for that to compile. Make sure you also install the Python bindings, which allow you to use Z3 from within Python:

``\$ pip install z3-solver``

Using Z3

Let's take the example of Hack The Box's Hissss challenge. Once you do the whole python decompilation step, you end up with a large `if` statement for the password:

``````if ord(password[0]) != 48
or ord('n') - ord(password[9]) != 1

else:

So we have a bunch of relations. Some of them are easy - `password[0] == 48`, `password[10] == str(3)`. Some, however, would require some thinking - the different characters are interrelated and appear in multiple statements. Sometimes, you might have other relations - for example, `password[4] > 68`.

What we really want is to be able to plug all of this into a program that will solve the system of statements. Enter Z3!

First, set up the solver:

``````from z3 import *

s = Solver()

password = [BitVec(f'char{i}', 8) for i in range(12)]``````

A `BitVec` is just a binary number. In this case, we are making them `8` bits long (like a character!) and also calling them `char0`, `char1`, etc. Each `charX` is the `X`th character of the flag, so `password` is really an array of characters which are represented in the form of `BitVec` so that Z3 understands them.

Now we add the conditions to the `Solver` object:

``````s.add(password[0] == 48)

We then grab the solution as well as setting an `answer` array of the correct length to populate:

``````s.check()            # generate the model if it exists
sol = s.model()      # grab the model  ``````

The values returned by `sol` are not in the simplest form possible, but we can extract the values for each index as so:

``````flag = [sol[f].as_long() for f in password]
flag = ''.join(chr(c) for c in flag)
print(flag)``````

We get `0p3n_s3sam3!`

Last updated