Po mojem mnenju v ruskojezičnem sektorju interneta tema formalnega preverjanja ni dovolj pokrita, še posebej pa primanjkuje preprostih in jasnih primerov.
Navedel bom primer iz tujega vira, dodal pa bom svojo rešitev znanega problema prehoda volka, koze in zelja na drugo stran reke.
Najprej pa bom na kratko opisal, kaj je formalno preverjanje in zakaj je potrebno.
Formalno preverjanje običajno pomeni preverjanje enega programa ali algoritma z uporabo drugega.
To je potrebno za zagotovitev, da se program obnaša po pričakovanjih, in tudi za zagotovitev njegove varnosti.
Formalno preverjanje je najmočnejše sredstvo za iskanje in odpravljanje ranljivosti: omogoča vam, da poiščete vse obstoječe luknje in hrošče v programu ali dokažete, da ne obstajajo.
Omeniti velja, da je v nekaterih primerih to nemogoče, na primer pri problemu 8 dam s širino plošče 1000 polj: vse se spušča v algoritemsko zapletenost ali problem ustavljanja.
Vendar bo v vsakem primeru prejet eden od treh odgovorov: program je pravilen, napačen ali odgovora ni bilo mogoče izračunati.
Če je nemogoče najti odgovor, je pogosto mogoče nejasne dele programa predelati in zmanjšati njihovo algoritemsko kompleksnost, da bi dobili specifičen odgovor da ali ne.
Formalno preverjanje se uporablja na primer v jedru Windows in operacijskih sistemih brezpilotnih letal Darpa, da se zagotovi najvišja raven zaščite.
Uporabili bomo Z3Prover, zelo zmogljivo orodje za samodejno dokazovanje izrekov in reševanje enačb.
Poleg tega Z3 rešuje enačbe in ne izbira njihovih vrednosti s surovo silo.
To pomeni, da lahko najde odgovor tudi v primerih, ko obstaja 10^100 kombinacij možnosti vnosa.
Toda to je le približno ducat vhodnih argumentov tipa Integer in s tem se v praksi pogosto srečujemo.
Problem o 8 kraljicah (Povzeto iz angl ).
# 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)
Z zagonom Z3 dobimo rešitev:
[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 kraljice je primerljiv s programom, ki kot vhod vzame koordinate 8 kraljic in izpiše odgovor, ali sta kraljici druga drugo premagali.
Če bi tak program reševali s formalnim preverjanjem, bi morali v primerjavi s problemom preprosto narediti še en korak v obliki pretvorbe programske kode v enačbo: izkazalo bi se, da je v bistvu identična naši ( seveda, če je bil program pravilno napisan).
Skoraj enako se bo zgodilo v primeru iskanja ranljivosti: samo nastavimo izhodne pogoje, ki jih potrebujemo, na primer skrbniško geslo, pretvorimo izvorno ali dekompilirano kodo v enačbe, združljive s preverjanjem, in nato dobimo odgovor, kaj podatke je treba posredovati kot vhod za dosego cilja.
Zadeva o volku, kozi in zelju je po mojem mnenju še toliko bolj zanimiva, saj že njena rešitev zahteva veliko (7) korakov.
Če je problem kraljice primerljiv s primerom, ko lahko prodrete v strežnik z eno samo zahtevo GET ali POST, potem je volk, koza in zelje primer iz veliko bolj kompleksne in razširjene kategorije, v kateri je cilj mogoče doseči le po več prošnjah.
To je na primer primerljivo s scenarijem, ko morate najti injekcijo SQL, prek nje napisati datoteko, nato povečati svoje pravice in šele nato pridobiti geslo.
Pogoji problema in njegova rešitevKmet mora čez reko prepeljati volka, kozo in zelje. Kmet ima čoln, ki lahko sprejme le en predmet, poleg kmeta samega. Volk bo pojedel kozo in koza bo pojedla zelje, če ju kmet pusti brez nadzora.
Rešitev je, da bo moral kmet v 4. koraku vzeti kozo nazaj.
Zdaj pa ga začnimo reševati programsko.
Označimo kmeta, volka, kozo in zelje kot 4 spremenljivke, ki imajo samo vrednost 0 ali 1. Nič pomeni, da so na levem bregu, ena pa, da so na desnem.
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 število korakov, potrebnih za rešitev. Vsak korak predstavlja stanje reke, čolna in vseh entitet.
Za zdaj ga izberimo naključno in z rezervo, vzemimo 10.
Vsaka entiteta je predstavljena v 10 kopijah – to je njena vrednost pri vsakem od 10 korakov.
Zdaj pa postavimo pogoje za start in 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 ]
Nato kot omejitve v enačbi nastavimo pogoje, kjer volk poje kozo ali koza poje zelje.
(V prisotnosti kmeta je agresija nemogoč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) ]
In na koncu bomo opredelili vsa možna dejanja kmeta pri prehodu tja ali nazaj.
S seboj lahko vzame volka, kozo ali zelje ali pa ne vzame nikogar ali pa sploh ne odpluje nikamor.
Brez kmeta seveda nihče ne more čez.
To bo izraženo z dejstvom, da se lahko vsako naslednje stanje reke, čolna in entitet razlikuje od prejšnjega le na strogo omejen način.
Ne več kot 2 bita in s številnimi drugimi omejitvami, saj lahko kmet prevaža le eno entiteto naenkrat in ne more pustiti vseh skupaj.
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) ]
Zaženimo rešitev.
solve(Side + Start + Finish + Safe + Travel)
In dobimo odgovor!
Z3 je našel konsistenten niz stanj, ki izpolnjuje vse pogoje.
Nekakšen štiridimenzionalni odlitek prostora-časa.
Ugotovimo, kaj se je zgodilo.
Vidimo, da so na koncu vsi prestopili, le naš kmet se je najprej odločil počivati, v prvih 2 korakih pa ne plava nikamor.
Human_2 = 0
Human_3 = 0
To pomeni, da je število držav, ki smo jih izbrali, preveliko in bo 8 povsem dovolj.
Pri nas je kmet naredil takole: štart, počitek, počitek, prečkaj kozo, prečkaj nazaj, prečkaj zelje, vrni se s kozo, prečkaj volka, vrni se sam nazaj, predaj kozo.
Toda na koncu je bil 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
Zdaj pa poskusimo spremeniti pogoje in dokazati, da rešitev ni.
Da bi to naredili, bomo našemu volku dali rastlinojedo hrano in hotel bo jesti zelje.
To lahko primerjamo s primerom, ko je naš cilj zaščititi aplikacijo in se moramo prepričati, da ni nobenih vrzeli.
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 dal naslednji odgovor:
no solution
To pomeni, da res ni rešitev.
Tako smo programsko dokazali nezmožnost križanja z vsejedim volkom brez izgub za kmeta.
Če se občinstvu zdi ta tema zanimiva, vam bom v prihodnjih člankih povedal, kako navaden program ali funkcijo spremeniti v enačbo, ki je združljiva s formalnimi metodami, in jo rešiti ter tako razkriti vse legitimne scenarije in ranljivosti. Najprej na isti nalogi, vendar predstavljeni v obliki programa, nato pa jo postopoma zapletamo in prehajamo na aktualne primere iz sveta razvoja programske opreme.
Naslednji članek je že pripravljen:
V njem se premaknem od formalne verifikacije problemov k programom in jih opišem
kako jih je mogoče samodejno pretvoriti v formalne sisteme pravil.
Vir: www.habr.com