Minu arvates ei ole venekeelses internetisektoris formaalse kontrolli teema piisavalt käsitletud ning eriti napib lihtsaid ja selgeid näiteid.
Toon näite välismaisest allikast ja lisan omapoolse lahenduse tuntud probleemile hundi, kitse ja kapsa ületamisel teisele poole jõge.
Kuid kõigepealt kirjeldan lühidalt, mis on formaalne kontrollimine ja miks seda vaja on.
Ametlik kontrollimine tähendab tavaliselt ühe programmi või algoritmi kontrollimist teise programmi või algoritmi abil.
See on vajalik programmi ootuspärase käitumise tagamiseks ja ka selle turvalisuse tagamiseks.
Ametlik kontrollimine on kõige võimsam vahend haavatavuste leidmiseks ja kõrvaldamiseks: see võimaldab leida programmis kõik olemasolevad augud ja vead või tõestada, et neid pole.
Väärib märkimist, et mõnel juhul on see võimatu, näiteks 8 ruudu laiusega 1000 emanda probleemi puhul: kõik taandub algoritmilisele keerukusele või peatamisprobleemile.
Kuid igal juhul saabub üks kolmest vastusest: programm on õige, vale või ei olnud võimalik vastust välja arvutada.
Kui vastust pole võimalik leida, on sageli võimalik programmi ebaselgeid osi ümber töötada, vähendades nende algoritmilist keerukust, et saada konkreetne jah või ei vastus.
Ja formaalset verifitseerimist kasutatakse näiteks Windowsi kerneli ja Darpa drone operatsioonisüsteemides, et tagada maksimaalne kaitsetase.
Kasutame Z3Proverit, mis on väga võimas tööriist teoreemide automaatseks tõestamiseks ja võrrandite lahendamiseks.
Lisaks lahendab Z3 võrrandeid ega vali nende väärtusi toore jõu abil.
See tähendab, et see suudab leida vastuse isegi juhtudel, kui sisestusvalikute kombinatsioone on 10^100.
Kuid see on vaid kümmekond Integer tüüpi sisendargumenti ja seda kohtab praktikas sageli.
Probleem 8 kuninganna kohta (võetud inglise keelest ).
# 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)
Z3 käivitades saame lahenduse:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Kuninganna probleem on võrreldav programmiga, mis võtab sisendiks 8 emanda koordinaadid ja väljastab vastuse, kas emandad võidavad üksteist.
Kui lahendaksime sellise programmi formaalse verifitseerimise abil, siis võrreldes probleemiga oleks meil vaja lihtsalt teha veel üks samm programmi koodi võrrandiks teisendamise näol: see osutuks sisuliselt identseks meie omaga ( muidugi juhul, kui programm oli õigesti kirjutatud).
Peaaegu sama juhtub turvaaukude otsimise puhul: seame lihtsalt vajalikud väljundtingimused, näiteks administraatori parooli, teisendame lähtekoodi või dekompileeritud koodi verifitseerimisega ühilduvateks võrranditeks ja saame siis vastuse, mida eesmärgi saavutamiseks tuleb sisendina esitada andmed.
Hundi, kitse ja kapsa probleem on minu meelest veelgi huvitavam, kuna selle lahendamine nõuab juba palju (7) sammu.
Kui kuninganna probleem on võrreldav juhtumiga, kus serverisse saab tungida ühe GET- või POST-päringu abil, siis hunt, kits ja kapsas demonstreerib näidet palju keerulisemast ja laiemalt levinud kategooriast, kus eesmärki saab saavutada ainult mitme palvega.
See on võrreldav näiteks stsenaariumiga, kus tuleb leida SQL-i süst, selle kaudu fail kirjutada, seejärel oma õigusi tõsta ja alles siis parool hankida.
Probleemi tingimused ja selle lahendusTalumehel on vaja üle jõe transportida hunt, kitse ja kapsas. Talumehel on paat, kuhu peale taluniku enda mahub ainult üks objekt. Hunt sööb kitse ja kits sööb kapsast, kui talunik jätab nad järelevalveta.
Lahendus on see, et etapis 4 peab talunik kitse tagasi viima.
Nüüd hakkame seda programmiliselt lahendama.
Tähistame põllumeest, hunti, kitse ja kapsast 4 muutujana, mis saavad väärtuseks ainult 0 või 1. Null tähendab, et nad asuvad vasakul kaldal ja üks tähendab, et nad asuvad paremal.
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 on lahendamiseks vajalike sammude arv. Iga samm tähistab jõe, paadi ja kõigi üksuste olekut.
Praegu valime selle juhuslikult ja varuga, võtame 10.
Iga olem on esitatud 10 eksemplaris – see on selle väärtus igal 10 etapil.
Nüüd paneme paika stardi ja finiši tingimused.
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 ]
Seejärel seame võrrandis piiranguteks tingimused, kus hunt sööb kitse või kits sööb kapsast.
(Põllumehe juuresolekul on agressioon võimatu)
# 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) ]
Ja lõpuks määratleme kõik võimalikud põllumehe tegevused sinna või tagasi sõitmisel.
Ta võib kas hundi, kitse või kapsa kaasa võtta või mitte kedagi kaasa võtta või üldse mitte kuhugi purjetada.
Muidugi ei saa keegi üle ilma põllumeheta.
Seda väljendab asjaolu, et iga järgmine jõe, paadi ja olemite olek võib eelmisest erineda ainult rangelt piiratud viisil.
Mitte rohkem kui 2 bitti ja paljude muude piirangutega, kuna põllumees saab korraga transportida ainult ühte olemit ja kõiki ei saa kokku jätta.
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) ]
Käivitame lahenduse.
solve(Side + Start + Finish + Safe + Travel)
Ja me saame vastuse!
Z3 leidis järjekindla olekukogumi, mis vastab kõigile tingimustele.
Omamoodi neljamõõtmeline aegruum.
Uurime välja, mis juhtus.
Näeme, et lõpuks läksid kõik üle, ainult algul otsustas meie talunik puhata ja esimese 2 sammuga ei uju ta kuhugi.
Human_2 = 0
Human_3 = 0
See viitab sellele, et meie valitud olekute arv on liiga suur ja 8 on täiesti piisav.
Meie puhul tegi põllumees nii: start, puhka, puhka, risti kitse, risti tagasi, üle kapsa, naaseb koos kitsega, ületas hundi, naasis üksi tagasi, toimetas kitse uuesti.
Kuid lõpuks sai probleem lahendatud.
#Старт.
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
Proovime nüüd tingimusi muuta ja tõestada, et lahendusi pole.
Selleks anname oma hundile rohusööja ja ta tahab kapsast süüa.
Seda võib võrrelda juhtumiga, kus meie eesmärk on rakenduse turvalisus ja peame veenduma, et lünki pole.
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 andis meile järgmise vastuse:
no solution
See tähendab, et tegelikult pole lahendusi.
Nii tõestasime programmiliselt kõigesööja hundiga ristumise võimatust taluniku jaoks kahjudeta.
Kui publikule tundub see teema huvitav, siis järgmistes artiklites räägin teile, kuidas muuta tavaline programm või funktsioon formaalsete meetoditega ühilduvaks võrrandiks ja seda lahendada, paljastades seeläbi nii kõik õigustatud stsenaariumid kui ka haavatavused. Esiteks samal ülesandel, kuid esitatuna programmi kujul ja seejärel järk-järgult seda keerulisemaks muutes ja liikudes edasi aktuaalsete näidete juurde tarkvaraarenduse maailmast.
Järgmine artikkel on juba valmis:
Selles liigun probleemide formaalse kontrollimise juurest programmide juurde ja kirjeldan
kuidas saab neid automaatselt teisendada formaalseteks reeglisüsteemideks.
Allikas: www.habr.com