Hacknite Wiki

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

Z3 se može instalirati i namjestiti korištenjem „službenog“ git repozitorija projekta: 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:

pip install z3-solver

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.

Nakon stvaranja nove .py datoteke, instalirani pip paket se može koristiti naredbom “import”:

from z3 import *

Za inicijalizaciju objekta “solver”, kojem će se proslijediti definirane varijable i uvjeti za definiciju i rješavanje problema se koristi naredba:

solver = Solver()

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:

x = Int('x')

Za definiranje s varijable koja je tipa string se koristi naredba:

s = String('s')

Za definiranje varijable koja predstavlja jedan bit se koristi naredba:

bitA = BitVec('bit_var_a', 1)

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:

byte1 = BitVec('byte_var_1', 8)

Nakon što je solver objekt inicijaliziran i varijable su definirane, ograničenja i uvjeti se mogu dodavati naredbom:

solver.add(<ograničenje>)

Tako bi se za sljedeći skup ograničenja nad x i y int varijablama: x + y = 106, x - y > -111, y / x > 10, x < 50, y > 19, y % 7 = 0 koristile sljedeće naredbe za postavljanje ograničenja modela:

    solver.add(x + y == 106)
    solver.add(x - y > -111)
    solver.add(y / x > 10)
    solver.add(x < 50)
    solver.add(y > 19)
    solver.add(y % 7 == 0)

Vidimo da je zapis vrlo jednostavan, samo se mora koristit dupli znak jednakosti za definiranje uvjeta.

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:

solver.check()

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:

model = solver.model()

Nakon toga se može napraviti:

print(model)

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:

    if solver.check() == sat:

        model = solver.model()
        print("Rješenje: x = ", model[x], "y = ", model[y])

    else:
        print("Nema rješenja")

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 rješenje više ne može pronaći. Ova programska logika se može ostvariti sljedećim kodom:

    while solver.check()  == sat:
        model = solver.model()
        print("Rješenje: x = ", model[x], "y = ", model[y])
        solver.add(Or(x != solver.model()[x], y != solver.model()[y]))

Pokretanjem ovog koda za prethodno definirani problem, Z3 osim rješenja x = 1, y = 105 pronalazi i drugo rješenje: x = 8, y = 98.

Spava mi se od ovog zadatka
 python_checker.py

Uz zadatak dostupna je i datoteka python_checker.py. Ime zadatka „ZZZ“ je hint na Z3 solver. Kôd zadatka, uz formatiranje uvjeta radi bolje čitljivosti, je prikazan na slici 1.

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 provjeriti prvi uvjet. Programski kôd za inicijalizaciju Z3 solvera i definiciju skupa uvjeta problema, bez prvog uvjeta provjere hash-a, prikazan je na slici 2.

Sada je potrebno dodati programsku logiku za pronalazak svih rješenja koja zadovoljavaju ovaj skup uvjeta. Ova programska logika je prikazana na slici 3.

Pokretanjem ovog programa, Z3 pronalazi 3 rješenja koja zadovoljavaju definirani skup uvjeta. Pronađena rješenja su prikazana na slici 4.

** dio znamenki rješenja je skriven, pronađite ih sami

Analizom triju pronađenih rješenja može se uočiti da su 3., 9., 10. i 11. znamenka iste u svim rješenjima, što znači da bi uvjet sa sha256 hashem nad spomenutim znamenkama za sva 3 rješenja bio isti. Također, provjerom hash uvjeta nad rješenjima, može se vidjeti da sva rješenja zadovoljavaju uvjet. Kako bi se uspješno riješio zadatak, trebaju se samo probati unijeti sve tri vrijednosti flag-a od kojih je jedno ispravno rješenje.

Teorija:
https://microsoft.github.io/z3guide/
https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/
https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
https://en.wikipedia.org/wiki/Symbolic_execution
https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
Korištenje:
https://github.com/Z3Prover/z3
https://aldosari.medium.com/a-step-by-step-guide-to-harnessing-the-power-of-z3-solver-a96c4aa1b619
https://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/guide-examples.htm