Hacknite Wiki

User Tools

Site Tools

Trace: • ret2libc • linux
z3

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
z3 [2025/02/10 12:27] – kresimirz3 [2025/12/01 11:40] (current) – external edit 127.0.0.1
Line 1: Line 1:
 ====Z3 solver==== ====Z3 solver====
  
-Z3 solver je alat napravljen za dokazivanje teorema koji je razvio Microsofta. Open source je i dostupan je pod MIT licencom. Implementiran je u C++ programskom jeziku no ima razrađena sučelja za korištenje s drugim programskim jezicima, kao što su C#, Java, Python, .NET, TypeScript (JavaScript) i drugi. Preporučeni jezik za korištenje radi jednostavnosti je Python. +//Z3 solver// je alat napravljen za dokazivanje teorema, a koji je razvio Microsoft. Open source je i dostupan je pod MIT licencom. Implementiran je u C++ programskom jeziku no ima razrađena sučelja za korištenje s drugim programskim jezicima, kao što su C#, Java, Python, .NET, TypeScript (JavaScript) i drugi. Preporučeni jezik za korištenje radi jednostavnosti je Python. 
-Njegova namjena je da može odrediti je li skup zadanih logičkih pretpostavki zadovoljiv, te u slučaju da je, nalazi rješenje koje zadovoljava definirani skup. Ima mnoge primjene u području računarstva, od kojih su neke: formalna verifikacija softwarea i hardwarea, rješavanje različitih problema optimizacije, rješavanje različitih problema u području geometrije i biologije a ima i zanimljive primjene u području kriptografije i računalne sigurnosti. Z3 koristi SMTLIB2 (Satisfiability Modulo Theories Library) format za definiranje formula, varijabli, ograničenja i upita koje onda procesuira koristeći stog strukturu podataka. Za procesuiranje i rješavanje zadanog modela, Z3 koristi različite napredne metode i tehnike kao što su simboličko izvršavanje, rješavanje SAT problema (Boolean satisfiability problem), korištenje heuristika, paralelizacija, lijena evaluacija (optimizacija izvođenja izračuna), konstruiranje modela i generiranje dokaza i druge. Za više informacija o implementaciji i načinu na koji Z3 funkcionira može se pogledati popis izvora na dnu ovog članka.  +Njegova namjena je da može odrediti je li skup zadanih logičkih pretpostavki zadovoljiv, te u slučaju da je, nalazi rješenje koje zadovoljava definirani skup. Ima mnoge primjene u području računarstva, od kojih su neke: formalna verifikacija softvera i hardvera, rješavanje različitih problema optimizacije, problema u području geometrije i biologije, a ima i zanimljive primjene u području kriptografije i računalne sigurnosti. Z3 koristi SMTLIB2 (Satisfiability Modulo Theories Library) format za definiranje formula, varijabli, ograničenja i upita koje onda obrađuje koristeći strukturu podataka tipa stog. Za obradu i rješavanje zadanog modela, Z3 koristi različite napredne metode i tehnike kao što su simboličko izvršavanje, rješavanje SAT problema (Boolean satisfiability problem), korištenje heuristika, paralelizacija, lijena evaluacija (optimizacija izvođenja izračuna), konstruiranje modela i generiranje dokaza i druge. Za više informacija o implementaciji i načinu na koji Z3 funkcionira može se pogledati popis izvora na dnu ovog članka.  
-Za korištenje Z3 nije potrebno detaljno poznavati teoriju i implementaciju, nego je dovoljno znati slučajeve u kojima je Z3 primjenjiv i kada se može iskoristiti te poznavati neko sučelje za korištenje Z3 solvera, od kojih ima jednostavnih i praktičnih Python implementacija.+Za korištenje Z3 nije potrebno detaljno poznavati teoriju i implementaciju, nego je dovoljno razumjeti u kojima slučajevima je Z3 primjenjiv te poznavati neko sučelje za korištenje //Z3 solvera//, od kojih ima jednostavnih i praktičnih Python implementacija.
  
 ===Python bilioteka za korištenje Z3=== ===Python bilioteka za korištenje Z3===
Line 10: Line 10:
 https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3
 u kojemu su dostupne upute za instalaciju i korištenje, ili se može jednostavno instalirati pip paket u Python okruženje korištenjem naredbe: u kojemu su dostupne upute za instalaciju i korištenje, ili se može jednostavno instalirati pip paket u Python okruženje korištenjem naredbe:
