Greek - Ht
HackTricks Training Twitter Linkedin Sponsor

Z3 - Satisfiability Modulo Theories (SMT)

Μάθετε το hacking του AWS από το μηδέν μέχρι τον ήρωα με το htARTE (HackTricks AWS Red Team Expert)!

Άλλοι τρόποι για να υποστηρίξετε το HackTricks:

Βασικά, αυτό το εργαλείο θα μας βοηθήσει να βρούμε τιμές για μεταβλητές που πρέπει να ικανοποιούν κάποιες συνθήκες και η χειροκίνητη υπολογιστική τους θα είναι ενοχλητική. Επομένως, μπορείτε να υποδείξετε στο Z3 τις συνθήκες που πρέπει να ικανοποιούν οι μεταβλητές και αυτό θα βρει κάποιες τιμές (εάν είναι δυνατόν).

Ορισμένα κείμενα και παραδείγματα εξάγονται από το https://ericpony.github.io/z3py-tutorial/guide-examples.htm

Βασικές Λειτουργίες

Λογικές Τιμές/Και/Ή/Όχι

#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

Ακέραιοι/Απλοποίηση/Πραγματικοί

Η βιβλιοθήκη Z3 παρέχει μια πληθώρα εργαλείων για την επίλυση προβλημάτων ικανοποίησης modulo θεωριών (SMT). Μερικά από αυτά τα εργαλεία περιλαμβάνουν τη δυνατότητα επίλυσης προβλημάτων με ακέραιους αριθμούς, απλοποίησης εκφράσεων και επίλυσης προβλημάτων με πραγματικούς αριθμούς.

Για την επίλυση προβλημάτων με ακέραιους αριθμούς, μπορούμε να χρησιμοποιήσουμε τη συνάρτηση Int της Z3. Αυτή η συνάρτηση μας επιτρέπει να δημιουργήσουμε μεταβλητές ακεραίους και να εκφράσουμε περιορισμούς μεταξύ αυτών των μεταβλητών. Έπειτα, μπορούμε να χρησιμοποιήσουμε τη συνάρτηση solve για να επιλύσουμε το πρόβλημα και να βρούμε μια λύση.

Για την απλοποίηση εκφράσεων, μπορούμε να χρησιμοποιήσουμε τη συνάρτηση Simplify της Z3. Αυτή η συνάρτηση μας επιτρέπει να μετατρέψουμε μια πολύπλοκη έκφραση σε μια απλούστερη μορφή, χωρίς να αλλάζει η σημασία της έκφρασης.

Για την επίλυση προβλημάτων με πραγματικούς αριθμούς, μπορούμε να χρησιμοποιήσουμε τη συνάρτηση Real της Z3. Αυτή η συνάρτηση μας επιτρέπει να δημιουργήσουμε μεταβλητές πραγματικούς αριθμούς και να εκφράσουμε περιορισμούς μεταξύ αυτών των μεταβλητών. Με τη χρήση της συνάρτησης solve, μπορούμε να επιλύσουμε το πρόβλημα και να βρούμε μια λύση.

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

Εκτύπωση Μοντέλου

To print the model, you can use the model object obtained from the solver. The model object represents the satisfying assignment for the given constraints.

print(model)

Για να εκτυπώσετε το μοντέλο, μπορείτε να χρησιμοποιήσετε το αντικείμενο model που έχετε λάβει από τον επιλύτη. Το αντικείμενο model αναπαριστά την ικανοποιητική ανάθεση για τους δεδομένους περιορισμούς.

print(model)
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]))

Μηχανική Αριθμητική

Οι σύγχρονοι επεξεργαστές και οι κύριες γλώσσες προγραμματισμού χρησιμοποιούν αριθμητικές πράξεις πάνω σε δυαδικούς αριθμούς με σταθερό μέγεθος. Η μηχανική αριθμητική είναι διαθέσιμη στο Z3Py ως Bit-Vectors.

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

Υπογεγραμμένοι/Ανυπογράμμιστοι Αριθμοί

