Mielestäni venäjänkielisellä Internetin sektorilla muodollisen todentamisen aihetta ei ole käsitelty riittävästi, ja erityisesti yksinkertaisista ja selkeistä esimerkeistä puuttuu.
Annan esimerkin ulkomaisesta lähteestä ja lisään oman ratkaisuni tunnettuun ongelmaan suden, vuohen ja kaalin ylittämisestä joen toiselle puolelle.
Mutta ensin kuvailen lyhyesti, mitä muodollinen todentaminen on ja miksi sitä tarvitaan.
Muodollinen todentaminen tarkoittaa yleensä yhden ohjelman tai algoritmin tarkistamista toisella.
Tämä on tarpeen, jotta varmistetaan, että ohjelma toimii odotetusti, ja myös sen turvallisuuden varmistamiseksi.
Muodollinen todentaminen on tehokkain tapa löytää ja poistaa haavoittuvuuksia: sen avulla voit löytää kaikki ohjelman aukot ja virheet tai todistaa, että niitä ei ole olemassa.
On syytä huomata, että joissakin tapauksissa tämä on mahdotonta, kuten 8 kuningattaren ongelmassa, joiden laudan leveys on 1000 ruutua: kaikki johtuu algoritmin monimutkaisuudesta tai pysäytysongelmasta.
Joka tapauksessa saadaan yksi kolmesta vastauksesta: ohjelma on oikea, virheellinen tai vastausta ei voitu laskea.
Jos vastausta on mahdotonta löytää, on usein mahdollista muokata ohjelman epäselviä osia ja vähentää niiden algoritmista monimutkaisuutta, jotta saadaan tietty kyllä tai ei vastaus.
Ja muodollista varmennusta käytetään esimerkiksi Windows-ytimen ja Darpa-drone-käyttöjärjestelmissä, jotta varmistetaan maksimaalinen suojaustaso.
Käytämme Z3Proveria, joka on erittäin tehokas työkalu automatisoituun lauseen todistamiseen ja yhtälöiden ratkaisemiseen.
Lisäksi Z3 ratkaisee yhtälöitä, eikä valitse niiden arvoja raa'alla voimalla.
Tämä tarkoittaa, että se pystyy löytämään vastauksen myös tapauksissa, joissa syöttövaihtoehtoja on 10^100 yhdistelmää.
Mutta tämä on vain noin tusina Integer-tyyppistä syöteargumenttia, ja tämä tulee usein vastaan käytännössä.
Ongelma 8 kuningattaresta (Otettu englannista ).
# 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)
Kun käytämme Z3:a, saamme ratkaisun:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Kuningatarongelma on verrattavissa ohjelmaan, joka ottaa syötteeksi 8 kuningattaren koordinaatit ja antaa vastauksen, lyövätkö kuningattaret toisiaan.
Jos ratkaisisimme tällaisen ohjelman käyttämällä muodollista todentamista, niin ongelmaan verrattuna meidän olisi yksinkertaisesti otettava vielä yksi askel muuttamalla ohjelmakoodi yhtälöksi: se osoittautuisi olennaisesti identtiseksi meidän kanssamme ( tietenkin, jos ohjelma on kirjoitettu oikein).
Melkein sama tapahtuu haavoittuvuuksien etsimisessä: asetamme vain tarvitsemamme lähtöehdot, esimerkiksi järjestelmänvalvojan salasanan, muunnamme lähdekoodin tai puretun koodin vahvistuksen kanssa yhteensopiviin yhtälöihin ja saamme sitten vastauksen, mitä tiedot on toimitettava syötteenä tavoitteen saavuttamiseksi.
Minusta suden, vuohen ja kaalin ongelma on vielä mielenkiintoisempi, koska sen ratkaiseminen vaatii jo monta (7) askelta.
Jos kuningatar-ongelma on verrattavissa tapaukseen, jossa voit tunkeutua palvelimelle yhdellä GET- tai POST-pyynnöllä, niin susi, vuohi ja kaali on esimerkki paljon monimutkaisemmasta ja laajemmasta kategoriasta, jossa tavoite voidaan saavuttaa vain useiden pyyntöjen perusteella.
Tämä on verrattavissa esimerkiksi tilanteeseen, jossa sinun on löydettävä SQL-injektio, kirjoitettava tiedosto sen kautta, nostettava oikeuksiasi ja vasta sitten hankittava salasana.
Ongelman ehdot ja sen ratkaisuViljelijän on kuljetettava susi, vuohi ja kaali joen yli. Viljelijällä on vene, johon mahtuu vain yksi esine maanviljelijän itsensä lisäksi. Susi syö vuohen ja vuohi syö kaalin, jos viljelijä jättää ne ilman valvontaa.
Ratkaisu on, että vaiheessa 4 viljelijän on otettava vuohi takaisin.
Aloitetaan nyt sen ratkaiseminen ohjelmallisesti.
Merkitään viljelijää, susia, vuohetta ja kaalia 4 muuttujaksi, jotka saavat arvon vain 0 tai 1. Nolla tarkoittaa, että ne ovat vasemmalla rannalla, ja yksi tarkoittaa, että ne ovat oikealla.
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 ratkaisemiseen tarvittavien vaiheiden lukumäärä. Jokainen askel edustaa joen, veneen ja kaikkien kokonaisuuksien tilaa.
Toistaiseksi valitaan se satunnaisesti ja marginaalilla otetaan 10.
Jokainen entiteetti on edustettuna 10 kopiona - tämä on sen arvo kussakin 10 vaiheessa.
Laitetaan nyt lähtö- ja maaliehdot.
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 ]
Sitten asetamme yhtälöön rajoituksiksi ehdot, joissa susi syö vuohen tai vuohi syö kaalin.
(Maanviljelijän läsnäollessa aggressio on mahdotonta)
# 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 lopuksi määrittelemme kaikki mahdolliset viljelijän toimet ylitettäessä sinne tai takaisin.
Hän voi ottaa mukaansa suden, vuohen tai kaalin tai olla ottamatta ketään mukaan tai olla purjehtimatta ollenkaan.
Tietenkään kukaan ei voi ylittää ilman maanviljelijää.
Tämä ilmenee siinä, että jokainen myöhempi joen, veneen ja kokonaisuuksien tila voi poiketa edellisestä vain tiukasti rajoitetusti.
Enintään 2 bittiä ja monilla muilla rajoituksilla, koska viljelijä voi kuljettaa vain yhden kokonaisuuden kerrallaan eikä kaikkia voi jättää yhteen.
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) ]
Ajetaan ratkaisu.
solve(Side + Start + Finish + Safe + Travel)
Ja saamme vastauksen!
Z3 löysi johdonmukaisen joukon tiloja, jotka täyttävät kaikki ehdot.
Eräänlainen neliulotteinen aika-avaruus.
Selvitetään mitä tapahtui.
Näemme, että lopulta kaikki ylittivät, vain aluksi viljelijämme päätti levätä, ja ensimmäisissä kahdessa vaiheessa hän ei ui missään.
Human_2 = 0
Human_3 = 0
Tämä viittaa siihen, että valitsemiemme tilojen määrä on liian suuri, ja 8 on aivan riittävä.
Meidän tapauksessamme maanviljelijä teki näin: aloita, lepää, lepää, ylitä vuohi, ylitä takaisin, ylitä kaali, palasi vuohen kanssa, ylitti suden, palaa takaisin yksin, toimitti vuohen uudelleen.
Mutta lopulta ongelma ratkesi.
#Старт.
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
Yritetään nyt muuttaa ehtoja ja todistaa, ettei ratkaisuja ole.
Tätä varten annamme susimme kasvissyöjällemme, ja hän haluaa syödä kaalia.
Tätä voidaan verrata tapaukseen, jossa tavoitteenamme on suojata sovellus ja meidän on varmistettava, ettei porsaanreikiä 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 antoi meille seuraavan vastauksen:
no solution
Se tarkoittaa, että ratkaisuja ei todellakaan ole.
Todistimme siis ohjelmallisesti, että kaikkiruokaisen suden kanssa ei ole mahdollista risteytyä ilman tappioita viljelijälle.
Jos yleisö pitää tätä aihetta kiinnostavana, kerron tulevissa artikkeleissa, kuinka tavallinen ohjelma tai funktio muutetaan muodollisten menetelmien kanssa yhteensopivaksi yhtälöksi ja ratkaistaan, mikä paljastaa sekä kaikki oikeutetut skenaariot että haavoittuvuudet. Ensin samassa tehtävässä, mutta esiteltiin ohjelman muodossa, ja sitten vähitellen monimutkaistaan ja siirrytään ajankohtaisiin esimerkkeihin ohjelmistokehityksen maailmasta.
Seuraava artikkeli on jo valmis:
Siinä siirryn muodollisesta ongelmien todentamisesta ohjelmiin ja kuvaan
kuinka ne voidaan muuntaa automaattisesti muodollisiksi sääntöjärjestelmiksi.
Lähde: will.com