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')