Mislim da je u ruskojezičnom sektoru interneta tema formalne verifikacije nedovoljno obrađena, i posebno nedostaju jednostavni i pregledni primeri.
Navest ću jedan takav primer iz inozemnog izvora, i dopuniti vlastitim rješenjem poznate zagonetke o prijelazu vuka, koze i kupusa na drugu stranu rijeke.
Ali najprije ću ukratko objasniti što predstavlja formalna verifikacija i zašto je potrebna.
Formalna verifikacija obično se razumije kao provjera jednog programa ili algoritma pomoću drugog.
To je potrebno kako bi se osiguralo da se ponašanje programa podudara s očekivanim, kao i da bi se osigurala njegova sigurnost.
Formalna verifikacija je najmoćnije sredstvo za otkrivanje i uklanjanje ranjivosti: omogućuje pronalaženje svih postojećih sigurnosnih propusta i grešaka u programu, ili dokazivanje da ih nema.
Treba napomenuti da u nekim slučajevima to može biti nemoguće, kao što je primjer s problemom 8 kraljica na ploči širine 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 ispravan, neispravan, ili nije moguće izračunati odgovor.
U slučaju nemogućnosti pronalaska odgovora, često se može preraditi nejasna mesta u programu, smanjujući njihovu algoritamsku složenost, kako bi se dobio konkretan odgovor da ili ne.
Formalna verifikacija se, na primer, primenjuje u Windows jezgru i operativnim sistemima bespilotnih letelica Darpa, kako bi se osigurala maksimalna razina zaštite.
Koristit ćemo Z3Prover, vrlo moćan alat za automatizirano dokazivanje teorema i rešavanje jednačina.
Pri tome Z3 zapravo rešava jednačine, a ne pronalazi njihova rešenja grubim pretraživanjem.
To znači da je sposoban pronaći odgovor, čak i u slučajevima kada kombinacija ulaznih varijanti iznosi 10^100.
A to je svega oko dvanaest ulaznih argumenata tipa Integer, što se često viđa u praksi.
Problem 8 kraljica (uzeto iz 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 reš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 kraljica sličan je programu koji kao ulaz prima koordinate 8 kraljica i daje odgovor udaraju li se kraljice.
Kada bismo rješavali takav program koristeći formalnu verifikaciju, u odnosu na zadatak, jednostavno bismo trebali napraviti još jedan korak u obliku pretvaranja koda programa u jednačinu: ona bi po svojoj suštini bila identična našoj (naravno, pod uvjetom da je program bez greške).
Praktično, isto će se dogoditi i prilikom traženja ranjivosti: samo postavljamo potrebne izlazne uvjete, poput administratorske lozinke, pretvaramo izvorni ili dekompilirani kod u jednadžbe kompatibilne s verifikacijom, a zatim dobijamo odgovor koje podatke treba unijeti kako bismo postigli cilj.
Po mom mišljenju, zadatak o vuku, kozi i kupusu je još zanimljiviji, jer za njegovo rješavanje treba mnogo (7) koraka.
Ako je zadatak o kraljicama usporediv s varijantom kada se može ući na server s jednim GET ili POST zahtjevom, onda vuk, koza i kupus demonstrira primjer iz mnogo složenije i rasprostranjenije kategorije u kojoj se ciljevi mogu postići samo s nekoliko zahtjeva.
To je usporedivo, na primjer, sa scenarijom gdje je potrebno pronaći SQL injekciju, zapisati datoteku kroz nju, zatim podići svoje privilegije i tek tada dobiti lozinku.
Uvjeti zadatka i njegovo rješenjeFarmer treba prenijeti preko rijeke vuka, kozu i kupus. Farmer ima čamac u kojem može stati, osim samoga farmera, samo jedan objekt. Vuk će pojesti kozu, a koza će pojesti kupus, ako ih farmer ostavi bez nadzora.
Rješenje je da na 4. koraku farmer mora odvesti kozu nazad.
Sada ćemo pristupiti rješenju na programski način.
Odredit ćemo farmera, vuka, kozu i kupus kao 4 varijable koje mogu imati samo vrijednost 0 ili 1. Nula označava da su na lijevoj obali, a jedinica - 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) ]
# Svako biće može biti samo na lijevoj (0) ili desnoj strani (1) u svakom stanju
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 — to je broj koraka potrebnih za rješavanje. Svaki korak predstavlja stanje rijeke, čamca i svih entiteta.
Za sada ćemo ga odabrati nasumično i s rezervom, uzet ćemo 10.
Svaka entitet je predstavljena u 10 primjeraka — to je njezina vrijednost na svakom od 10 koraka.
Sada definirajmo uvjete za početak i završetak.
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 gdje vuk jede kozu, ili koza kupus, kao ograničenja u jednadžbi.
(U prisutnosti farmera agresija nije moguć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 konačno, postavićemo sve moguće radnje farmera prilikom prijenosa naprijed ili nazad.
Može uzeti sa sobom vuka, kozu ili kupus, ili ne uzeti nikoga, ili uopće ničim ne ploviti.
Naravno, bez farmera nitko ne može prijeći.
To će biti izraženo tako da svako sljedeće stanje rijeke, čamca i entiteta može odstupati od prethodnog samo na strogo ograničen način.
Ne više od 2 bita, i uz mnogo drugih limita, jer farmer može prevesti samo jedan entitet odjednom i ne može se sve ostaviti 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 dosljedan i zadovoljavajući sve uvjete skup stanja.
Kao četverodimenzionalni otisak prostora-vremena.
Hajde da vidimo što se dogodilo.
Vidimo da su se svi na kraju prebacili, samo je naš farmer na početku odlučio odmoriti se i tijekom prva 2 koraka nije plovio nigdje.
Human_2 = 0
Human_3 = 0
To pokazuje da smo odabrali prekomjeran broj stanja, a 8 će biti sasvim dovoljno.
U našem slučaju farmer se ponašao ovako: početak, odmor, odmor, prijenos koze, povratak, prijenos kupusa, povratak s kozom, prijenos vuka, povratak sam, ponovni prijenos koze.
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
Sada pokušajmo promijeniti uvjete i dokazati da rješenja nema.
Za to ćemo dati našem vuku biljojednost, i on će poželjeti pojesti kupus.
To je moguće usporediti sa slučajem u kojem je naš cilj zaštita aplikacije i moramo se uvjeriti da nema sigurnosnih 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:
nema rješenja
To znači da zaista nema rješenja.
Na taj način smo programom dokazali nemogućnost prijevoza s svejedom vukom, bez gubitaka za farmera.
Ako publika smatra ovu temu zanimljivom, u budućim člancima ću objasniti kako pretvoriti običan program ili funkciju u jednadžbu koja je kompatibilna s formalnim metodama, i riješiti je, otkrivajući na taj način kako sve legitimne scenarije, tako i ranjivosti. Prvo na ovom zadatku, ali predstavljenom već u obliku programa, a zatim postupno komplicirajući i prelazeći na aktualne primjere iz svijeta razvoja softvera.
Sljedeći članak je već spreman:
U njemu prelazim od formalne verifikacije zadataka, ka programima, i opisujem,
na koji način ih je moguće automatski konvertirati u sustave formalnih pravila.
Izvor: habr.com
