7.2 KiB
{% hint style="success" %}
Learn & practice AWS Hacking:
HackTricks Training AWS Red Team Expert (ARTE)
Learn & practice GCP Hacking: 
HackTricks Training GCP Red Team Expert (GRTE)
Support HackTricks
- Check the subscription plans!
- Join the 💬 Discord group or the telegram group or follow us on Twitter 🐦 @hacktricks_live.
- Share hacking tricks by submitting PRs to the HackTricks and HackTricks Cloud github repos.
Kwa msingi, chombo hiki kitatusaidia kupata thamani za mabadiliko ambayo yanahitaji kutimiza masharti fulani na kuhesabu kwa mkono kutakuwa na usumbufu mkubwa. Hivyo, unaweza kuonyesha kwa Z3 masharti ambayo mabadiliko yanahitaji kutimiza na itapata baadhi ya thamani (ikiwa inawezekana).
Baadhi ya maandiko na mifano yameondolewa kutoka https://ericpony.github.io/z3py-tutorial/guide-examples.htm
Basic Operations
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
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))
Kuchapisha Mfano
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]))
Hesabu ya Mashine
CPUs za kisasa na lugha za programu za kawaida hutumia hesabu juu ya bit-vectors zenye ukubwa wa kudumu. Hesabu ya mashine inapatikana katika Z3Py kama 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
Signed/Unsigned Numbers
Z3 inatoa toleo maalum la operesheni za kihesabu ambapo ina umuhimu ikiwa bit-vector inachukuliwa kama signed au unsigned. Katika Z3Py, waendeshaji <, <=, >, >=, /, % na >> wanalingana na toleo la signed. Waendeshaji wa unsigned husika ni ULT, ULE, UGT, UGE, UDiv, URem na 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))
Functions
Kazi za tafsiri kama za hesabu ambapo kazi + ina tafsiri ya kawaida isiyobadilika (inaongeza nambari mbili). Kazi zisizo na tafsiri na constants ni za kiwango cha juu cha kubadilika; zinaruhusu tafsiri yoyote ambayo ni sawa na vizuizi juu ya kazi au constant.
Mfano: f inatumika mara mbili kwa x inarudi x tena, lakini f inatumika mara moja kwa x ni tofauti na 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())
Mifano
Mchambuzi wa 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"
References
{% hint style="success" %}
Jifunze na fanya mazoezi ya AWS Hacking:HackTricks Training AWS Red Team Expert (ARTE)
Jifunze na fanya mazoezi ya GCP Hacking: HackTricks Training GCP Red Team Expert (GRTE)
Support HackTricks
- Angalia mpango wa usajili!
- Jiunge na 💬 kikundi cha Discord au kikundi cha telegram au tufuatilie kwenye Twitter 🐦 @hacktricks_live.
- Shiriki mbinu za hacking kwa kuwasilisha PRs kwa HackTricks na HackTricks Cloud repos za github.