-¸¸+<code>
 pip install z3-solver pip install z3-solver
-¸¸+</code>
 Za korištenje u jednostavnijim slučajevima, preporučen je python pip  paket z3-solver, a za korištenje najnovije verzije, preporučena je instalacija putem gita. Za korištenje u jednostavnijim slučajevima, preporučen je python pip  paket z3-solver, a za korištenje najnovije verzije, preporučena je instalacija putem gita.
-Osnovne upotrebe +===Osnovne upotrebe=== 
-Definicija varijabli +==Definicija varijabli== 
-Nakon stvaranja nove .py datoteke, instalirani pip paket se može koristiti import naredbom: +Nakon stvaranja nove .py datoteke, instalirani pip paket se može koristiti naredbom "import": 
-¸¸+<code>
 from z3 import * from z3 import *
-¸¸+</code>
  
-Za inicijalizaciju objekta solver, kojem će se proslijediti definirane varijable i uvjeti za definiciju i rješavanje problema se koristi naredba: +Za inicijalizaciju objekta "solver", kojem će se proslijediti definirane varijable i uvjeti za definiciju i rješavanje problema se koristi naredba: 
-¸¸+<code>
 solver = Solver() solver = Solver()
-¸¸+</code>
  
 Varijable koje Z3 koristi se inicijaliziraju definiranjem tipa podataka koji sadrže, kao u C-u. npr. za definiranje x varijable koja je integer se koristi naredba: Varijable koje Z3 koristi se inicijaliziraju definiranjem tipa podataka koji sadrže, kao u C-u. npr. za definiranje x varijable koja je integer se koristi naredba:
-¸¸+<code>
 x = Int('x') x = Int('x')
-¸¸+</code>
 Za definiranje s varijable koja je tipa string se koristi naredba: Za definiranje s varijable koja je tipa string se koristi naredba:
-¸¸+<code>
 s = String('s') s = String('s')
-¸¸+</code>
 Za definiranje varijable koja predstavlja jedan bit se koristi naredba: Za definiranje varijable koja predstavlja jedan bit se koristi naredba:
-¸¸+<code>
 bitA = BitVec('bit_var_a', 1) bitA = BitVec('bit_var_a', 1)
-¸¸ +</code> 
-Osim integer, string i bit tipova, Z3 podržava još mnoge druge tipove varijabli, od kojih su neki osnovni: boolean, bajt (izveden kao polje od 8 bitova), realni brojevi, float brojevi i drugi. Od ovih osnovnih tipova se mogu graditi složeniji tipovi, kao enumeracije, n-torke (tuple), skupovi, polja i vektori osnovnih tipova, kao što je bajt izgrađen kao vektor od 8 bitova – „BitVec“, koji se definira naredbom: +Osim tipova integer, string i bit, Z3 podržava još mnoge druge tipove varijabli, od kojih su neki osnovni: boolean, bajt (izveden kao polje od 8 bitova), realni brojevi, float brojevi i drugi. Od ovih osnovnih tipova se mogu graditi složeniji tipovi, kao enumeracije, n-torke (tuple), skupovi, polja i vektori osnovnih tipova, kao što je bajt izgrađen kao vektor od 8 bitova – „BitVec“, koji se definira naredbom: 
-¸¸+<code>
 byte1 = BitVec('byte_var_1', 8) byte1 = BitVec('byte_var_1', 8)
-¸¸+</code> 
 + 
 + 
 +==Definicija ograničenja (uvjeta)==
  
-Iz prethodnih naredbi može se uočiti da jest string argument u inicijalizaciji osnovnih tipova, odnosno prvi argument u inicijalizaciji vektorskih tipova ime varijable koja se definira u kontekstu Z3 rješavatelj objekta. Ova varijabla je proizvoljna i najčešće je istog naziva kao i Python varijabla ili neka izvedenica naziva Python varijable koja se koristi. 
-Drugi argument u naredbi inicijalizacije vektora je dužina vektora, koja je 8 u definiranju bajta kao bit vektora dužine 8. Također mogu se koristiti i druge dužine za definiranje bit vektora. 
-Definicija ograničenja (uvjeta) 
 Nakon što je solver objekt inicijaliziran i varijable su definirane, ograničenja i uvjeti se mogu dodavati naredbom: Nakon što je solver objekt inicijaliziran i varijable su definirane, ograničenja i uvjeti se mogu dodavati naredbom:
