Mano nuomone, rusakalbiame interneto sektoriuje formalaus patikrinimo tema nėra pakankamai išnagrinėta, ypač trūksta paprastų ir aiškių pavyzdžių.
Pateiksiu pavyzdį iš užsienio šaltinio ir pridėsiu savo sprendimą gerai žinomai vilko, ožio ir kopūsto kirtimo kitapus upės problemai.
Bet pirmiausia trumpai aprašysiu, kas yra formalus patikrinimas ir kodėl jis reikalingas.
Oficialus patikrinimas paprastai reiškia vienos programos ar algoritmo patikrinimą naudojant kitą.
Tai būtina norint užtikrinti, kad programa veiktų taip, kaip tikimasi, ir užtikrinti jos saugumą.
Oficialus patikrinimas yra galingiausia pažeidžiamumų radimo ir pašalinimo priemonė: ji leidžia rasti visas esamas programos spragas ir klaidas arba įrodyti, kad jų nėra.
Verta paminėti, kad kai kuriais atvejais tai neįmanoma, pavyzdžiui, 8 karalienių, kurių lentos plotis 1000 kvadratų, uždavinys: viskas priklauso nuo algoritmo sudėtingumo arba stabdymo problemos.
Tačiau bet kuriuo atveju bus gautas vienas iš trijų atsakymų: programa teisinga, neteisinga arba nepavyko apskaičiuoti atsakymo.
Jei atsakymo rasti neįmanoma, dažnai galima pertvarkyti neaiškias programos dalis, sumažinant jų algoritminį sudėtingumą, kad gautume konkretų atsakymą taip arba ne.
O formalus patikrinimas naudojamas, pavyzdžiui, Windows branduolio ir Darpa drone operacinėse sistemose, siekiant užtikrinti maksimalų apsaugos lygį.
Naudosime Z3Prover – labai galingą automatinio teoremų įrodinėjimo ir lygčių sprendimo įrankį.
Be to, Z3 išsprendžia lygtis ir nepasirenka jų verčių naudodamas brutalią jėgą.
Tai reiškia, kad jis gali rasti atsakymą net tais atvejais, kai yra 10^100 įvesties parinkčių derinių.
Tačiau tai tik apie keliolika sveikojo skaičiaus įvesties argumentų, ir su tuo dažnai susiduriama praktikoje.
Problema apie 8 karalienes (paimta iš anglų kalbos ).
# 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)
Paleidę Z3, gauname sprendimą:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Karalienės problema yra panaši į programą, kuri kaip įvestį paima 8 damų koordinates ir pateikia atsakymą, ar karalienės įveikia viena kitą.
Jei išspręstume tokią programą naudodami formalų patikrinimą, tada, palyginti su problema, mums tiesiog reikėtų žengti dar vieną žingsnį konvertuojant programos kodą į lygtį: jis iš esmės būtų identiškas mūsų ( žinoma, jei programa buvo parašyta teisingai).
Beveik tas pats nutiks ir ieškant pažeidžiamumų: mes tiesiog nustatome reikalingas išvesties sąlygas, pavyzdžiui, administratoriaus slaptažodį, šaltinį arba dekompiliuotą kodą paverčiame lygtimis, suderinamomis su patvirtinimu, ir tada gauname atsakymą, ką. norint pasiekti tikslą, reikia pateikti duomenis kaip įvesties duomenis.
Mano nuomone, problema apie vilką, ožką ir kopūstą yra dar įdomesnė, nes ją išspręsti jau reikia daug (7) žingsnių.
Jei karalienės problema yra panaši į atvejį, kai galite įsiskverbti į serverį naudodami vieną GET arba POST užklausą, tada vilkas, ožka ir kopūstas rodo pavyzdį iš daug sudėtingesnės ir labiau paplitusios kategorijos, kurioje tikslą galima pasiekti tik keliais prašymais.
Tai galima palyginti, pavyzdžiui, su scenarijumi, kai reikia rasti SQL injekciją, per ją parašyti failą, tada pakelti savo teises ir tik tada gauti slaptažodį.
Problemos sąlygos ir jos sprendimasŪkininkui reikia per upę pervežti vilką, ožką ir kopūstą. Ūkininkas turi valtį, kurioje, be paties ūkininko, telpa tik vienas objektas. Vilkas suės ožką, o ožka – kopūstą, jei ūkininkas paliks juos be priežiūros.
Sprendimas yra tas, kad 4 veiksme ūkininkas turės pasiimti ožką atgal.
Dabar pradėkime ją spręsti programiškai.
Pažymime ūkininką, vilką, ožką ir kopūstą kaip 4 kintamuosius, kurių reikšmė yra tik 0 arba 1. Nulis reiškia, kad jie yra kairiajame krante, o vienas – dešiniajame.
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
Skaičius – tai žingsnių, reikalingų išspręsti, skaičius. Kiekvienas žingsnis atspindi upės, valties ir visų objektų būklę.
Kol kas pasirinkime atsitiktinai ir su marža, imkime 10.
Kiekvienas subjektas pateikiamas 10 kopijų – tai yra jo vertė kiekviename iš 10 žingsnių.
Dabar nustatykime sąlygas startui ir finišui.
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 ]
Tada mes nustatome sąlygas, kai vilkas valgo ožką arba ožka valgo kopūstą, kaip apribojimus lygtyje.
(Ūkininko akivaizdoje agresija neįmanoma)
# 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) ]
Ir galiausiai apibrėžsime visus galimus ūkininko veiksmus kertant ten ar atgal.
Jis gali arba pasiimti su savimi vilką, ožką ar kopūstą, arba nieko nesiimti, arba išvis niekur neplaukti.
Žinoma, niekas negali kirsti be ūkininko.
Tai bus išreikšta tuo, kad kiekviena paskesnė upės, valties ir objektų būsena gali skirtis nuo ankstesnės tik griežtai ribotai.
Ne daugiau kaip 2 bitai ir su daugybe kitų apribojimų, nes ūkininkas vienu metu gali vežti tik vieną objektą ir ne visi gali būti palikti kartu.
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) ]
Paleiskite sprendimą.
solve(Side + Start + Finish + Safe + Travel)
Ir mes gauname atsakymą!
Z3 rado nuoseklų būsenų rinkinį, atitinkantį visas sąlygas.
Savotiškas keturmatis erdvės laiko atliejimas.
Išsiaiškinkime, kas atsitiko.
Matome, kad galiausiai visi kirto, tik iš pradžių mūsų ūkininkas nusprendė pailsėti, o pirmus 2 žingsnius niekur neplaukia.
Human_2 = 0
Human_3 = 0
Tai rodo, kad mūsų pasirinktų būsenų skaičius yra per didelis, o 8 visiškai pakaks.
Mūsų atveju ūkininkas darė taip: pradėk, pailsėk, pailsėk, kirsti ožką, kirsti atgal, kirsti kopūstą, grįžti su ožiuku, kirsti vilką, grįžti vienas, vėl pristatyti ožką.
Bet galų gale problema buvo išspręsta.
#Старт.
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
Dabar pabandykime pakeisti sąlygas ir įrodyti, kad sprendimų nėra.
Norėdami tai padaryti, mes duosime savo vilkui žolyną, o jis norės valgyti kopūstą.
Tai galima palyginti su tuo atveju, kai mūsų tikslas yra apsaugoti programą ir turime įsitikinti, kad nėra spragų.
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 mums pateikė tokį atsakymą:
no solution
Tai reiškia, kad sprendimų tikrai nėra.
Taip programiškai įrodėme, kad kirsti su visaėdžiu vilku be nuostolių ūkininkui neįmanoma.
Jei auditorijai ši tema bus įdomi, būsimuose straipsniuose papasakosiu, kaip įprastą programą ar funkciją paversti lygtimi, suderinama su formaliais metodais, ir ją išspręsti, taip atskleisdama visus teisėtus scenarijus ir pažeidžiamumą. Pirma, ta pati užduotis, bet pateikiama programos pavidalu, o po to palaipsniui ją apsunkinant ir pereinant prie dabartinių programinės įrangos kūrimo pavyzdžių.
Kitas straipsnis jau paruoštas:
Jame nuo formalaus problemų patikrinimo pereinu prie programų ir aprašinėju
kaip jas galima automatiškai konvertuoti į formalias taisyklių sistemas.
Šaltinis: www.habr.com