Το Z3 παρέχει ειδικές υπογεγραμμένες εκδόσεις των αριθμητικών λειτουργιών όπου κάνει διαφορά εάν το bit-vector θεωρείται ως υπογεγραμμένο ή ανυπογεγραμμένο. Στην Z3Py, οι τελεστές <, <=, >, >=, /, % και >> αντιστοιχούν στις υπογεγραμμένες εκδόσεις. Οι αντίστοιχοι ανυπογεγραμμένοι τελεστές είναι ULT, ULE, UGT, UGE, UDiv, URem και 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))

Συναρτήσεις

Οι ερμηνευμένες συναρτήσεις όπως η αριθμητική, όπου η συνάρτηση + έχει μια σταθερή τυπική ερμηνεία (προσθέτει δύο αριθμούς). Οι μη ερμηνευμένες συναρτήσεις και σταθερές είναι μέγιστα ευέλικτες· επιτρέπουν οποιαδήποτε ερμηνεία που είναι συνεπής με τους περιορισμούς πάνω στη συνάρτηση ή σταθερά.

Παράδειγμα: η εφαρμογή της f δύο φορές στο x έχει ως αποτέλεσμα το x ξανά, αλλά η εφαρμογή της f μία φορά στο x είναι διαφορετική από το 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())

Παραδείγματα

Λύτης Sudoku

from z3 import *

def solve_sudoku(grid):
    # Δημιουργία μοντέλου Z3
    s = Solver()

    # Δημιουργία μεταβλητών για τις τιμές των κελιών
    cells = [[Int(f"cell_{i}_{j}") for j in range(9)] for i in range(9)]

    # Περιορισμοί για τις τιμές των κελιών
    for i in range(9):
        for j in range(9):
            # Οι τιμές των κελιών είναι από 1 έως 9
            s.add(And(cells[i][j] >= 1, cells[i][j] <= 9))

    # Περιορισμοί για τις τιμές των γραμμών
    for i in range(9):
        s.add(Distinct(cells[i]))

    # Περιορισμοί για τις τιμές των στηλών
    for j in range(9):
        s.add(Distinct([cells[i][j] for i in range(9)]))

    # Περιορισμοί για τις τιμές των τετραγώνων 3x3
    for i in range(0, 9, 3):
        for j in range(0, 9, 3):
            s.add(Distinct([cells[x][y] for x in range(i, i+3) for y in range(j, j+3)]))

    # Περιορισμός για τις αρχικές τιμές του πίνακα Sudoku
    for i in range(9):
        for j in range(9):
            if grid[i][j] != 0:
                s.add(cells[i][j] == grid[i][j])

    # Επίλυση του προβλήματος
    if s.check() == sat:
        m = s.model()
        solution = [[m.evaluate(cells[i][j]).as_long() for j in range(9)] for i in range(9)]
        return solution
    else:
        return None

# Αρχικός πίνακας 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]
]

# Επίλυση του Sudoku
solution = solve_sudoku(grid)

# Εκτύπωση της λύσης
if solution:
    for row in solution:
        print(row)
else:
    print("No solution found.")

Αυτός ο κώδικας χρησιμοποιεί τη βιβλιοθήκη Z3 για να επιλύσει ένα πρόβλημα Sudoku. Ο κώδικας δημιουργεί ένα μοντέλο Z3 και ορίζει τις μεταβλητές για τις τιμές των κελιών του Sudoku. Στη συνέχεια, ο κώδικας προσθέτει περιορισμούς για τις τιμές των κελιών, των γραμμών, των στηλών και των τετραγώνων 3x3. Επίσης, ο κώδικας προσθέτει περιορισμούς για τις αρχικές τιμές του πίνακα Sudoku. Τέλος, ο κώδικας επιλύει το πρόβλημα και εκτυπώνει τη λύση, αν υπάρχει.

# 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"

Αναφορές

Μάθετε το χάκινγκ του AWS από το μηδέν μέχρι τον ήρωα με το htARTE (HackTricks AWS Red Team Expert)!

Άλλοι τρόποι για να υποστηρίξετε το HackTricks:

PreviousAngr - ExamplesNextCheat Engine

Last updated