Z3 - Satisfiability Modulo Theories (SMT)

reversing z3

Z3, reverse’ten çıkardığın denklemleri çözer. Angr otomatik path bulurken Z3 elle yazılmış checker mantığını doğrudan modeler.

Metodoloji

1. Checker’ı Ghidra’dan denklemlere dök.

2. BitVec değişkenleri ve kısıtları ekle.

3. check()==sat ise model’den flag’i oku.

4. Native binary ile doğrula.

Kurulum

pip install z3-solver

from z3 import *
print(Simplify(Int('x')+0))

Basit crackme

from z3 import *
flag=[BitVec(f'c{i}',8) for i in range(8)]
s=Solver()
for c in flag:
    s.add(c>=0x20,c<=0x7e)
s.add(flag[0]==ord('F'))
s.add(flag[1]^0x13==ord('l'))
s.add((flag[2]+flag[3])==0xA0)
s.add(flag[7]==ord('}'))
assert s.check()==sat
m=s.model()
print(bytes(m[c].as_long() for c in flag))

Bit ops

from z3 import *
x=BitVec('x',32)
s=Solver(); s.add(RotateLeft(x,5)^0xdeadbeef==0x12345678)
print(s.check(), s.model())

from z3 import *
# array / memory benzeri
A=Array('A',BitVecSort(8),BitVecSort(8))
s=Solver(); s.add(Select(A,0)==ord('A')); print(s.check())

angr + z3

# angr claripy zaten z3 backend kullanır
# elle ek kısıt:
state.solver.add(flag_bv[0]==ord('f'))

Checklist

[ ] denklemler doğru aktarıldı
[ ] printable bound eklendi
[ ] sat model üretildi
[ ] native verify geçti