# Black magic? Using Z3 for automated crackme solving

## What is Z3?

Z3 is an open-source theorem prover by Microsoft (yes, seriously). In layman’s terms, you can give it any mathematically expressable problem and it will tell you if there is a solution for it and what the solution is. It’s not only a mathematician’s tool though - in this little introduction I would like to show you how you can use it to find a valid key for a super secret NSA tool (or just any CTF/Crackme challenge). It’s not meant to be a full tutorial, it’s just to show you that Z3 exists and how you can use it. You can find all the info you need for your specific problem in their documentary.

## Finding the ‘mathematically expressable problem’

Is there a way to solve the problem fast enough so that you have time to upload your work AND get the next plane to russia to escape the feds? This is where Z3 comes into play.

Have you watched or read the Hitchhiker’s guide? Of course you have. Z3 is like Deep Thought, it can give you any answer, but only if you have the right question. This introduction is not about the question, but about talking to Deep Thought. For this scenario I will assume that you have recovered the following ‘question’, or in Z3 terms, constraints, from the key checker:

• The key consists of 3 integers (x, y, z)
• x is a multiple of 7
• the LSB of the result of the bitwise or of x and y is 123
• x > 1337337
• z = avg(x, y)
• z < 42424242

That’s just what I’ve come up with spontanously, but Z3 can really solve anything you throw at it.

## Installation

`sudo pip install z3-solver`
It might take a while to compile. Don’t get fooled by the ‘z3’ packet that can also be installed with pip.

## Writing the solver

``````from z3 import *

# There are a few datatypes to choose from. For our purpose,
# 32-bit BitVecs are a good representation of ints. Z3 has its
# own int, which is more a 'mathematical int', it can get infinitely
# large and does not support bitwise operations.
x, y, z = BitVecs("x y z", 32)

s = Solver()
s.add((x | y) & 0xFF == 123)

#and check if a solution exists. If there is one, it will be printed.
if s.check():
print(s.model())
``````
``````\$ time python crack.py
[y = 3625989961, x = 719564090, z = 25293377]

real	0m0,255s
user	0m0,237s
sys	0m0,017s
``````

Bam! Instant result. That’s all. Easy, right?

## How does it work?

Black magic. Seriously, I advice you to just treat it as a black box.
If you DO want to find out about the crazy theory behind it, have a look at the wiki. https://github.com/Z3Prover/z3/wiki

## Where to go on from here?

Try it out! Try this challenge for example. A bruteforce solution is already provided, so if you want to skip the RE part you can find the constraints there and build your solver directly.

11 Likes

Could you provide a crackme that this will solve?

1 Like

Sure! Good idea, I’ve added one.

3 Likes

This topic was automatically closed after 30 days. New replies are no longer allowed.