How to efficiently solve problems ranging from simple mathematical equations to advanced logical satisfiability.
What is Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT)
Boolean Satisfiability abbreviated SAT. Boolean stands for True or False and satisfiability is when it is true under some assignment of values to its variables. Meaning SAT solvers trying to find if the variables can be replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. The standard definition is:
SAT solvers determine the ‘satisfiability’ of boolean set of equations for a set of inputs.
In other hand the SMT practically doing the same thing, but it combines the power of SAT solvers and other types of solvers to solve more complicated formulas for example handling inequalities, uninterpreted functions. SMT can handle formulas that involve multiple theories such as linear arithmetic, bit-vectors, and arrays.
Intro into Z3 Solver
Why we were talking about SMT and SAT, because the Z3 is one of the SMTs. It can be used for a variety of purposes such as formal verification, model checking, static program analysis and lot more.
Often when navigating through this field you will come across the terms like:
Symbols (= variables),
Unsat/sat (= unsatisfiable/satisfiable), (= unsolvable/solvable)
Concrete values (= strings, decimals and integers)
Literals (= SAT variable in short)
Clauses (= combination of literals)
Bonus
P problem (Polynomial problem): Refers to problems that can be solved efficiently (in polynomial time [n² + n, n]) by a deterministic algorithm. Example: Sorting a list.
NP problem (Nondeterministic Polynomial problem): Refers to problems for which a solution can be quickly verified (in polynomial time). Example: Verifying a solution to a Sudoku puzzle.
How the Z3 actually works? Well here you go:
The fastest way how to demonstrate it, is how to solve Facebook quiz:
We can rewrite it into Z3 form, where flowers will be the symbols (variables):
from z3 import *
# flowers => Symbolic [Int] type
rflower = Int("rflower")
bflower = Int("bflower")
yflower = Int("yflower")
# rflower, bflower, yflower = Ints('rflower bflower yflower')
solver = Solver()
# (Constraints) Equations
solver.add(rflower + rflower + rflower == 60)
solver.add(rflower + bflower + bflower == 30)
solver.add(bflower - yflower == 3)
# note: if we know the result is positive, we can add constraint: flower > 0
# Solver.check => CheckSatResult[sat, unsat, unknown]
if solver.check() == sat:
model = solver.model()
print("Sat solution:")
print(
f"Answer is: {model[yflower]} + {model[rflower]} + {model[bflower]} =",
f"{model[yflower].as_long() + model[rflower].as_long() + model[bflower].as_long()}"
)
else:
print("unsat: No solution found.")
I think everything is straight forward except one thing why “.as_long()”? That’s because model[variable] is not Int, but class z3.z3.IntNumRef.
When we dive a little bit deeper and look how Z3 is actually solving these problems:
Solving reverse engineering challenge:
What do we even see? It’s binary that checks whatever license format is right or not, the license is hardcoded under some if statement, which has to be true in order to crack the binary.
The argc arguments is the number of arguments supplied we know we need to run the binary with at least one argument and the length is 32 bytes.
There are two approaches about this problem using Z3, we use it to solve as equation or with angr that will control flow of the program and try to brute force it until everything is met.
We will apply Z3 by rewriting the if statement into equation (you don’t need to do it manually, help yourself, for example you can use global replace)
There is a small catch with the conversion, the chars are from -128 to 127 and when they overflow it will move back and forth.
In order to solve this weird unusual acting we will use BitVecs, I thought of using a function to handle the logic, but I end up using BitVecs for the simplicity.
from z3 import *
def check_license_with_z3():
solver = Solver()
# Create array of bitvecs with size of 32
string = [BitVec(f"string_{i}", 8) for i in range(32)]
solver.add(
string[29] == string[5] - string[3] + ord("F"),
string[2] + string[22] == string[13] + ord("{"),
string[12] + string[4] == string[5] + 0x1c,
string[25] * string[23] == string[0] + string[17] + 0x17,
string[27] * string[1] == string[5] + string[22] + -21,
string[9] * string[13] == string[28] * string[3] + -9,
string[9] == ord("p"),
string[19] + string[21] == string[6] + -128,
string[16] == string[15] - string[11] + ord("0"),
string[7] * string[27] == string[1] * string[13] + ord("-"),
string[13] == string[18] + string[13] + -101,
string[20] - string[8] == string[9] + ord("|"),
string[31] == string[8] - string[31] + -121,
string[20] * string[31] == string[20] + 4,
string[24] - string[17] == string[21] + string[8] + -23,
string[7] + string[5] == string[5] + string[29] + ord(","),
string[12] * string[10] == string[1] - string[11] + -36,
string[31] * string[0] == string[26] + -27,
string[1] + string[20] == string[10] + -125,
string[18] == string[27] + string[14] + 2,
string[30] * string[11] == string[21] + ord("D"),
string[5] * string[19] == string[1] + -44,
string[13] - string[26] == string[21] + -127,
string[23] == string[29] - string[0] + ord("X"),
string[19] == string[8] * string[13] + -23,
string[6] + string[22] == string[3] + ord("S"),
string[12] == string[26] + string[7] + -114,
string[16] == string[18] - string[5] + ord("3"),
string[30] - string[8] == string[29] + -77,
string[20] - string[11] == string[3] + -76,
string[16] - string[7] == string[17] + ord("f"),
string[1] + string[21] == string[11] + string[18] + ord("+"),
)
if solver.check() == sat:
model = solver.model()
print(
"".join([
chr(c.as_long())
for c in [model.eval(string[i]) for i in range(len(string))]
])
)
print("License Correct")
return True
else:
print("License Invalid")
return False
(Bonus if we want to just get the string “License Correct”, it’s done by overwriting the if instruction.)
Conclusion
We’ve learnt about Z3, the most fundamental terminology in Z3, and how to solve basic problems with Z3.
With a little knowledge about Z3, you will be able to solve complex problems like rubic cube, sudoku, magic square and lot more.
If you enjoyed this article, clap👋 and follow me! Thanks for reading! Looking forward to seeing you in the future.
More Resources
Exemplar challenges: https://github.com/PwnFunction/learn-z3
Docs: https://github.com/Z3Prover/z3/wiki#background
YouTube explanation: https://www.youtube.com/watch?v=EacYNe7moSs