-¸¸+<code>
 solver.add(<ograničenje>) solver.add(<ograničenje>)
-¸¸+</code>
 Tako bi se za sljedeći skup  ograničenja nad x i y int varijablama:  Tako bi se za sljedeći skup  ograničenja nad x i y int varijablama: 
 x + y = 106,  x + y = 106, 
Line 58: Line 58:
  y % 7 = 0  y % 7 = 0
 koristile sljedeće naredbe za postavljanje ograničenja modela: koristile sljedeće naredbe za postavljanje ograničenja modela:
-¸¸ +<code> 
-    solver .add(x + y == 106) +    solver.add(x + y == 106) 
-    solver .add(x - y > -111) +    solver.add(x - y > -111) 
-    solver .add(y / x > 10) +    solver.add(y / x > 10) 
-    solver .add(x < 50) +    solver.add(x < 50) 
-    solver .add(y > 19) +    solver.add(y > 19) 
-    solver .add(y % 7 == 0) +    solver.add(y % 7 == 0) 
-¸¸+</code>
 Vidimo da je zapis vrlo jednostavan, samo se mora koristit dupli znak jednakosti za definiranje uvjeta. Vidimo da je zapis vrlo jednostavan, samo se mora koristit dupli znak jednakosti za definiranje uvjeta.
  
-Pokretanje rješavanja definiranog problema+==Pokretanje rješavanja definiranog problema==
  
-Kako bi se pokrenulo rješavanje problema i provjerilo postoji li model koji može zadovoljiti definiranu skup uvjeta, odnosno ima li rješenja problema, koristi se naredba: +Kako bi se pokrenulo rješavanje problema i provjerilo postoji li model koji može zadovoljiti definirani skup uvjeta, odnosno ima li problem rješenje, koristi se naredba: 
-¸¸+<code>
 solver.check() solver.check()
-¸¸+</code>
 Koja vraća vrijednost „sat“ za satisfiable ako ima rješenja ili vrijednost „unsat“ za unsatisfiable ako nema rješenja. Koja vraća vrijednost „sat“ za satisfiable ako ima rješenja ili vrijednost „unsat“ za unsatisfiable ako nema rješenja.
 Ako je problem rješiv, naredba za generiranje modela koji zadovoljava postavljene uvjete je sljedeća: Ako je problem rješiv, naredba za generiranje modela koji zadovoljava postavljene uvjete je sljedeća:
-¸¸+<code>
 model = solver.model() model = solver.model()
-¸¸ +</code> 
-Nakon toga se može napraviti  +Nakon toga se može napraviti: 
-¸¸+<code>
 print(model) print(model)
-¸¸ +</code> 
-Kako bi se vidjelo rješenje, ili se ispis može formatirati i preurediti da bude čitljiviji+Kako bi se vidjelo rješenje, ili se ispis može formatirati i preurediti da bude čitljiviji.
 Ovaj dio programa se može jednostavno ostvariti sljedećim kodom: Ovaj dio programa se može jednostavno ostvariti sljedećim kodom:
-¸¸+<code>
  
     if solver.check() == sat:     if solver.check() == sat:
Line 94: Line 94:
     else:     else:
         print("Nema rješenja")         print("Nema rješenja")
-¸¸+</code>
  
 Za pokretanje izvršavanja prethodno definiranog skupa uvjeta s varijablama X i Y, Z3 će uspješno pronaći rješenje x =  1, y =  105. Za pokretanje izvršavanja prethodno definiranog skupa uvjeta s varijablama X i Y, Z3 će uspješno pronaći rješenje x =  1, y =  105.
  
-No definirani problem često može sadržavati više rješenja. Jednostavan pristup kako pronaći sva rješenja pojedinog problema je da se u while petlji nakon pronalaska jednog rješenja, doda novi uvjet koji definira da X i Y ne smiju biti vrijednosti pronađene u prethodnom rješenju i da se ponovno pokrene postupak pronalaska rješenja, sve dok se ne dođe do slučaja da se više rješenje ne može pronaći.+No definirani problem često može sadržavati više rješenja. Jednostavan pristup kako pronaći sva rješenja pojedinog problema je da se u while petlji nakon pronalaska jednog rješenja, doda novi uvjet koji definira da X i Y ne smiju biti vrijednosti pronađene u prethodnom rješenju i da se ponovno pokrene postupak pronalaska rješenja, sve dok se ne dođe do slučaja da se rješenje više ne može pronaći.
 Ova programska logika se može ostvariti sljedećim kodom: Ova programska logika se može ostvariti sljedećim kodom:
