# Fun With Flags - Z3 SMT Solver

`Z3 `

is a satisfiability modulo theories (SMT) constraint solver. `Angr `

uses it, so in many cases we will use it too without noticing. However, there are some cases where angr may not work for us immediately and we may want to use `Z3 `

directly. I some cases angr is not appropriate in the first place such as this excellent JavaScript example by LiveOverflow:

https://www.youtube.com/watch?v=TpdDq56KH1I

Let's look at some c code snippet produced by `IDA `

from a CTF challenge.

`relation1 = *password - password[1];`

`relation2 = *password - password[2];`

`if ( initiallyzerothenthree`

` + initiallyzerothenthree`

` + password[2]`

` + -2 * relation2`

` + relation1 * initiallyzerothenthree`

` - password[3]`

` + onecalc )`

` {`

` ++accumulator;`

` }`

`if ( 222 * relation2 + 51 * relation1 - password[2] + password[3] != -8985 )`

` ++accumulator;`

`[....SNIP....]`

`accumulator += 1670 * (relation7 ^ 0x22 | relation9 ^ 0x36 | relation8 ^ 0x65);`

`[....SNIP....]`

`accumulator += onecalc + zerocalc + v9;`

` if ( accumulator )`

` return puts("Nope.");`

So this is not a simple one-by-one check. Several things are calculated and only on the very last check do we know if we have the right answer. Every check has the potential to change the accumulator, or not. All the checks together have to result in an accumulator value of `0`

. And this is the type of thing where `Z3 `

shines.

Lets write some rules in python for `Z3`

. Lets start with just setting up a symbolic password. I have borrowed a little from LiveOverflow...

`from z3 import *`

`import string`

`import subprocess`

`clearTextPassLength = 9 # dissassembly suggests a 9 character password; definitely constrains between 4 and 14`

`z3Solver = Solver() # create a Z3 solver`

`passwordString = ""`

`# creating a string of password character fields like this: pw[0] pw[1] pw[2] pw[3] pw[4] pw[5] pw[6] pw[7] pw[8] .....`

`for i in range(0, clearTextPassLength):`

` passwordString += "pw[{}] ".format(i) `

`# turning the paswordString into a list of 8-bit bit vectors. each list item is of type <class 'z3.z3.BitVecRef'>`

`passwordList = BitVecs(passwordString, 8) `

`# now add a rule for each 8-bit value that it has to be printable ascii`

`for i in range(0, clearTextPassLength):`

`z3Solver.add(Or(`

` And((passwordList[i] >= 32),(passwordList[i] <= 126))`

` #And((passwordList[i] >= 63),(passwordList[i] <= 90)), # change this and one line above to refine ascii range`

` ))`

We can then start to encode the constraints from the c code

`# encode the first if statement`

`# define 'relation1' in both python and Z3 name space using the same name to avoid confusion`

`relation1 = BitVec('relation1',32)`

`z3Solver.add(relation1 == SignExt(24,passwordList[0]) - SignExt(24,passwordList[1]))`

`relation2 = BitVec('relation2',32)`

`z3Solver.add(relation2 == SignExt(24,passwordList[0]) - SignExt(24,passwordList[2]))`

`relation3 = 6 - 2*relation2 + relation1*3 + onecalc`

`z3Solver.add(0 < (relation3 + SignExt(24,passwordList[2]) - SignExt(24,passwordList[3]) + onecalc))`

Note, that what I did here is make an assumption for the

`if ( initiallyzerothenthree`

` + initiallyzerothenthree`

` + password[2]`

` + -2 * relation2`

` + relation1 * initiallyzerothenthree`

` - password[3]`

` + onecalc )`

` {`

` ++accumulator;`

` }`

calculation to evaluate to true, because it constrains the solution space significantly.

Similarly, for the if statement

`if ( 222 * relation2 + 51 * relation1 - password[2] + password[3] != -8985 )`

` ++accumulator;`

we will assume that we don't want it to evaluate to true for the same reason.

`z3Solver.add((222*relation2 + 51*relation1 - SignExt(24,passwordList[2]) + SignExt(24,passwordList[3])) == -8985)`

In general, one has to be very careful about the bitvectors to represent the computer hardware and assembly instructions. All the `passwordList[]`

items are 8-bit ASCII encoded characters. It matters if the assembly instructions perform operations on these in 8/16/32/64 bit registers. `SignExt(24,passwordList[2])`

extends the 8-bit bitvector to a 32 bit bitvector. This assembly code loads the 8-bit value and sign extends it to 32 bits before performing the next operations:

Once all the constraints have been added, we can cycle through the solutions and print them out. If we did everything right, there should be just a single solution which is the flag.

`while (z3Solver.check() == z3.sat):`

` model = z3Solver.model()`

` modelAsString = ""`

` removalList = []`

` for i in passwordList:`

` if model[i] != None:`

` modelAsString += chr(model[i].as_long()&0xff)`

` removalList.append(i!=model[i]) `

` z3Solver.add(Or(removalList[:-1])) # remove found model from next iteration by adding it to the constraint list`

` print(modelAsString)`

` print('\n') `