mirror of
https://github.com/carlospolop/hacktricks
synced 2024-12-25 20:43:29 +00:00
201 lines
7.4 KiB
Markdown
201 lines
7.4 KiB
Markdown
|
<details>
|
||
|
|
|
||
|
|
<summary><strong>Aprenda hacking AWS do zero ao herói com</strong> <a href="https://training.hacktricks.xyz/courses/arte"><strong>htARTE (HackTricks AWS Red Team Expert)</strong></a><strong>!</strong></summary>
|
||
|
|
|
||
|
|
Outras maneiras de apoiar o HackTricks:
|
||
|
|
|
||
|
|
* Se você deseja ver sua **empresa anunciada no HackTricks** ou **baixar o HackTricks em PDF** Confira os [**PLANOS DE ASSINATURA**](https://github.com/sponsors/carlospolop)!
|
||
|
|
* Adquira o [**swag oficial PEASS & HackTricks**](https://peass.creator-spring.com)
|
||
|
|
* Descubra [**A Família PEASS**](https://opensea.io/collection/the-peass-family), nossa coleção exclusiva de [**NFTs**](https://opensea.io/collection/the-peass-family)
|
||
|
|
* **Junte-se ao** 💬 [**grupo Discord**](https://discord.gg/hRep4RUj7f) ou ao [**grupo telegram**](https://t.me/peass) ou **siga-nos** no **Twitter** 🐦 [**@carlospolopm**](https://twitter.com/hacktricks_live)**.**
|
||
|
|
* **Compartilhe seus truques de hacking enviando PRs para os** [**HackTricks**](https://github.com/carlospolop/hacktricks) e [**HackTricks Cloud**](https://github.com/carlospolop/hacktricks-cloud) repositórios do github.
|
||
|
|
|
||
|
|
</details>
|
||
|
|
|
||
|
|
|
||
|
|
Muito basicamente, esta ferramenta nos ajudará a encontrar valores para variáveis que precisam satisfazer algumas condições e calculá-los manualmente será muito irritante. Portanto, você pode indicar ao Z3 as condições que as variáveis precisam satisfazer e ele encontrará alguns valores (se possível).
|
||
|
|
|
||
|
|
**Alguns textos e exemplos são extraídos de [https://ericpony.github.io/z3py-tutorial/guide-examples.htm](https://ericpony.github.io/z3py-tutorial/guide-examples.htm)**
|
||
|
|
|
||
|
|
# Operações Básicas
|
||
|
|
|
||
|
|
## Booleanos/E/OU/Não
|
||
|
|
```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
|
||
|
|
```
|
||
|
|
## Inteiros/Simplificar/Reais
|
||
|
|
```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))
|
||
|
|
```
|
||
|
|
## Imprimindo Modelo
|
||
|
|
```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]))
|
||
|
|
```
|
||
|
|
# Aritmética de Máquina
|
||
|
|
|
||
|
|
As CPUs modernas e linguagens de programação mainstream utilizam aritmética sobre **vetores de bits de tamanho fixo**. A aritmética de máquina está disponível no Z3Py como **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
|
||
|
|
```
|
||
|
|
## Números assinados/não assinados
|
||
|
|
|
||
|
|
O Z3 fornece versões especiais assinadas de operações aritméticas onde faz diferença se o **vetor de bits é tratado como assinado ou não assinado**. No Z3Py, os operadores **<, <=, >, >=, /, % e >>** correspondem às versões **assinadas**. Os operadores **não assinados** correspondentes são **ULT, ULE, UGT, UGE, UDiv, URem e 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))
|
||
|
|
```
|
||
|
|
## Funções
|
||
|
|
|
||
|
|
**Funções interpretadas** como aritmética, onde a **função +** tem uma **interpretação padrão fixa** (soma dois números). **Funções não interpretadas** e constantes são **maximamente flexíveis**; elas permitem **qualquer interpretação** que seja **consistente** com as **restrições** sobre a função ou constante.
|
||
|
|
|
||
|
|
Exemplo: f aplicado duas vezes a x resulta em x novamente, mas f aplicado uma vez a x é diferente de 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())
|
||
|
|
```
|
||
|
|
# Exemplos
|
||
|
|
|
||
|
|
## Solucionador de 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"
|
||
|
|
```
|
||
|
|
## Referências
|
||
|
|
|
||
|
|
* [https://ericpony.github.io/z3py-tutorial/guide-examples.htm](https://ericpony.github.io/z3py-tutorial/guide-examples.htm)
|
||
|
|
|
||
|
|
|
||
|
|
<details>
|
||
|
|
|
||
|
|
<summary><strong>Aprenda hacking AWS do zero ao herói com</strong> <a href="https://training.hacktricks.xyz/courses/arte"><strong>htARTE (HackTricks AWS Red Team Expert)</strong></a><strong>!</strong></summary>
|
||
|
|
|
||
|
|
Outras maneiras de apoiar o HackTricks:
|
||
|
|
|
||
|
|
* Se você deseja ver sua **empresa anunciada no HackTricks** ou **baixar o HackTricks em PDF** Verifique os [**PLANOS DE ASSINATURA**](https://github.com/sponsors/carlospolop)!
|
||
|
|
* Adquira o [**swag oficial PEASS & HackTricks**](https://peass.creator-spring.com)
|
||
|
|
* Descubra [**A Família PEASS**](https://opensea.io/collection/the-peass-family), nossa coleção exclusiva de [**NFTs**](https://opensea.io/collection/the-peass-family)
|
||
|
|
* **Junte-se ao** 💬 [**grupo Discord**](https://discord.gg/hRep4RUj7f) ou ao [**grupo telegram**](https://t.me/peass) ou **siga-nos** no **Twitter** 🐦 [**@carlospolopm**](https://twitter.com/hacktricks_live)**.**
|
||
|
|
* **Compartilhe seus truques de hacking enviando PRs para os** [**HackTricks**](https://github.com/carlospolop/hacktricks) e [**HackTricks Cloud**](https://github.com/carlospolop/hacktricks-cloud) repositórios do github.
|
||
|
|
|
||
|
|
</details>
|