Satisfiability Modulo Theories (SMT) - Z3

Tip

AWS Hacking’i öğrenin ve pratik yapın:HackTricks Training AWS Red Team Expert (ARTE)
GCP Hacking’i öğrenin ve pratik yapın: HackTricks Training GCP Red Team Expert (GRTE) Azure Hacking’i öğrenin ve pratik yapın: HackTricks Training Azure Red Team Expert (AzRTE)

HackTricks'i Destekleyin

• abonelik planlarını kontrol edin!
• 💬 Discord grubuna veya telegram grubuna katılın ya da Twitter’da bizi takip edin 🐦 @hacktricks_live.**
• Hacking ipuçlarını paylaşmak için HackTricks ve HackTricks Cloud github reposuna PR gönderin.

Çok temel düzeyde, bu araç belirli koşulları sağlaması gereken değişkenler için değerler bulmamıza yardımcı olur; bunları elle hesaplamak çok zahmetli olur. Bu nedenle Z3’e değişkenlerin sağlaması gereken koşulları belirtirseniz, mümkünse bazı değerler bulacaktır.

Bazı metinler ve örnekler https://ericpony.github.io/z3py-tutorial/guide-examples.htm sitesinden alınmıştır

Temel İşlemler

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))

Printing 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]))

Makine Aritmetiği

Modern işlemciler ve yaygın programlama dilleri, fixed-size bit-vectors üzerinde aritmetik kullanır. Makine aritmetiği Z3Py’de Bit-Vectors olarak mevcuttur.

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

İşaretli/İşaretsiz Sayılar

Z3, bit vektörünün işaretli mi yoksa işaretsiz mi olarak değerlendirildiğinin fark yarattığı durumlarda aritmetik işlemlerin özel işaretli sürümlerini sağlar. Z3Py’de operatörler <, <=, >, >=, /, % ve >> işaretli sürümlere karşılık gelir. Buna karşılık gelen işaretsiz operatörler ULT, ULE, UGT, UGE, UDiv, URem ve 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))

Tersine mühendislikte sıkça ihtiyaç duyulan bit-vektör yardımcıları

assembly veya decompiler çıktısından kontrolleri çıkarırken, genellikle her giriş baytını BitVec(..., 8) olarak modellemek ve sonra kelimeleri hedef kodun yaptığı gibi tam olarak yeniden oluşturmak daha iyidir. Bu, matematiksel tamsayıları makine aritmetiği ile karıştırmaktan kaynaklanan hataları önler.

from z3 import *

b0, b1, b2, b3 = BitVecs('b0 b1 b2 b3', 8)
eax = Concat(b3, b2, b1, b0)        # little-endian bytes -> 32-bit register value
low_byte = Extract(7, 0, eax)        # AL
high_word = Extract(31, 16, eax)     # upper 16 bits
signed_b0 = SignExt(24, b0)          # movsx eax, byte ptr [...]
unsigned_b0 = ZeroExt(24, b0)        # movzx eax, byte ptr [...]
rot = RotateLeft(eax, 13)            # rol eax, 13
logical = LShR(eax, 3)               # shr eax, 3
arith = eax >> 3                     # sar eax, 3 (signed shift)

Bazı yaygın tuzaklar, kodu kısıtlamalara çevirirken:

• >> bit vektörleri (bit-vectors) için bir aritmetik sağa kaydırmadır. Mantıksal shr talimatı için LShR kullanın.
• Orijinal karşılaştırma/bölme işaretsiz ise UDiv, URem, ULT, ULE, UGT ve UGE kullanın.
• Genişlikleri açık tutun. Binary 8 veya 16 bite kırpılıyorsa, her şeyi sessizce Python integerlarına yükseltmek yerine Extract ekleyin veya değeri Concat ile yeniden oluşturun.

Fonksiyonlar

Yorumlanmış fonksiyonlar aritmetik gibi, function +’nın sabit standart yorumu olduğu durumlarda (iki sayıyı toplar). Yorumlanmamış fonksiyonlar ve sabitler mümkün olduğunca esnektir; fonksiyon veya sabit üzerindeki kısıtlarla uyumlu olan herhangi bir yoruma izin verirler.

Örnek: f’in x’e iki kez uygulanması sonucunda tekrar x elde edilir, fakat f’in x’e bir kez uygulanması x’ten farklıdır.

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())

Örnekler

Sudoku çözücü

# 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"

Reversing iş akışları

Eğer ikiliyi sembolik olarak yürütmeniz ve kısıtlamaları otomatik olarak toplamanız gerekiyorsa, angr notlarına buradan bakın:

Angr

Zaten decompiled kontrollerine bakıyor ve sadece bunları çözmeniz gerekiyorsa, raw Z3 genellikle daha hızlıdır ve kontrol etmesi daha kolaydır.

crackme’den byte-based kontrolleri yükseltme

crackme’lerde ve packed loader’larda çok yaygın bir örüntü, aday parola üzerinde uzun bir byte denklemleri listesidir. Byte’ları 8-bit vectors olarak modelleyin, alfabeti kısıtlayın ve yalnızca orijinal kod bunları genişlettiğinde genişletin.

</details>

#### Artımlı çözümleme `push()` / `pop()` ile

Bu yaklaşım gerçek dünyadaki reversing ile iyi örtüşür çünkü modern writeups'ların pratikte yaptığına uyar: aritmetik/bit düzeyindeki ilişkileri ortaya çıkarmak, her karşılaştırmayı bir kısıta dönüştürmek ve tüm sistemi aynı anda çözmek.

Reversing sırasında genellikle tüm solver'ı yeniden oluşturmak zorunda kalmadan birden fazla hipotezi test etmek istersiniz. `push()` bir checkpoint oluşturur ve `pop()` o checkpoint'ten sonra eklenen kısıtları atar. Bu, bir branch'in signed mı yoksa unsigned mı olduğu, bir register'ın zero-extended mı yoksa sign-extended mı olduğu konusunda emin olmadığınızda veya disassembly'den çıkarılan birkaç aday sabiti denerken faydalıdır.
```python
from z3 import *

x = BitVec('x', 32)
s = Solver()
s.add((x & 0xff) == 0x41)

s.push()
s.add(UGT(x, 0x1000))
print(s.check())
s.pop()

s.push()
s.add(x == 0x41)
print(s.check())
print(s.model())
s.pop()

from z3 import *

xs = [BitVec(f'x{i}', 8) for i in range(4)]
s = Solver()
for x in xs:
s.add(And(x >= 0x30, x <= 0x39))
s.add(xs[0] + xs[1] == xs[2] + 1)
s.add(xs[3] == xs[0] ^ 3)

while s.check() == sat:
m = s.model()
print(''.join(chr(m[x].as_long()) for x in xs))
s.add(Or([x != m.eval(x, model_completion=True) for x in xs]))

from z3 import *

t = Then('simplify', 'solve-eqs', 'bit-blast', 'sat')
s = t.solver()