Véleményem szerint az internet orosz nyelvű szektorában a formális ellenőrzés témája nem foglalkozik kellőképpen, és különösen hiányoznak az egyszerű és világos példák.
Mondok egy külföldi forrásból származó példát, és hozzáteszem a saját megoldásomat a jól ismert farkas, kecske és káposzta átkelés problémájára a folyó túlsó partjára.
Először azonban röviden leírom, mi az a formális ellenőrzés, és miért van rá szükség.
A formális ellenőrzés általában azt jelenti, hogy egy program vagy algoritmus egy másikkal ellenőrzi.
Erre azért van szükség, hogy a program az elvárásoknak megfelelően működjön, valamint a biztonsága érdekében.
A formális ellenőrzés a sebezhetőségek megtalálásának és megszüntetésének leghatékonyabb módja: lehetővé teszi, hogy megtalálja a programban lévő összes hiányosságot és hibát, vagy bebizonyítsa, hogy nem léteznek.
Érdemes megjegyezni, hogy bizonyos esetekben ez lehetetlen, például a 8 dáma problémájában, 1000 négyzet szélességű tábla esetén: mindez az algoritmus bonyolultságán vagy a leállítási problémán múlik.
Mindenesetre három válasz egyike érkezik: a program helyes, hibás, vagy nem lehetett kiszámítani a választ.
Ha nem lehet választ találni, gyakran lehetőség van a program homályos részeinek átdolgozására, csökkentve azok algoritmikus bonyolultságát, hogy konkrét igen vagy nem választ kapjunk.
A formális ellenőrzést pedig például a Windows kernel és a Darpa drone operációs rendszerekben alkalmazzák a maximális védelem biztosítása érdekében.
A Z3Provert fogjuk használni, amely egy nagyon hatékony eszköz az automatizált tételbizonyításhoz és egyenletmegoldáshoz.
Ezenkívül a Z3 egyenleteket old meg, és nem nyers erővel választja ki az értékeket.
Ez azt jelenti, hogy képes megtalálni a választ még olyan esetekben is, amikor a beviteli lehetőségek 10^100 kombinációja van.
De ez csak körülbelül egy tucat Integer típusú bemeneti argumentum, és ezzel gyakran találkozunk a gyakorlatban.
Probléma 8 dámával kapcsolatban (angolból átvéve ).
# 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)
A Z3 futtatásával megkapjuk a megoldást:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
A királynő probléma egy olyan programhoz hasonlítható, amely 8 dáma koordinátáit veszi be, és azt a választ adja, hogy a királynők verik-e egymást.
Ha egy ilyen programot formális verifikációval oldanánk meg, akkor a problémához képest egyszerűen még egy lépést kellene tennünk a programkód egyenletté alakítása formájában: kiderülne, hogy lényegében megegyezik a miénkkel ( persze, ha a program helyesen volt megírva).
Majdnem ugyanez fog történni a sebezhetőségek keresése esetén is: csak beállítjuk a szükséges kimeneti feltételeket, például az adminisztrátori jelszót, a forráskódot vagy a visszafordított kódot hitelesítéssel kompatibilis egyenletekké alakítjuk, majd választ kapunk, hogy mit adatokat kell megadni bemenetként a cél eléréséhez.
Szerintem a farkas, a kecske és a káposzta probléma még érdekesebb, hiszen a megoldása már sok (7) lépést igényel.
Ha a királynő probléma ahhoz az esethez hasonlítható, amikor egyetlen GET vagy POST kéréssel be lehet jutni egy szerverre, akkor a farkas, kecske és káposzta egy sokkal összetettebb és elterjedtebb kategóriából mutat példát, amelyben a cél csak akkor érhető el. több kéréssel is.
Ez hasonlítható például egy olyan forgatókönyvhöz, amikor meg kell találni egy SQL-befecskendezést, fájlt kell írnia rajta, majd meg kell emelni a jogait, és csak ezután kell jelszót kapnia.
A probléma feltételei és megoldásaA gazdának farkast, kecskét és káposztát kell átszállítania a folyón. A gazdának van egy csónakja, amelyen magán kívül csak egy tárgy fér el. A farkas megeszi a kecskét, a kecske pedig a káposztát, ha a gazda felügyelet nélkül hagyja.
A válasz az, hogy a 4. lépésben a gazdának vissza kell vinnie a kecskét.
Most kezdjük el programozottan megoldani.
Jelöljük a gazdát, a farkast, a kecskét és a káposztát 4 változóként, amelyek csak 0 vagy 1 értéket vesznek fel. A nulla azt jelenti, hogy a bal parton vannak, az egy pedig azt, hogy a jobb oldalon.
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 a megoldáshoz szükséges lépések száma. Minden lépés a folyó, a hajó és az összes entitás állapotát jelzi.
Egyelőre válasszuk véletlenszerűen, és egy margóval vegyünk 10-et.
Minden entitás 10 példányban jelenik meg – ez az értéke a 10 lépés mindegyikénél.
Most határozzuk meg a rajt és a cél feltételeit.
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 ]
Ezután az egyenletben kötöttségként beállítjuk azokat a feltételeket, ahol a farkas megeszi a kecskét, vagy a kecske megeszi a káposztát.
(Paraszt jelenlétében az agresszió lehetetlen)
# 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) ]
Végül pedig meghatározzuk a gazdálkodó minden lehetséges intézkedését oda- vagy visszautazáskor.
Vagy vihet magával farkast, kecskét vagy káposztát, vagy nem visz senkit, vagy egyáltalán nem vitorlázhat sehova.
Természetesen senki sem tud átkelni gazda nélkül.
Ezt fejezi ki az a tény, hogy a folyó, csónak és entitások minden további állapota csak szigorúan korlátozottan térhet el az előzőtől.
Legfeljebb 2 bit, és sok más korláttal, mivel a gazdálkodó egyszerre csak egy entitást szállíthat, és nem lehet mindent együtt hagyni.
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) ]
Futtassuk a megoldást.
solve(Side + Start + Finish + Safe + Travel)
És megkapjuk a választ!
A Z3 olyan következetes állapothalmazt talált, amely minden feltételt kielégít.
A téridő egyfajta négydimenziós öntése.
Találjuk ki, mi történt.
Látjuk, hogy a végén mindenki átkelt, csak először a gazdánk döntött úgy, hogy pihen, és az első 2 lépésben nem ússza meg sehol.
Human_2 = 0
Human_3 = 0
Ez arra utal, hogy az általunk választott állapotok száma túlzott, és 8 elég lesz.
Nálunk a gazda ezt csinálta: indulás, pihenés, pihenés, átkel a kecskén, átmegy vissza, át a káposztán, vissza a kecskével, keresztbe a farkassal, vissza egyedül, visszaadni a kecskét.
De végül a probléma megoldódott.
#Старт.
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
Most próbáljuk meg megváltoztatni a feltételeket, és bebizonyítani, hogy nincsenek megoldások.
Ehhez adjuk a farkasunk növényevőjét, ő pedig káposztát akar majd enni.
Ez ahhoz az esethez hasonlítható, amikor az alkalmazás biztonságossá tétele a célunk, és ügyelnünk kell arra, hogy ne legyenek kiskapuk.
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) ]
A Z3 a következő választ adta nekünk:
no solution
Ez azt jelenti, hogy tényleg nincsenek megoldások.
Így programszerűen bebizonyítottuk, hogy lehetetlen a mindenevő farkassal keresztezni veszteség nélkül a gazdálkodó számára.
Ha a közönség érdekesnek találja ezt a témát, akkor a következő cikkekben elmondom, hogyan lehet egy hétköznapi programot vagy függvényt formális módszerekkel kompatibilis egyenletté alakítani és megoldani, feltárva ezzel az összes jogos forgatókönyvet és sebezhetőséget. Először ugyanazon a feladaton, de program formájában bemutatva, majd fokozatosan bonyolítva, áttérve a szoftverfejlesztés világának aktuális példáira.
Már kész is a következő cikk:
Ebben a problémák formális ellenőrzésétől a programok felé haladok, és leírom
hogyan alakíthatók át automatikusan formális szabályrendszerekké.
Forrás: will.com