Polish - Ht
HackTricks Training Twitter Linkedin Sponsor

Z3 - Satisfiability Modulo Theories (SMT)

Naucz się hakować AWS od zera do bohatera z htARTE (HackTricks AWS Red Team Expert)!

Inne sposoby wsparcia HackTricks:

Bardzo podstawowo, ten narzędzie pomoże nam znaleźć wartości dla zmiennych, które muszą spełniać pewne warunki, a ręczne obliczanie ich byłoby uciążliwe. Dlatego możemy wskazać Z3 warunki, które zmienne muszą spełniać, a on znajdzie pewne wartości (jeśli to możliwe).

Niektóre teksty i przykłady są zaczerpnięte z https://ericpony.github.io/z3py-tutorial/guide-examples.htm

Podstawowe operacje

Boole'owskie/I/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

Liczby całkowite/Uprość/Liczby rzeczywiste

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

Drukowanie modelu

To print the model, you can use the model object obtained from the solver. The model object represents the satisfying assignment for the variables in the formula.

Aby wydrukować model, można użyć obiektu model uzyskanego z solvera. Obiekt model reprezentuje przypisanie wartości zmiennym w formule.

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

Arytmetyka maszynowa

Współczesne procesory i popularne języki programowania korzystają z arytmetyki na wektorach bitów o stałej wielkości. Arytmetyka maszynowa jest dostępna w Z3Py jako wektory bitowe.

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

Liczby ze znakiem/bez znaku

Z3 dostarcza specjalne wersje operacji arytmetycznych, w których istnieje różnica w traktowaniu wektora bitowego jako liczby ze znakiem lub bez znaku. W Z3Py, operatorzy <, <=, >, >=, /, % i >> odpowiadają wersjom ze znakiem. Odpowiednikiem tych operatorów bez znaku są 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))

Funkcje

Funkcje interpretowane takie jak arytmetyka, gdzie funkcja + ma ustaloną standardową interpretację (dodaje dwie liczby). Funkcje niewyinterpretowane i stałe są maksymalnie elastyczne; pozwalają na dowolną interpretację, która jest zgodna z ograniczeniami na funkcję lub stałą.

Przykład: dwukrotne zastosowanie funkcji f do x daje ponownie x, ale jednokrotne zastosowanie funkcji f do x jest różne 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())

Przykłady

Rozwiązywacz Sudoku

from z3 import *

def solve_sudoku(grid):
    # Tworzenie solvera Z3
    solver = Solver()

    # Tworzenie zmiennych dla każdej komórki Sudoku
    cells = [[Int(f"cell_{i}_{j}") for j in range(9)] for i in range(9)]

    # Dodawanie ograniczeń dla wartości komórek
    for i in range(9):
        for j in range(9):
            # Ograniczenie wartości od 1 do 9
            solver.add(And(cells[i][j] >= 1, cells[i][j] <= 9))

            # Ograniczenie wartości unikalnych w wierszach
            solver.add(Distinct(cells[i]))

            # Ograniczenie wartości unikalnych w kolumnach
            solver.add(Distinct([cells[k][j] for k in range(9)]))

    # Ograniczenie wartości unikalnych w blokach 3x3
    for i in range(0, 9, 3):
        for j in range(0, 9, 3):
            solver.add(Distinct([cells[i + di][j + dj] for di in range(3) for dj in range(3)]))

    # Dodawanie ograniczeń dla znanych wartości w siatce Sudoku
    for i in range(9):
        for j in range(9):
            if grid[i][j] != 0:
                solver.add(cells[i][j] == grid[i][j])

    # Rozwiązanie Sudoku
    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

# Przykładowa siatka Sudoku
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]
]

# Rozwiązanie Sudoku
solution = solve_sudoku(grid)
if solution:
    for row in solution:
        print(row)
else:
    print("Brak rozwiązania")

Wynik:

[5, 3, 4, 6, 7, 8, 9, 1, 2]
[6, 7, 2, 1, 9, 5, 3, 4, 8]
[1, 9, 8, 3, 4, 2, 5, 6, 7]
[8, 5, 9, 7, 6, 1, 4, 2, 3]
[4, 2, 6, 8, 5, 3, 7, 9, 1]
[7, 1, 3, 9, 2, 4, 8, 5, 6]
[9, 6, 1, 5, 3, 7, 2, 8, 4]
[2, 8, 7, 4, 1, 9, 6, 3, 5]
[3, 4, 5, 2, 8, 6, 1, 7, 9]
# 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"

Odwołania

Naucz się hakować AWS od zera do bohatera z htARTE (HackTricks AWS Red Team Expert)!

Inne sposoby wsparcia HackTricks:

PreviousAngr - ExamplesNextCheat Engine

Last updated