Black magic? Using Z3 for automated crackme solving

python

(A E S T H E T I C) #1

Or your math homework. Or anything, really. Z3’s rad. :sunglasses:

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’

This is the scenario: Let’s say you haxxed into the NSA and downloaded a sweet tool that can be used to hack the planet or whatever, but you need to put in a key first. You have already RE’d the key checker and you know how it works, and you could write a bruteforce script, but you haxxed into the mainframe earlier and found out that the feds are already on the way. You’re short on time! Your script might not finish before they get you and nobody will ever know about your sick skillz, about how you haxxed into the NSA, about the software you borrowed, about how you were able to RE it, because you can’t twitter from Guantanamo.

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. :sunglasses:

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)

#Now just add the constraints
s = Solver()
s.add(x % 7 == 0)
s.add((x | y) & 0xFF == 123)
s.add(x > 1337337)
s.add(z == (x + y)/2)
s.add(z < 42424242)

#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.


(fxbg) #2

Could you provide a crackme that this will solve?


(A E S T H E T I C) #3

Sure! Good idea, I’ve added one.