Hacknite Wiki

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

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. Osnovne upotrebe Definicija varijabli Nakon stvaranja nove .py datoteke, instalirani pip paket se može koristiti import naredbom: ¸¸ 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 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: ¸¸ byte1 = BitVec('byte_var_1', 8) ¸¸

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

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: ¸¸ 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 više rješenje 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. Kod zadatka uz formatiranje uvjeta radi bolje čitljivosti je prikazan na slici 1.

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