7.3 KiB
{% hint style="success" %}
Leer & oefen AWS Hacking:
HackTricks Training AWS Red Team Expert (ARTE)
Leer & oefen GCP Hacking: 
HackTricks Training GCP Red Team Expert (GRTE)
Ondersteun HackTricks
- Kyk na die subskripsie planne!
- Sluit aan by die 💬 Discord groep of die telegram groep of volg ons op Twitter 🐦 @hacktricks_live.
- Deel hacking truuks deur PRs in te dien na die HackTricks en HackTricks Cloud github repos.
Baie basies, hierdie hulpmiddel sal ons help om waardes vir veranderlikes te vind wat aan sekere voorwaardes moet voldoen, en om dit met die hand te bereken sal baie irriterend wees. Daarom kan jy vir Z3 die voorwaardes aandui waaraan die veranderlikes moet voldoen en dit sal 'n paar waardes vind (indien moontlik).
Sommige teks en voorbeelde is onttrek van 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
Ints/Simplify/Reals
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
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]))
Masjien Aritmetiek
Moderne CPU's en hoofstroom programmeertale gebruik aritmetiek oor vaste-grootte bit-vektore. Masjien aritmetiek 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
Getekende/Ongetekende Getalle
Z3 bied spesiale getekende weergawes van wiskundige operasies waar dit 'n verskil maak of die bit-vectore as getekend of ongetekend behandel word. In Z3Py, die operateurs <, <=, >, >=, /, % en >> stem ooreen met die getekende weergawes. Die ooreenstemmende ongetekende operateurs 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 vaste standaardinterpretasie het (dit voeg twee getalle by). Nie-geïnterpreteerde funksies en konstantes is maksimaal buigsaam; hulle laat enige interpretasie toe wat konsekwent is met die beperkings oor die funksie of konstante.
Voorbeeld: f wat twee keer op x toegepas word, lei tot x weer, maar f wat een keer op x toegepas word, is anders as 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
{% hint style="success" %}
Leer & oefen AWS Hacking:HackTricks Opleiding AWS Red Team Expert (ARTE)
Leer & oefen GCP Hacking: HackTricks Opleiding GCP Red Team Expert (GRTE)
Ondersteun HackTricks
- Kyk na die subskripsie planne!
- Sluit aan by die 💬 Discord groep of die telegram groep of volg ons op Twitter 🐦 @hacktricks_live.
- Deel hacking truuks deur PRs in te dien na die HackTricks en HackTricks Cloud github repos.