Minu arvates on venekeelses internetis formaalse verifitseerimise teema ebapiisavalt kajastatud, eriti puuduvad lihtsad ja selged näited.
Toon ühe näite välismaalt ja täiendan seda oma lahendusega tuntud probleemist, kus tuleb ületada hunt, kits ja kapsas jõe poolt.
Kuid esmalt kirjeldan lühidalt, mis on formaalne verifitseerimine ja milleks seda vaja on.
Formaalse verifitseerimise all mõistetakse tavaliselt ühe programmi või algoritmi kontrollimist teise abil.
Seda on vaja selleks, et veenduda, et programmi käitumine vastab ootustele ja tagada selle ohutus.
Formaalse verifitseerimise abil on kõige tõhusam meetod haavatavuste leidmiseks ja kõrvaldamiseks: see võimaldab leida kõik olemasolevad vead ja probleemid programmis või tõestada, et neid pole.
On oluline märkida, et mõnel juhul on see võimatu, nagu näiteks 8 daami ülesandes, kus laua laius on 1000 ruutu: kõik sõltub algoritmilisest keerukusest või peatamise probleemist.
Kuid igal juhul saadakse üks kolmest vastusest: programm on õige, vale või ei õnnestunud vastust leida.
Kui vastuse leidmine on võimatu, on sageli võimalik töötada ümber programmikahtlased osad, vähendades nende algoritmilist keerukust, et saada konkreetne jah või ei.
Formaalset verifitseerimist, näiteks Windowsi tuumas ja Darpa droonide operatsioonisüsteemides, kasutatakse maksimaalse kaitse tagamiseks.
Kasutame Z3Proverit, mis on väga võimas automatiseeritud teoreemide tõendamise ja võrrandite lahendamise tööriist.
Z3 lahendab vahetult võrrandeid, mitte ei püüa nende väärtusi bruteforce'i teel.
See tähendab, et ta suudab leida vastuse, isegi juhul, kui sisendvariandi kombinatsioone on 10^100.
Ja see on vaid umbes tosin täisarvudest koosnevat sisendargumendi, mis esineb praktikas tihti.
8 daami probleem (Võetud ingliskeelsest ).
# 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)
Käivitades Z3, 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]
Vähiülesanne on võrreldav programmiga, mis võtab sisendiks 8 vähi koordinaati ja väljastab vastuse, kas vähid üksteist ründavad.
Kui me lahendaksime sarnase programmi formaalse verifitseerimise abil, siis võrreldes ülesandega peaksime lihtsalt tegema veel ühe sammu, muundades programmi koodi võrrandiks: see osutuks olemuselt identseks meiega (loomulikult, kui programm on kirjutatud ilma vigadeta).
Peaaegu sama juhtub haavatavuste otsimisel: me simply seame vajalikud väljunditingimused, näiteks admini parooli, muundame algse või dekompileeritud koodi verifitseerimisega ühilduvateks võrranditeks ja saame seejärel vastuse, milliseid andmeid tuleb sisendiks anda, et eesmärki saavutada.
Minu arvates on hundi, kitse ja kapsa ülesanne veelgi huvitavam, kuna selle lahendamiseks on vaja juba palju (7) sammu.
Kui džessipüüd oleks võrreldav olukorraga, kus saab serverisse siseneda ühe GET või POST päringuga, siis hunt, kits ja kapsas näitab näidet palju keerulisemast ja levinumast kategooriast, kus eesmärke on võimalik saavutada ainult mitme päringuga.
See on võrreldav näiteks stsenaariumiga, kus tuleb leida SQL süstimine, kirjutada läbi selle fail, seejärel oma õigusi tõsta ja lõpuks parool saada.
Ülesande tingimused ja selle lahendusFermere peab üle tooma jõe kaudu hundi, kitsi ja kapsa. Fermere paadis on ruumi lisaks talunikule ainult ühele objektile. Hunt sööb kiti, kui talunik jätab nad järelevalveta, ja kits sööb kapsa.
Lahendus on see, et 4. sammul peab talunik viima kiti tagasi.
Nüüd asume lahendama programmiliselt.
Määratleme taluniku, hundi, kiti ja kapsa neljana muutujana, mis võivad võtta väärtuse ainult 0 või 1. Null tähendab, et need on vasakul kaldal, ja üks, et nad on 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) ]
# Iga olendid saavad olla kas vasakul (0) või paremal (1) igas olekus
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 sammude arv, mis on vajalik lahenduse leidmiseks. Iga samm esindab jõe, paadi ja kõigi elementide olekut.
Praegu valime selle juhuslikult ja varuga, võtame 10.
Iga element on esindatud 10 eksemplariga — see on selle väärtus igal 10 sammul.
Nüüd seadke alg- ja lõppetingimused.
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 seadke tingimused, kus hunt sööb kitsi või kits sööb kapsast, kui piirangud võrrandis.
(Kuna farmeri kohalolekul ei ole agressioon võimalik)
# 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 seadke kõik võimalikud farmeri tegevused, kui ta ületab edasi või tagasi.
Ta võib võtta kaasa kas hundi, kitsi või kapsa, või mitte kedagi kaasa võtta, või täiesti mitte sõuda.
Muidugi, ilma talunikuta ei saa keegi üle minna.
See väljendub selles, et iga järgmine seisund jõel, paadil ja olenditel võib erineda eelmisest ainult rangelt piiratud viisil.
Mitte rohkem kui 2 bitti ja palju muid piiranguid, kuna talunik suudab korraga üle viia vaid ühe olendi ning kõiki ei saa korraga 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 vastuolulise ja kõiki tingimusi rahuldava seisundite kogumi.
Nii-öelda neljamõõtmeline ajaruumikuju.
Vaatame, mis siin juhtus.
Näeme, et lõpuks kõik ületasid, kuid alguses otsustas meie taluniku puhata ja ei liikunud esimestel kahel sammul kuhugi.
Human_2 = 0
Human_3 = 0
See näitab, et valisime olekute arvu liialt ja 8 on täiesti piisav.
Meie puhul tegutses talunik järgmiselt: algus, puhkus, puhkus, koti ületamine, tagasi ületamine, kapsa ületamine, kaameli tagasiviimine, hundi ületamine, üksi tagasi pöördumine, uuesti kaameli toimetamine.
Ent lõpuks on ülesanne 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
Nüüd proovime olukordi vahetada ja tõestada, et lahendusi ei ole.
Selleks anname meie hundile taimetoitluse ja ta tahab kapsast süüa.
Seda võib võrrelda juhtumiga, kus meie eesmärk on rakenduse kaitsmine ja me peame veenduma, et prahti ei ole.
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:
ei lahendust
See tähendab, et lahendusi tõepoolest ei ole.
Nii oleme programmiliselt tõestanud, et kõigesööva hundi saatmine on talunikule vastuvõetamatu kaotuseta.
Kui publik peab seda teemat huvitavaks, siis järgmistes artiklites räägin, kuidas tavaline programm või funktsioon vormistada sobivaks formaalseteks meetoditeks ja kuidas seda lahendada, avastades seega kõik seaduslikud stsenaariumid ning haavatavused. Alustame samal ülesandel, aga programmi kujul, ning liigutame järk-järgult keerulisematele kaasaaegsetele näidetele tarkvaraarenduse maailmas.
Järgmine artikkel on juba valmis:
Selles liigun ma formaalsest verifitseerimisest ülesannete juures programmide suunas ja kirjeldan,
kuidas neid automaatselt formaalseteks reegliteks konverteerida.
Allikas: habr.com
