Po mom mišljenju, u sektoru interneta na ruskom jeziku tema formalne verifikacije nije dovoljno obrađena, a posebno nedostaju jednostavni i jasni primjeri.
Navest ću primjer iz stranog izvora i dodati svoje rješenje poznatom problemu prelaska vuka, koze i kupusa na drugu stranu rijeke.
Ali prvo ću ukratko opisati šta je formalna verifikacija i zašto je potrebna.
Formalna verifikacija obično znači provjeru jednog programa ili algoritma korištenjem drugog.
Ovo je neophodno kako bi se osiguralo da se program ponaša kako se očekuje i da bi se osigurala njegova sigurnost.
Formalna verifikacija je najmoćnije sredstvo za pronalaženje i eliminisanje ranjivosti: omogućava vam da pronađete sve postojeće rupe i greške u programu ili da dokažete da ne postoje.
Vrijedi napomenuti da je u nekim slučajevima to nemoguće, kao na primjer u problemu 8 dama sa širinom ploče od 1000 polja: sve se svodi na algoritamsku složenost ili problem zaustavljanja.
Međutim, u svakom slučaju će se dobiti jedan od tri odgovora: program je tačan, netačan ili nije bilo moguće izračunati odgovor.
Ako je nemoguće pronaći odgovor, često je moguće preraditi nejasne dijelove programa, smanjujući njihovu algoritamsku složenost, kako bi se dobio konkretan odgovor da ili ne.
I formalna verifikacija se koristi, na primjer, u Windows kernelu i operativnim sistemima Darpa drone, kako bi se osigurala maksimalna razina zaštite.
Koristit ćemo Z3Prover, vrlo moćan alat za automatizirano dokazivanje teorema i rješavanje jednačina.
Štoviše, Z3 rješava jednadžbe, a ne bira njihove vrijednosti grubom silom.
To znači da je u stanju pronaći odgovor, čak iu slučajevima kada postoji 10^100 kombinacija ulaznih opcija.
Ali ovo je samo desetak ulaznih argumenata tipa Integer, i to se često susreće u praksi.
Problem o 8 kraljica (preuzeto sa engleskog ).
# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]
# Each queen is in a column {1, ... 8 }
val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]
# At most one queen per column
col_c = [ Distinct(Q) ]
# Diagonal constraint
diag_c = [ If(i == j,
True,
And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
for i in range(8) for j in range(i) ]
solve(val_c + col_c + diag_c)
Pokretanjem Z3 dobijamo rješenje:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Problem s kraljicom je uporediv s programom koji uzima kao ulaz koordinate 8 dama i daje odgovor da li su dame pobijedile jedna drugu.
Ako bismo takav program riješili koristeći formalnu verifikaciju, onda bi u poređenju s problemom jednostavno morali napraviti još jedan korak u obliku pretvaranja programskog koda u jednadžbu: pokazalo bi se da je u suštini identičan našem ( naravno, ako je program ispravno napisan).
Gotovo ista stvar će se dogoditi u slučaju traženja ranjivosti: samo postavljamo izlazne uvjete koji su nam potrebni, na primjer, administratorsku lozinku, transformiramo izvorni ili dekompilirani kod u jednadžbe kompatibilne s verifikacijom, a zatim dobijamo odgovor šta podaci se moraju dostaviti kao ulaz da bi se postigao cilj.
Po mom mišljenju, problem o vuku, kozi i kupusu je još zanimljiviji, jer je za njegovo rješavanje potrebno mnogo (7) koraka.
Ako je problem matice uporediv sa slučajem kada možete prodreti na server pomoću jednog GET ili POST zahtjeva, onda vuk, koza i kupus pokazuju primjer iz mnogo složenije i raširenije kategorije, u kojoj se cilj može postići samo po nekoliko zahteva.
Ovo je uporedivo, na primjer, sa scenarijem u kojem trebate pronaći SQL injekciju, napisati datoteku kroz nju, zatim podići svoja prava i tek onda dobiti lozinku.
Uslovi problema i njegovo rješenjeSeljak treba da preveze vuka, kozu i kupus preko reke. Farmer ima čamac koji može primiti samo jedan objekt, osim samog farmera. Vuk će pojesti kozu, a koza kupus ako ih farmer ostavi bez nadzora.
Rješenje je da će u koraku 4 farmer morati vratiti kozu.
Sada krenimo s programskim rješavanjem.
Označimo seljaka, vuka, koze i kupusa kao 4 varijable koje imaju vrijednost samo 0 ili 1. Nula znači da su na lijevoj obali, a jedan znači da su na desnoj.
import json
from z3 import *
s = Solver()
Num= 8
Human = [ Int('Human_%i' % (i + 1)) for i in range(Num) ]
Wolf = [ Int('Wolf_%i' % (i + 1)) for i in range(Num) ]
Goat = [ Int('Goat_%i' % (i + 1)) for i in range(Num) ]
Cabbage = [ Int('Cabbage_%i' % (i + 1)) for i in range(Num) ]
# Each creature can be only on left (0) or right side (1) on every state
HumanSide = [ Or(Human[i] == 0, Human[i] == 1) for i in range(Num) ]
WolfSide = [ Or(Wolf[i] == 0, Wolf[i] == 1) for i in range(Num) ]
GoatSide = [ Or(Goat[i] == 0, Goat[i] == 1) for i in range(Num) ]
CabbageSide = [ Or(Cabbage[i] == 0, Cabbage[i] == 1) for i in range(Num) ]
Side = HumanSide+WolfSide+GoatSide+CabbageSide
Num je broj koraka potrebnih za rješavanje. Svaki korak predstavlja stanje rijeke, čamca i svih entiteta.
Za sada, izaberimo ga nasumično i sa marginom, uzmimo 10.
Svaki entitet je predstavljen u 10 kopija - ovo je njegova vrijednost u svakom od 10 koraka.
Sada postavimo uslove za početak i cilj.
Start = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ]
Finish = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]
Zatim postavljamo uslove u kojima vuk jede kozu, ili koza jede kupus, kao ograničenja u jednačini.
(U prisustvu farmera agresija je nemoguća)
# Wolf cant stand with goat, and goat with cabbage without human. Not 2, not 0 which means that they are one the same side
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
I na kraju ćemo definisati sve moguće radnje farmera pri prelasku tamo ili nazad.
Može ili da povede sa sobom vuka, kozu ili kupus, ili da ne vodi nikoga, ili da ne plovi nigde.
Naravno, niko ne može preći bez farmera.
To će biti izraženo činjenicom da se svako naredno stanje rijeke, čamca i entiteta može razlikovati od prethodnog samo na strogo ograničen način.
Ne više od 2 bita, i sa mnogim drugim ograničenjima, budući da farmer može transportovati samo jedan po jedan entitet i ne mogu svi biti ostavljeni zajedno.
Travel = [ Or(
And(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
And(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
And(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) for i in range(Num-1) ]
Pokrenimo rješenje.
solve(Side + Start + Finish + Safe + Travel)
I dobijamo odgovor!
Z3 je pronašao konzistentan skup stanja koji zadovoljava sve uslove.
Neka vrsta četvorodimenzionalnog odlivanja prostor-vremena.
Hajde da shvatimo šta se desilo.
Vidimo da su na kraju svi prešli, samo je naš farmer isprva odlučio da se odmori, a u prva 2 koraka ne pliva nigdje.
Human_2 = 0
Human_3 = 0
To sugerira da je broj država koje smo odabrali prevelik, a 8 će biti sasvim dovoljno.
U našem slučaju, farmer je uradio ovo: počni, odmori se, odmori se, pređi kozu, pređi nazad, ukrsti kupus, vrati se sa kozom, pređe vuka, vrati se sam, ponovo isporuči kozu.
Ali na kraju je problem rešen.
#Старт.
Human_1 = 0
Wolf_1 = 0
Goat_1 = 0
Cabbage_1 = 0
#Фермер отдыхает.
Human_2 = 0
Wolf_2 = 0
Goat_2 = 0
Cabbage_2 = 0
#Фермер отдыхает.
Human_3 = 0
Wolf_3 = 0
Goat_3 = 0
Cabbage_3 = 0
#Фермер отвозит козу на нужный берег.
Human_4 = 1
Wolf_4 = 0
Goat_4 = 1
Cabbage_4 = 0
#Фермер возвращается.
Human_5 = 0
Wolf_5 = 0
Goat_5 = 1
Cabbage_5 = 0
#Фермер отвозит капусту на нужный берег.
Human_6 = 1
Wolf_6 = 0
Cabbage_6 = 1
Goat_6 = 1
#Ключевая часть операции: фермер возвращает козу обратно.
Human_7 = 0
Wolf_7 = 0
Goat_7 = 0
Cabbage_7 = 1
#Фермер отвозит волка на другой берег, где он теперь находится вместе с капустой.
Human_8 = 1
Wolf_8 = 1
Goat_8 = 0
Cabbage_8 = 1
#Фермер возвращается за козой.
Human_9 = 0
Wolf_9 = 1
Goat_9 = 0
Cabbage_9 = 1
#Фермер повторно доставляет козу на нужный берег и завершают переправу.
Human_10 = 1
Wolf_10 = 1
Goat_10 = 1
Cabbage_10 = 1
Pokušajmo sada promijeniti uslove i dokazati da rješenja nema.
Da bismo to učinili, dat ćemo našem vuku biljojedi, a on će htjeti jesti kupus.
Ovo se može usporediti sa slučajem u kojem nam je cilj osigurati aplikaciju i moramo se pobrinuti da nema rupa.
Safe = [ And( Or(Wolf[i] != Goat[i], Wolf[i] == Human[i]), Or(Goat[i] != Cabbage[i], Goat[i] == Human[i]), Or(Wolf[i] != Cabbage[i], Goat[i] == Human[i])) for i in range(Num) ]
Z3 nam je dao sljedeći odgovor:
no solution
To znači da zaista nema rješenja.
Tako smo programski dokazali nemogućnost križanja sa vukom svejedom bez gubitaka za farmera.
Ako publici ova tema bude zanimljiva, u budućim člancima ću vam reći kako pretvoriti običan program ili funkciju u jednadžbu kompatibilnu s formalnim metodama i riješiti je, otkrivajući tako sve legitimne scenarije i ranjivosti. Prvo na istom zadatku, ali predstavljenom u formi programa, a zatim ga postepeno komplikuje i prelazi na aktuelne primere iz sveta razvoja softvera.
Sljedeći članak je već spreman:
U njemu prelazim sa formalne verifikacije problema na programe i opisujem ih
kako ih možete automatski pretvoriti u sisteme formalnih pravila.
izvor: www.habr.com