Mirrors/hacktricks
2
0
Fork 0
mirror of https://github.com/carlospolop/hacktricks synced 2024-11-30 00:20:59 +00:00
Code Issues Projects Releases Packages Wiki Activity
hacktricks/reversing-and-exploiting/reversing-tools-basic-methods/satisfiability-modulo-theories-smt-z3.md
CPol 5b39029d68
GitBook: No commit message
2024-04-06 18:08:38 +00:00

9 KiB
Raw Blame History

Leer AWS-hacking van nul tot held met htARTE (HackTricks AWS Red Team Expert)!

Ander maniere om HackTricks te ondersteun:

Baie basies sal hierdie instrument ons help om waardes vir veranderlikes te vind wat aan sekere voorwaardes moet voldoen, en dit sal baie vervelig wees om dit met die hand te bereken. Daarom kan jy aan Z3 aandui watter voorwaardes die veranderlikes moet bevredig en dit sal enkele waardes vind (indien moontlik).

Sommige teks en voorbeelde is onttrek uit https://ericpony.github.io/z3py-tutorial/guide-examples.htm

Basiese Operasies

Booleans/En/Of/Nie

#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

Inte/Simplifiseer/Reëls

Die Z3 SMT-solver bied 'n verskeidenheid funksies vir die hantering van ints, vereenvoudiging en werk met reële getalle. Hier is 'n oorsig van die basiese metodes wat beskikbaar is:

Inte

  • Int is die tipe vir ints in Z3.
  • Jy kan ints skep deur die IntVal-funksie te gebruik, byvoorbeeld IntVal(42) sal 'n int met die waarde 42 skep.
  • Inte kan ook geskep word deur die Int-funksie te gebruik, byvoorbeeld Int('x') sal 'n int met die naam 'x' skep.
  • Inte kan gebruik word in wiskundige uitdrukkings, byvoorbeeld x + 2 of y * 3.

Vereenvoudiging

  • Die simplify-funksie kan gebruik word om wiskundige uitdrukkings te vereenvoudig.
  • Byvoorbeeld, simplify(x + 0) sal vereenvoudig na x, en simplify(x * 1) sal vereenvoudig na x.
  • Vereenvoudiging kan help om die uitdrukking te vereenvoudig en die oplossing te vind.

Reële getalle

  • Real is die tipe vir reële getalle in Z3.
  • Jy kan reële getalle skep deur die RealVal-funksie te gebruik, byvoorbeeld RealVal(3.14) sal 'n reële getal met die waarde 3.14 skep.
  • Reële getalle kan ook geskep word deur die Real-funksie te gebruik, byvoorbeeld Real('y') sal 'n reële getal met die naam 'y' skep.
  • Reële getalle kan gebruik word in wiskundige uitdrukkings, byvoorbeeld y + 2.5 of z * 1.5.

Met hierdie basiese metodes kan jy ints en reële getalle hanteer, vereenvoudig en gebruik in jou SMT-probleme met die Z3-solver.

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

Druk Model

To print the model generated by Z3, you can use the model method. This method returns a string representation of the model.

Om die model wat deur Z3 gegenereer is af te druk, kan jy die model metode gebruik. Hierdie metode gee 'n teksvoorstelling van die model terug.

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

Masjienrekenkunde

Moderne CPU's en algemene programmeertale gebruik rekenkunde oor vasgestelde grootte bit-vektore. Masjienrekenkunde is beskikbaar in Z3Py as Bit-Vektore.

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

Ondertekende/Ondertekende Getalle

Z3 bied spesiale ondertekende weergawes van aritmetiese operasies waar dit 'n verskil maak of die bit-vektor as ondertekend of onondertekend behandel word. In Z3Py, stem die operatore <, <=, >, >=, /, % en >> ooreen met die ondertekende weergawes. Die ooreenstemmende onondertekende operatore is ULT, ULE, UGT, UGE, UDiv, URem en 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))

Funksies

Geïnterpreteerde funksies soos aritmetika waar die funksie + 'n vasgestelde standaardinterpretasie het (dit tel twee getalle bymekaar). Ongeïnterpreteerde funksies en konstantes is maximaal buigsaam; hulle laat enige interpretasie toe wat konsekwent is met die beperkings oor die funksie of konstante.

Voorbeeld: f toegepas twee keer op x lei tot x weer, maar f toegepas een keer op x is verskillend van 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())

Voorbeelde

Sudoku-oplosser

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

Verwysings

Leer AWS-hacking van nul tot held met htARTE (HackTricks AWS Red Team Expert)!

Ander maniere om HackTricks te ondersteun: