Serbian - Ht
HackTricks Training Twitter Linkedin Sponsor

Z3 - Satisfiability Modulo Theories (SMT)

Naučite hakovanje AWS-a od nule do heroja sa htARTE (HackTricks AWS Red Team Expert)!

Drugi načini podrške HackTricks-u:

Veoma jednostavno, ovaj alat će nam pomoći da pronađemo vrednosti za promenljive koje treba da zadovolje neke uslove, a ručno ih izračunavanje bi bilo veoma dosadno. Zato možete navesti Z3 uslove koje promenljive treba da zadovolje i on će pronaći neke vrednosti (ako je moguće).

Neki tekstovi i primeri su izvučeni sa https://ericpony.github.io/z3py-tutorial/guide-examples.htm

Osnovne operacije

Booleans/And/Or/Not

#pip3 install z3-solver
from z3 import *
s = Solver() #The solver will be given the conditions

x = Bool("x") #Declare the symbos x, y and z
y = Bool("y")
z = Bool("z")

# (x or y or !z) and y
s.add(And(Or(x,y,Not(z)),y))
s.check() #If response is "sat" then the model is satifable, if "unsat" something is wrong
print(s.model()) #Print valid values to satisfy the model

Celi brojevi/Pojednostavljivanje/Realni brojevi

from z3 import *

x = Int('x')
y = Int('y')
#Simplify a "complex" ecuation
print(simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5)))
#And(x >= 2, 2*x**2 + y**2 >= 3)

#Note that Z3 is capable to treat irrational numbers (An irrational algebraic number is a root of a polynomial with integer coefficients. Internally, Z3 represents all these numbers precisely.)
#so you can get the decimals you need from the solution
r1 = Real('r1')
r2 = Real('r2')
#Solve the ecuation
print(solve(r1**2 + r2**2 == 3, r1**3 == 2))
#Solve the ecuation with 30 decimals
set_option(precision=30)
print(solve(r1**2 + r2**2 == 3, r1**3 == 2))

Ispisivanje modela

To print the model, you can use the model object obtained from the solver. The model object contains the assignments for each variable in the formula.

Za ispisivanje modela, možete koristiti model objekat dobijen od rešavača. Model objekat sadrži dodeljene vrednosti za svaku promenljivu u formuli.

from z3 import *

x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
s.check()

m = s.model()
print ("x = %s" % m[x])
for d in m.decls():
print("%s = %s" % (d.name(), m[d]))

Mašinska aritmetika

Moderne CPU i popularni programski jezici koriste aritmetiku nad bit-vektorima fiksne veličine. Mašinska aritmetika je dostupna u Z3Py kao Bit-Vektori.

from z3 import *

x = BitVec('x', 16) #Bit vector variable "x" of length 16 bit
y = BitVec('y', 16)

e = BitVecVal(10, 16) #Bit vector with value 10 of length 16bits
a = BitVecVal(-1, 16)
b = BitVecVal(65535, 16)
print(simplify(a == b)) #This is True!
a = BitVecVal(-1, 32)
b = BitVecVal(65535, 32)
print(simplify(a == b)) #This is False

Potpisani/Nepotpisani brojevi

Z3 pruža posebne potpisane verzije aritmetičkih operacija gde je važno da li se bit-vektor tretira kao potpisan ili nepotpisan. U Z3Py, operatori <, <=, >, >=, /, % i >> odgovaraju potpisanim verzijama. Odgovarajući nepotpisani operatori su ULT, ULE, UGT, UGE, UDiv, URem i LShR.

from z3 import *

# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)
solve(x + y == 2, x > 0, y > 0)

# Bit-wise operators
# & bit-wise and
# | bit-wise or
# ~ bit-wise not
solve(x & y == ~y)
solve(x < 0)

# using unsigned version of <
solve(ULT(x, 0))

Funkcije

Tumačene funkcije kao što je aritmetika, gde funkcija + ima fiksnu standardnu interpretaciju (sabira dva broja). Neterpretirane funkcije i konstante su maksimalno fleksibilne; dozvoljavaju bilo koju interpretaciju koja je konzistentna sa ograničenjima nad funkcijom ili konstantom.

