Po mom mišljenju, u sektoru interneta na ruskom jeziku tema formalne provjere nije dovoljno pokrivena, a posebno nedostaje jednostavnih i jasnih primjera.
Navest ću primjer iz stranog izvora, te dodati svoje rješenje poznatog problema prelaska vuka, koze i kupusa na drugu stranu rijeke.
Ali prvo ću ukratko opisati što je formalna verifikacija i zašto je potrebna.
Formalna verifikacija obično znači provjeru jednog programa ili algoritma pomoću drugog.
Ovo je neophodno kako bi se osiguralo da se program ponaša prema očekivanjima i da bi se osigurala njegova sigurnost.
Formalna provjera najmoćnije je sredstvo pronalaženja i uklanjanja ranjivosti: omogućuje vam da pronađete sve postojeće rupe i greške u programu ili dokažete da ne postoje.
Vrijedno je napomenuti da je u nekim slučajevima to nemoguće, kao 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, dobit će se jedan od tri odgovora: program je točan, netoč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.
Formalna provjera koristi se, na primjer, u Windows kernelu i operativnim sustavima Darpa drone, kako bi se osigurala maksimalna razina zaštite.
Koristit ćemo Z3Prover, vrlo moćan alat za automatizirano dokazivanje teorema i rješavanje jednadžbi.
Štoviše, Z3 rješava jednadžbe, a ne odabire njihove vrijednosti korištenjem grube sile.
To znači da je u stanju pronaći odgovor, čak iu slučajevima kada postoji 10^100 kombinacija opcija unosa.
Ali ovo je samo oko desetak ulaznih argumenata tipa Integer, a ovo se često susreće u praksi.
Problem o 8 kraljica (preuzeto s 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)
Pokrećući Z3, dobivamo 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 usporediv je s programom koji kao ulaz uzima koordinate 8 kraljica i daje odgovor da li su kraljice pobijedile jedna drugu.
Kad bismo takav program riješili formalnom verifikacijom, tada bismo u usporedbi s problemom jednostavno morali poduzeti još jedan korak u obliku pretvaranja programskog koda u jednadžbu: ispalo bi da je u biti 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 provjerom, a zatim dobivamo odgovor što podaci se moraju dostaviti kao input za postizanje cilja.
Zadatak o vuku, kozi i kupusu je po meni još zanimljiviji, jer njegovo rješavanje već zahtijeva mnogo (7) koraka.
Ako je problem s kraljicom usporediv sa slučajem u kojem možete prodrijeti u poslužitelj koristeći jedan GET ili POST zahtjev, 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 zahtjeva.
To se može usporediti, 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.
Uvjeti problema i njegovo rješenjeSeljak treba prevesti vuka, kozu i kupus preko rijeke. Farmer ima čamac u koji može stati samo jedan objekt, osim samog farmera. Vuk će pojesti kozu, a koza će pojesti kupus ako ih seljak ostavi bez nadzora.
Rješenje je da će u koraku 4 farmer morati uzeti kozu natrag.
Sada počnimo to rješavati programski.
Označimo seljaka, vuka, kozu i kupus kao 4 varijable koje imaju vrijednost samo 0 ili 1. Nula znači da su na lijevoj obali, a jedinica 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, broda i svih entiteta.
Za sada, odaberimo ga nasumično i s marginom, uzmimo 10.
Svaki entitet je predstavljen u 10 primjeraka - to je njegova vrijednost u svakom od 10 koraka.
Sada postavimo uvjete za start 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 uvjete u kojima vuk jede kozu ili koza jede kupus, kao ograničenja u jednadžbi.
(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, definirat ćemo sve moguće radnje farmera pri prelasku tamo ili natrag.
Može ili povesti sa sobom vuka, kozu ili kupus, ili ne povesti nikoga, ili nikamo ne isploviti.
Naravno, nitko ne može prijeći bez farmera.
To će biti izraženo činjenicom da se svako sljedeće stanje rijeke, broda i entiteta može razlikovati od prethodnog samo na strogo ograničen način.
Ne više od 2 bita, uz mnoga druga ograničenja, budući da farmer može transportirati samo jedan entitet u isto vrijeme 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 dobivamo odgovor!
Z3 je pronašao konzistentan skup stanja koji zadovoljava sve uvjete.
Neka vrsta četverodimenzionalnog odljeva prostor-vremena.
Idemo shvatiti što se dogodilo.
Vidimo da su na kraju svi prešli, samo je naš farmer prvo odlučio odmoriti, au prva 2 koraka ne pliva nigdje.
Human_2 = 0
Human_3 = 0
Ovo sugerira da je broj država koje smo odabrali pretjeran, a 8 će biti sasvim dovoljno.
Kod nas je seljak napravio ovako: krenuti, odmoriti se, odmoriti se, prijeći kozu, prijeći natrag, preći kupus, vratiti se s kozom, preći vuka, vratiti se sam natrag, ponovno predati kozu.
Ali na kraju je problem riješ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 uvjete i dokazati da rješenja nema.
Da bismo to učinili, dat ćemo našem vuku biljojed, a on će htjeti jesti kupus.
To se može usporediti sa slučajem u kojem nam je cilj osigurati aplikaciju i moramo biti sigurni da nema rupa u zakonu.
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
Znači da stvarno nema rješenja.
Time smo programski dokazali nemogućnost križanja s vukom svejedim bez gubitaka za farmera.
Ako publika smatra ovu temu zanimljivom, tada ću vam u budućim člancima 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. Najprije na istom zadatku, ali prikazanom u obliku programa, a zatim ga postupno komplicirajući i prelazeći na aktualne primjere iz svijeta razvoja softvera.
Sljedeći članak je već spreman:
U njemu prelazim s formalne verifikacije problema na programe i opisujem ih
kako se mogu automatski pretvoriti u formalne sustave pravila.
Izvor: www.habr.com