mirror of
https://github.com/carlospolop/hacktricks
synced 2024-11-22 20:53:37 +00:00
289 lines
15 KiB
Markdown
289 lines
15 KiB
Markdown
<details>
|
||
|
||
<summary><strong>Μάθετε το hacking του AWS από το μηδέν μέχρι τον ήρωα με το</strong> <a href="https://training.hacktricks.xyz/courses/arte"><strong>htARTE (HackTricks AWS Red Team Expert)</strong></a><strong>!</strong></summary>
|
||
|
||
Άλλοι τρόποι για να υποστηρίξετε το HackTricks:
|
||
|
||
* Εάν θέλετε να δείτε την **εταιρεία σας να διαφημίζεται στο HackTricks** ή να **κατεβάσετε το HackTricks σε μορφή PDF** ελέγξτε τα [**ΣΧΕΔΙΑ ΣΥΝΔΡΟΜΗΣ**](https://github.com/sponsors/carlospolop)!
|
||
* Αποκτήστε το [**επίσημο PEASS & HackTricks swag**](https://peass.creator-spring.com)
|
||
* Ανακαλύψτε [**The PEASS Family**](https://opensea.io/collection/the-peass-family), τη συλλογή μας από αποκλειστικά [**NFTs**](https://opensea.io/collection/the-peass-family)
|
||
* **Εγγραφείτε στη** 💬 [**ομάδα Discord**](https://discord.gg/hRep4RUj7f) ή στη [**ομάδα telegram**](https://t.me/peass) ή **ακολουθήστε** μας στο **Twitter** 🐦 [**@carlospolopm**](https://twitter.com/hacktricks_live)**.**
|
||
* **Μοιραστείτε τα hacking tricks σας υποβάλλοντας PRs στα** [**HackTricks**](https://github.com/carlospolop/hacktricks) και [**HackTricks Cloud**](https://github.com/carlospolop/hacktricks-cloud) αποθετήρια του github.
|
||
|
||
</details>
|
||
|
||
|
||
Βασικά, αυτό το εργαλείο θα μας βοηθήσει να βρούμε τιμές για μεταβλητές που πρέπει να ικανοποιούν κάποιες συνθήκες και η χειροκίνητη υπολογιστική τους θα είναι ενοχλητική. Επομένως, μπορείτε να υποδείξετε στο Z3 τις συνθήκες που πρέπει να ικανοποιούν οι μεταβλητές και αυτό θα βρει κάποιες τιμές (εάν είναι δυνατόν).
|
||
|
||
**Ορισμένα κείμενα και παραδείγματα εξάγονται από το [https://ericpony.github.io/z3py-tutorial/guide-examples.htm](https://ericpony.github.io/z3py-tutorial/guide-examples.htm)**
|
||
|
||
# Βασικές Λειτουργίες
|
||
|
||
## Λογικές Τιμές/Και/Ή/Όχι
|
||
```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
|
||
```
|
||
## Ακέραιοι/Απλοποίηση/Πραγματικοί
|
||
|
||
Η βιβλιοθήκη Z3 παρέχει μια πληθώρα εργαλείων για την επίλυση προβλημάτων ικανοποίησης modulo θεωριών (SMT). Μερικά από αυτά τα εργαλεία περιλαμβάνουν τη δυνατότητα επίλυσης προβλημάτων με ακέραιους αριθμούς, απλοποίησης εκφράσεων και επίλυσης προβλημάτων με πραγματικούς αριθμούς.
|
||
|
||
Για την επίλυση προβλημάτων με ακέραιους αριθμούς, μπορούμε να χρησιμοποιήσουμε τη συνάρτηση `Int` της Z3. Αυτή η συνάρτηση μας επιτρέπει να δημιουργήσουμε μεταβλητές ακεραίους και να εκφράσουμε περιορισμούς μεταξύ αυτών των μεταβλητών. Έπειτα, μπορούμε να χρησιμοποιήσουμε τη συνάρτηση `solve` για να επιλύσουμε το πρόβλημα και να βρούμε μια λύση.
|
||
|
||
Για την απλοποίηση εκφράσεων, μπορούμε να χρησιμοποιήσουμε τη συνάρτηση `Simplify` της Z3. Αυτή η συνάρτηση μας επιτρέπει να μετατρέψουμε μια πολύπλοκη έκφραση σε μια απλούστερη μορφή, χωρίς να αλλάζει η σημασία της έκφρασης.
|
||
|
||
Για την επίλυση προβλημάτων με πραγματικούς αριθμούς, μπορούμε να χρησιμοποιήσουμε τη συνάρτηση `Real` της Z3. Αυτή η συνάρτηση μας επιτρέπει να δημιουργήσουμε μεταβλητές πραγματικούς αριθμούς και να εκφράσουμε περιορισμούς μεταξύ αυτών των μεταβλητών. Με τη χρήση της συνάρτησης `solve`, μπορούμε να επιλύσουμε το πρόβλημα και να βρούμε μια λύση.
|
||
```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))
|
||
```
|
||
## Εκτύπωση Μοντέλου
|
||
|
||
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.
|
||
|
||
```python
|
||
print(model)
|
||
```
|
||
|
||
Για να εκτυπώσετε το μοντέλο, μπορείτε να χρησιμοποιήσετε το αντικείμενο `model` που έχετε λάβει από τον επιλύτη. Το αντικείμενο `model` αναπαριστά την ικανοποιητική ανάθεση για τους δεδομένους περιορισμούς.
|
||
|
||
```python
|
||
print(model)
|
||
```
|
||
```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]))
|
||
```
|
||
# Μηχανική Αριθμητική
|
||
|
||
Οι σύγχρονοι επεξεργαστές και οι κύριες γλώσσες προγραμματισμού χρησιμοποιούν αριθμητικές πράξεις πάνω σε **δυαδικούς αριθμούς με σταθερό μέγεθος**. Η μηχανική αριθμητική είναι διαθέσιμη στο Z3Py ως **Bit-Vectors**.
|
||
```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
|
||
```
|
||
## Υπογεγραμμένοι/Ανυπογράμμιστοι Αριθμοί
|
||
|
||
Το Z3 παρέχει ειδικές υπογεγραμμένες εκδόσεις των αριθμητικών λειτουργιών όπου κάνει διαφορά εάν το **bit-vector** θεωρείται ως υπογεγραμμένο ή ανυπογεγραμμένο. Στην Z3Py, οι τελεστές **<, <=, >, >=, /, % και >>** αντιστοιχούν στις **υπογεγραμμένες** εκδόσεις. Οι αντίστοιχοι **ανυπογεγραμμένοι** τελεστές είναι **ULT, ULE, UGT, UGE, UDiv, URem και 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))
|
||
```
|
||
## Συναρτήσεις
|
||
|
||
Οι **ερμηνευμένες συναρτήσεις** όπως η αριθμητική, όπου η **συνάρτηση +** έχει μια **σταθερή τυπική ερμηνεία** (προσθέτει δύο αριθμούς). Οι **μη ερμηνευμένες συναρτήσεις** και σταθερές είναι **μέγιστα ευέλικτες**· επιτρέπουν **οποιαδήποτε ερμηνεία** που είναι **συνεπής** με τους περιορισμούς πάνω στη συνάρτηση ή σταθερά.
|
||
|
||
Παράδειγμα: η εφαρμογή της f δύο φορές στο x έχει ως αποτέλεσμα το x ξανά, αλλά η εφαρμογή της f μία φορά στο x είναι διαφορετική από το 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())
|
||
```
|
||
# Παραδείγματα
|
||
|
||
## Λύτης Sudoku
|
||
|
||
```python
|
||
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. Τέλος, ο κώδικας επιλύει το πρόβλημα και εκτυπώνει τη λύση, αν υπάρχει.
|
||
```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"
|
||
```
|
||
## Αναφορές
|
||
|
||
* [https://ericpony.github.io/z3py-tutorial/guide-examples.htm](https://ericpony.github.io/z3py-tutorial/guide-examples.htm)
|
||
|
||
|
||
<details>
|
||
|
||
<summary><strong>Μάθετε το χάκινγκ του AWS από το μηδέν μέχρι τον ήρωα με το</strong> <a href="https://training.hacktricks.xyz/courses/arte"><strong>htARTE (HackTricks AWS Red Team Expert)</strong></a><strong>!</strong></summary>
|
||
|
||
Άλλοι τρόποι για να υποστηρίξετε το HackTricks:
|
||
|
||
* Εάν θέλετε να δείτε την **εταιρεία σας να διαφημίζεται στο HackTricks** ή να **κατεβάσετε το HackTricks σε μορφή PDF** ελέγξτε τα [**ΠΑΚΕΤΑ ΣΥΝΔΡΟΜΗΣ**](https://github.com/sponsors/carlospolop)!
|
||
* Αποκτήστε το [**επίσημο PEASS & HackTricks swag**](https://peass.creator-spring.com)
|
||
* Ανακαλύψτε [**την Οικογένεια PEASS**](https://opensea.io/collection/the-peass-family), τη συλλογή μας από αποκλειστικά [**NFTs**](https://opensea.io/collection/the-peass-family)
|
||
* **Εγγραφείτε στη** 💬 [**ομάδα Discord**](https://discord.gg/hRep4RUj7f) ή στη [**ομάδα telegram**](https://t.me/peass) ή **ακολουθήστε** μας στο **Twitter** 🐦 [**@carlospolopm**](https://twitter.com/hacktricks_live)**.**
|
||
* **Μοιραστείτε τα χάκινγκ κόλπα σας υποβάλλοντας PRs στα** [**HackTricks**](https://github.com/carlospolop/hacktricks) και [**HackTricks Cloud**](https://github.com/carlospolop/hacktricks-cloud) αποθετήρια του github.
|
||
|
||
</details>
|