Minu arvates on vene keeles internetis formaalse verifitseerimise teema ebapiisavalt kaetud ning eriti puuduvad lihtsad ja selged näited.
Toon ühe näite välismaisest allikast ja täiendan oma lahendusega tuntud ülesande kohta, kuidas ületada hunt, kits ja kapsas jõe teisele poole.
Kuid esmalt kirjeldan lühidalt, mis on formaalne verifitseerimine ja miks see on vajalik.
Formaalse verifitseerimise all mõistetakse tavaliselt ühe programmi või algoritmi kontrollimist teise abil.
See on vajalik selleks, et veenduda, et programmi käitumine vastab ootustele ja tagada selle turvalisus.
Formaalse verifitseerimise abil saab tuvastada ja kõrvaldada haavatavusi: see võimaldab leida kõik olemasolevad augud ja vead programmis või tõestada, et neid ei ole.
M值得 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 peatamisprobleemist.
Siiski saadakse igal juhul üks kolmest vastusest: programm on korrektne, ebaõige või - vastust ei suutnud leida.
Kui vastuse leidmine on võimatu, saab sageli töödelda ebaselgeid kohti programmis, vähendades nende algoritmilist keerukust, et saada konkreetne jah või ei.
Formaalse verifitseerimise rakendamine toimub näiteks Windowsi tuumas ja Darpa droonide operatsioonisüsteemides, et tagada maksimaalne kaitsetase.
Kasutame Z3Proverit, väga võimsat tööriista teoreemide automaatseks tõestamiseks ja võrrandite lahendamiseks.
Z3 lahendab tõeliselt võrrandeid, mitte ei püüa leida väärtusi jõhkralt brute force’iga.
See tähendab, et ta suudab leida vastuse isegi siis, kui sisendvariantide kombinatsioone on 10^100.
Ja see on vaid umbes tosin sisendargumendid, näiteks Integer, ja sarnast tuleb praktikas tihti ette.
8 daami ülesanne (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)
Z3 käivitamisel 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]
Daamide ülesanne on võrreldav programmiga, mis võtab sisendiks 8 daami koordinaadid ja annab vastuse, kas nad tülitavad üksteist.
Kui me lahendaksime seda programmi formaalse verifikatsiooni kaudu, vajaksime võrreldes ülesande lahendamisega lihtsalt veel ühte sammu, muutes programmi koodi võrrandiks: see osutuks oma olemuselt identseks meiega (loomulikult eeldusel, et programm on kirjutatud vigadeta).
Suunas, kus otsime haavatavusi, toimub praktiliselt sama: me lihtsalt määrame vajalikud väljundtingimused, näiteks administraatori parooli, muundame algse või dekompileeritud koodi verifikatsiooniga ühilduvateks võrranditeks ja seejärel saame vastuse, milliseid andmeid tuleb sisendina kasutada, et saavutada soovitud eesmärk.
Minu arvates on hunt, kits ja kapsas veelgi huvitavam probleem, kuna selle lahendamiseks on juba vajalik palju (7) sammu.
Kui vene kuninganna ülesanne on võrreldav variandiga, kus serverisse pääsemiseks piisab ühest GET või POST-päringust, siis hunt, kits ja kapsas näitab näidet palju keerulisematest ja levinumatest kategooriatest, kus eesmärkide saavutamiseks on vajalikud mitmed päringud.
See on võrreldav näiteks stsenaariumiga, kus tuleb leida SQL-injekteerimine, läbi selle faili kirjutamine, seejärel oma õiguste tõstmine ja alles pärast seda parooli saamine.
Ülesande tingimused ja selle lahendusFarmer peab üle jõe viima hundi, kitsi ja kapsa. Farmeril on paat, kuhu peale tema enda mahub ainult üks objekt. Hunt sööb kiti ja kits sööb kapsast, kui farmer neid järelevalveta jätab.
Lahendus seisneb selles, et neljandas sammus peab farmer viima kitsi tagasi.
Nüüd liikume lahenduse juurde programmeerimise teel.
Määratleme farmeri, hundi, kitsi ja kapsa kui 4 muutujat, mis võtavad väärtusi ainult 0 või 1. Null tähendab, et nad on vasakul kaldal, ja üks, et 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 olend võib olla ainult vasakul (0) või paremal (1) iga oleku korral
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 — see on sammude arv, mis on vajalik lahenduse leidmiseks. Iga samm kujutab endast jõe, paadi ja kõigi olendite olekut.
Valime selle juhuslikult ja varuga, võtame 10.
Iga olend on esindatud 10 eksemplariga — see on tema väärtus igaühel 10 sammust.
Nüüd seadke tingimused alguse ja lõpu jaoks.
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 kohal on farmer, pole 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 tegevused, mida farmer saab üle minna või tagasi tulla.
Ta võib võtta endaga kaasa hinde, kitsa või kapsa, või ei võtta kedagi, või üldse mitte liikuda.
Muidugi, ilma farmerita ei saa keegi ületada.
See väljendub selles, et iga järgnev olek jõe, paadi ja olenditega võib erineda eelnevast ainult rangelt piiratud viisil.
Mitte rohkem kui 2 bitti ja paljude teiste piirangutega, kuna farmer saab korraga viia ainult ühe olendi ja mitte kõik ei saa üksi jääda.
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ärjepideva ja kõikidele tingimustele vastava olekute kogumi.
Kuidagi neljamõõtmeline ajaruumi koopia.
Vaatame, mis tegelikult juhtus.
Näeme, et lõpuks kõik ületasid, kuid alguses otsustas meie farmer puhata ja ei liikunud esimesed 2 sammu.
Human_2 = 0
Human_3 = 0
See näitab, et valisime seisundite arvu liiga suureks ja 8 kõlbab täiesti.
Meie puhul käitus farmer järgmiselt: start, puhkus, puhkus, kitsi ületamine, tagasimine, kapsa ületamine, naasmine kitsega, hundi ületamine, tagasimine üksi, kitse taaskohandamine.
Ent ülesanne on lõpuks 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 tingimusi muuta 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 nõrku kohti 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:
ei ole lahendust
See tähendab, et lahendusi tõeliselt ei ole.
Seega oleme programmeerimise teel tõestanud, et mitte mingit lahendust ei ole ahvilise hundiga üleveo tegemiseks ilma, et tal oleks kaotusi.
Kui publik leiab selle teema huvitavaks, siis järgnevas artiklis räägin, kuidas muuta tavaline programm või funktsioon ühilduvaks formaalsete meetoditega, ning lahendada see, tuvastades nii kõik legaalsed stsenaariumid kui ka haavatavused. Esiteks samas ülesandes, kuid juba programmina esitatud, seejärel järk-järgult keerulisemaks muutes ja liikudes tarkvaraarenduse maailma aktuaalsetele näidetele.
Järgmine artikkel on juba valmis:
Selles lähenen formaalverifikatsiooni ülesannetest programmide poole ja kirjeldan,
kuidas neid automaatselt formaalsete reeglite süsteemideks konverteerida.
Allikas: habr.com