-¸¸+<code>
     while solver.check()  == sat:     while solver.check()  == sat:
         model = solver.model()         model = solver.model()
         print("Rješenje: x = ", model[x], "y = ", model[y])         print("Rješenje: x = ", model[x], "y = ", model[y])
         solver.add(Or(x != solver.model()[x], y != solver.model()[y]))         solver.add(Or(x != solver.model()[x], y != solver.model()[y]))
-¸¸ +</code> 
-Pokretanjem ovog koda za prethodno definirani problem, Z3 osim rješenja x =  1, y =  105 pronalazi i drugo rješenje x = 8, y = 98.+Pokretanjem ovog koda za prethodno definirani problem, Z3 osim rješenja x =  1, y =  105 pronalazi i drugo rješenje: x = 8, y = 98.
  
-===PRIMJER -Zadatak s Hacknite platforme –  ZZZ===+===PRIMJER - Zadatak s Hacknite platforme –  ZZZ===
  
 <file> <file>
Line 115: Line 115:
 </file> </file>
 Uz zadatak dostupna je i datoteka python_checker.py. Uz zadatak dostupna je i datoteka python_checker.py.
-Ime zadatka „ZZZ“ je hint na Z3. +Ime zadatka „ZZZ“ je hint na Z3 solver. 
-Kod zadatka uz formatiranje uvjeta radi bolje čitljivosti je prikazan na slici 1.+Kôd zadatka, uz formatiranje uvjeta radi bolje čitljivosti, je prikazan na slici 1.
  
 {{z3solver:slika1.png}} {{z3solver:slika1.png}}
  
-Pregledom koda zadatka može se vidjeti da je definiran velik skup uvjeta znamenki varijable flag koji moraju biti zadovoljeni da bi program ispisao rješenje. Od uvjeta, prvi uvjet provjerava početak sha256 hash vrijednosti 3., 9., 10. i 11. ascii vrijednosti znamenke flaga. Ostali uvjeti definiraju različite relacije i uvjete znamenki flaga. Može se uočiti da su u relacijama ostalih uvjeta upotrijebljene sve znamenke flag-a od 0. do 11. znamenke.  +Pregledom kôda zadatka može se vidjeti da je definiran velik skup uvjeta znamenki varijable "flag" koji moraju biti zadovoljeni da bi program ispisao rješenje. Od uvjeta, prvi uvjet provjerava početak sha256 hash vrijednosti 3., 9., 10. i 11. ascii vrijednosti znamenke flaga. Ostali uvjeti definiraju različite relacije i uvjete znamenki flaga. Može se uočiti da su u relacijama ostalih uvjeta upotrijebljene sve znamenke flag-a od 0. do 11. znamenke.  
-Uz pretpostavku da skup svih uvjeta bez prvog uvjeta koji provjerava sha256 hash ima dovoljno mali skup rješenja, da se prvo mogu pronaći sva rješenja za ostale uvjete, a nakon toga se nad pronađenim rješenjima mogu generirati sha256 sažetci odgovarajućih znamenki rješenja i naknadno provjerit prvi uvjet.  +Uz pretpostavku da skup svih uvjeta bez prvog uvjeta koji provjerava sha256 hash ima dovoljno mali skup rješenja, da se prvo mogu pronaći sva rješenja za ostale uvjete, a nakon toga se nad pronađenim rješenjima mogu generirati sha256 sažetci odgovarajućih znamenki rješenja i naknadno provjeriti prvi uvjet.  
-Programski kod za inicijalizaciju Z3 solvera i definiciju skupa uvjeta problema bez prvog uvjeta provjere hash-a prikazan je na slici 2.+Programski kôd za inicijalizaciju //Z3 solvera// i definiciju skupa uvjeta problema, bez prvog uvjeta provjere hash-a, prikazan je na slici 2.
  
 {{z3solver:slika2.png}} {{z3solver:slika2.png}}
z3.1739190457.txt.gz · Last modified: 2025/12/01 11:40 (external edit)
Donate Powered by PHP Valid HTML5 Valid CSS Driven by DokuWiki