Naučite hakovanje AWS-a od nule do heroja sa htARTE (HackTricks AWS Red Team Expert)!
Drugi načini podrške HackTricks-u:
* Ako želite da vidite **vašu kompaniju reklamiranu na HackTricks-u** ili **preuzmete HackTricks u PDF formatu** proverite [**SUBSCRIPTION PLANS**](https://github.com/sponsors/carlospolop)!
* Nabavite [**zvanični PEASS & HackTricks swag**](https://peass.creator-spring.com)
* Otkrijte [**The PEASS Family**](https://opensea.io/collection/the-peass-family), našu kolekciju ekskluzivnih [**NFT-ova**](https://opensea.io/collection/the-peass-family)
* **Pridružite se** 💬 [**Discord grupi**](https://discord.gg/hRep4RUj7f) ili [**telegram grupi**](https://t.me/peass) ili nas **pratite** na **Twitter-u** 🐦 [**@carlospolopm**](https://twitter.com/hacktricks_live)**.**
* **Podelite svoje hakovanje trikove slanjem PR-ova na** [**HackTricks**](https://github.com/carlospolop/hacktricks) i [**HackTricks Cloud**](https://github.com/carlospolop/hacktricks-cloud) github repozitorijume.
Veoma jednostavno, ovaj alat će nam pomoći da pronađemo vrednosti za promenljive koje treba da zadovolje neke uslove, a ručno ih izračunavanje bi bilo veoma dosadno. Zato možete navesti Z3 uslove koje promenljive treba da zadovolje i on će pronaći neke vrednosti (ako je moguće).
**Neki tekstovi i primeri su izvučeni sa [https://ericpony.github.io/z3py-tutorial/guide-examples.htm](https://ericpony.github.io/z3py-tutorial/guide-examples.htm)**
# Osnovne operacije
## Booleans/And/Or/Not
```python
#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
```
## Celi brojevi/Pojednostavljivanje/Realni brojevi
```python
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))
```
## Ispisivanje modela
To print the model, you can use the `model` object obtained from the solver. The `model` object contains the assignments for each variable in the formula.
Za ispisivanje modela, možete koristiti `model` objekat dobijen od rešavača. `Model` objekat sadrži dodeljene vrednosti za svaku promenljivu u formuli.
```python
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]))
```
# Mašinska aritmetika
Moderne CPU i popularni programski jezici koriste aritmetiku nad **bit-vektorima fiksne veličine**. Mašinska aritmetika je dostupna u Z3Py kao **Bit-Vektori**.
```python
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
```
## Potpisani/Nepotpisani brojevi
Z3 pruža posebne potpisane verzije aritmetičkih operacija gde je važno da li se **bit-vektor tretira kao potpisan ili nepotpisan**. U Z3Py, operatori **<, <=, >, >=, /, % i >>** odgovaraju **potpisanim** verzijama. Odgovarajući **nepotpisani** operatori su **ULT, ULE, UGT, UGE, UDiv, URem i LShR.**
```python
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))
```
## Funkcije
**Tumačene funkcije** kao što je aritmetika, gde **funkcija +** ima **fiksnu standardnu interpretaciju** (sabira dva broja). **Neterpretirane funkcije** i konstante su **maksimalno fleksibilne**; dozvoljavaju **bilo koju interpretaciju** koja je **konzistentna** sa **ograničenjima** nad funkcijom ili konstantom.
Primer: dva puta primenjena funkcija f na x rezultuje ponovo x, ali jednom primenjena funkcija f na x je različita od x.
```python
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())
```
# Primeri
## Rešavač Sudoku-a
```python
from z3 import *
def solve_sudoku(grid):
# Kreiranje Z3 konteksta
solver = Solver()
# Definisanje promenljivih za svako polje u mreži
cells = [[Int(f"cell_{i}_{j}") for j in range(9)] for i in range(9)]
# Dodavanje ograničenja za vrednosti polja
for i in range(9):
for j in range(9):
# Vrednosti polja moraju biti između 1 i 9
solver.add(And(cells[i][j] >= 1, cells[i][j] <= 9))
# Dodavanje ograničenja za redove
for i in range(9):
solver.add(Distinct(cells[i]))
# Dodavanje ograničenja za kolone
for j in range(9):
solver.add(Distinct([cells[i][j] for i in range(9)]))
# Dodavanje ograničenja za kvadrante
for i in range(0, 9, 3):
for j in range(0, 9, 3):
solver.add(Distinct([cells[x][y] for x in range(i, i + 3) for y in range(j, j + 3)]))
# Dodavanje početnih vrednosti iz mreže
for i in range(9):
for j in range(9):
if grid[i][j] != 0:
solver.add(cells[i][j] == grid[i][j])
# Rešavanje Sudoku-a
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
# Primer rešavanja Sudoku-a
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]
]
solution = solve_sudoku(grid)
if solution is not None:
for row in solution:
print(row)
else:
print("No solution found.")
```
## Rešavač Sudoku-a
```python
# 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"
```
## Reference
* [https://ericpony.github.io/z3py-tutorial/guide-examples.htm](https://ericpony.github.io/z3py-tutorial/guide-examples.htm)
Naučite hakovanje AWS-a od nule do heroja sa htARTE (HackTricks AWS Red Team Expert)!
Drugi načini podrške HackTricks-u:
* Ako želite da vidite **vašu kompaniju reklamiranu na HackTricks-u** ili **preuzmete HackTricks u PDF formatu** proverite [**SUBSCRIPTION PLANS**](https://github.com/sponsors/carlospolop)!
* Nabavite [**zvanični PEASS & HackTricks swag**](https://peass.creator-spring.com)
* Otkrijte [**The PEASS Family**](https://opensea.io/collection/the-peass-family), našu kolekciju ekskluzivnih [**NFT-ova**](https://opensea.io/collection/the-peass-family)
* **Pridružite se** 💬 [**Discord grupi**](https://discord.gg/hRep4RUj7f) ili [**telegram grupi**](https://t.me/peass) ili nas **pratite** na **Twitter-u** 🐦 [**@carlospolopm**](https://twitter.com/hacktricks_live)**.**
* **Podelite svoje hakovanje trikove slanjem PR-ova na** [**HackTricks**](https://github.com/carlospolop/hacktricks) i [**HackTricks Cloud**](https://github.com/carlospolop/hacktricks-cloud) github repozitorijume.