Primer: dva puta primenjena funkcija f na x rezultuje ponovo x, ali jednom primenjena funkcija f na x je različita od x.

from z3 import *

x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
s = Solver()
s.add(f(f(x)) == x, f(x) == y, x != y)
s.check()
m = s.model()
print("f(f(x)) =", m.evaluate(f(f(x))))
print("f(x)    =", m.evaluate(f(x)))

print(m.evaluate(f(2)))
s.add(f(x) == 4) #Find the value that generates 4 as response
s.check()
print(m.model())

Primeri

Rešavač Sudoku-a

from z3 import *

def solve_sudoku(grid):
    # Kreiranje Z3 konteksta
    solver = Solver()

    # Definisanje promenljivih za svako polje u mreži
    cells = [[Int(f"cell_{i}_{j}") for j in range(9)] for i in range(9)]

    # Dodavanje ograničenja za vrednosti polja
    for i in range(9):
        for j in range(9):
            # Vrednosti polja moraju biti između 1 i 9
            solver.add(And(cells[i][j] >= 1, cells[i][j] <= 9))

    # Dodavanje ograničenja za redove
    for i in range(9):
        solver.add(Distinct(cells[i]))

    # Dodavanje ograničenja za kolone
    for j in range(9):
        solver.add(Distinct([cells[i][j] for i in range(9)]))

    # Dodavanje ograničenja za kvadrante
    for i in range(0, 9, 3):
        for j in range(0, 9, 3):
            solver.add(Distinct([cells[x][y] for x in range(i, i + 3) for y in range(j, j + 3)]))

    # Dodavanje početnih vrednosti iz mreže
    for i in range(9):
        for j in range(9):
            if grid[i][j] != 0:
                solver.add(cells[i][j] == grid[i][j])

    # Rešavanje Sudoku-a
    if solver.check() == sat:
        model = solver.model()
        solution = [[model.evaluate(cells[i][j]).as_long() for j in range(9)] for i in range(9)]
        return solution
    else:
        return None

# Primer rešavanja Sudoku-a
grid = [
    [5, 3, 0, 0, 7, 0, 0, 0, 0],
    [6, 0, 0, 1, 9, 5, 0, 0, 0],
    [0, 9, 8, 0, 0, 0, 0, 6, 0],
    [8, 0, 0, 0, 6, 0, 0, 0, 3],
    [4, 0, 0, 8, 0, 3, 0, 0, 1],
    [7, 0, 0, 0, 2, 0, 0, 0, 6],
    [0, 6, 0, 0, 0, 0, 2, 8, 0],
    [0, 0, 0, 4, 1, 9, 0, 0, 5],
    [0, 0, 0, 0, 8, 0, 0, 7, 9]
]

solution = solve_sudoku(grid)
if solution is not None:
    for row in solution:
        print(row)
else:
    print("No solution found.")

Rešavač Sudoku-a

# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
for i in range(9) for j in range(9) ]

# each row contains a digit at most once
rows_c   = [ Distinct(X[i]) for i in range(9) ]

# each column contains a digit at most once
cols_c   = [ Distinct([ X[i][j] for i in range(9) ])
for j in range(9) ]

# each 3x3 square contains a digit at most once
sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j]
for i in range(3) for j in range(3) ])
for i0 in range(3) for j0 in range(3) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,9,4,0,3,0),
(0,0,0,5,1,0,0,0,7),
(0,8,9,0,0,0,0,4,0),
(0,0,0,0,0,0,2,0,8),
(0,6,0,2,0,1,0,5,0),
(1,0,2,0,0,0,0,0,0),
(0,7,0,0,0,0,5,2,0),
(9,0,0,0,6,5,0,0,0),
(0,4,0,9,7,0,0,0,0))

instance_c = [ If(instance[i][j] == 0,
True,
X[i][j] == instance[i][j])
for i in range(9) for j in range(9) ]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
m = s.model()
r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
for i in range(9) ]
print_matrix(r)
else:
print "failed to solve"

Reference

Naučite hakovanje AWS-a od nule do heroja sa htARTE (HackTricks AWS Red Team Expert)!

Drugi načini podrške HackTricks-u:

PreviousAngr - ExamplesNextCheat Engine

Last updated