A véleményem szerint a orosz nyelvű internet szektorban a formális verifikáció témája nem elég jól van kidolgozva, és különösen hiányoznak az egyszerű és szemléletes példák.
Egy példát hozok fel egy külföldi forrásból, és kiegészítem a híres feladat megoldásával, amely a farkas, a kecske és a káposzta átkeléséről szól a folyó túloldalára.
De először is röviden leírom, hogy mi is az a formális verifikáció és mire van szükség.
A formális verifikáció általában egy program vagy algoritmus ellenőrzését jelenti egy másikkal.
Erre azért van szükség, hogy megbizonyosodjunk arról, hogy a program viselkedése megfelel a vártnak, továbbá a biztonságát is garantálja.
A formális verifikáció a legfőbb eszköz a sebezhetőségek keresésére és elhárítására: lehetővé teszi, hogy megtaláljuk az összes létező hibát és bugot a programban, vagy bizonyítsuk, hogy nincsenek.
Meg kell jegyezni, hogy bizonyos esetekben ez lehetetlen, mint például a 8 vezérlő problémája 1000 mezős táblán: itt az algoritmikus komplexitás vagy a megállás problémája jelent akadályt.
Mindazonáltal minden esetben három válasz közül az egyik fogunk kapni: a program helyes, helytelen, vagy a válasz kiszámítása nem sikerült.
Ha nem tudjuk megtalálni a választ, gyakran át lehet dolgozni a program zavaros részeit, csökkentve algoritmikus komplexitásukat, hogy konkrét választ kapjunk, igen vagy nem.
A formális verifikációt például a Windows magjában és a Darpa drón-operációs rendszereiben használják a maximális védelmi szint biztosítására.
Mi a Z3Prover-t fogjuk használni, amely egy nagyon hatékony eszköz a tételek automatikus bizonyítására és egyenletek megoldására.
A Z3 valóban egyenleteket old meg, és nem brute force módszerrel keresi az értékeiket.
Ez azt jelenti, hogy képes választ találni, még akkor is, ha a bemeneti lehetőségek kombinációja 10^100.
És ez csupán körülbelül egy tucat bemeneti argumentumot jelent, ami gyakorlatban gyakran előfordul.
A 8 vezérlő problémája (angol nyelvű forrásból ).
# 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 indítá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 vezérek problémája hasonlít egy programhoz, amely bemenetként a 8 vezérlő koordinátáit veszi, és megadja a választ, hogy a vezérek ütik-e egymást.
Ha a formális verifikáció segítségével kellene megoldanunk egy ilyen programot, akkor a feladat szempontjából csak egy lépést kellene tennünk, nevezetesen a program kódját átkonvertálni egy egyenletbe: ennek a lényege ugyanaz lenne, ha a program hibátlanul van megírva.
Szinte ugyanez történik a sebezhetőségek keresésekor is: csak a szükséges kimeneti feltételeket határozzuk meg, például az admin jelszót, az eredeti vagy visszafejtett kódot átkonvertáljuk a verifikációhoz kompatibilis egyenletekké, és ezután megkapjuk a választ, hogy milyen adatokat kell bemenetként megadnunk a cél eléréséhez.
Véleményem szerint a farkas, a kecske és a káposzta feladata még érdekesebb, mivel a megoldásához már sok (7) lépés szükséges.
Ha a vezérlő feladat a királynők esetén azzal lenne összehasonlítható, amikor egy GET vagy POST kéréssel be lehet jutni a szerverre, akkor a farkas, a kecske és a káposzta példája jóval bonyolultabb és elterjedtebb kategóriába tartozik, ahol a célokat csak több kérés következményeként lehet elérni.
Ez például összehasonlítható egy olyan forgatókönyvvel, ahol SQL injekciót kell találni, fájlt kell írni rajta, majd jogosultságokat kell növelni, és csak ezután szerezni meg a jelszót.
A feladat feltételei és megoldásaA farmernek át kell szállítania a farkast, a kecskét és a káposztát a folyón. A farmer egy csónakkal rendelkezik, amelybe rajta kívül csak egy objektum fér el. A farkas megeszi a kecskét, a kecske pedig megeszi a káposztát, ha a farmert a közelükben hagyja.
A megoldás az, hogy a 4. lépésben a farmernek vissza kell vinnie a kecskét.
Most lépjünk tovább a programozott megoldásra.
A farmert, a farkast, a kecskét és a káposztát 4 változóként határozzuk meg, amelyek csak 0 vagy 1 értéket vehetnek fel. A nulla azt jelenti, hogy a bal parton vannak, az egyes pedig, hogy a jobb parton.
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) ]
# Minden lény csak a bal (0) vagy a jobb oldalon (1) lehet minden állapotban
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 – ez a lépések száma, amely szükséges a megoldáshoz. Minden lépés a folyó, a csónak és az összes lény állapotát képviseli.
Jelenleg próbáljunk meg véletlenszerűen választani, és vegyünk 10-et.
Minden entitás 10 példányban van jelen — ez az értéke minden egyes lépésnél a 10-ből.
Most határozzuk meg a kezdeti és befejező feltételeket.
Kezdet = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ]
Befejezés = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]
Ezután állítsuk be a feltételeket, ahol a farkas megeszi a kecskét, vagy a kecske a káposztát, mint korlátozásokat az egyenletben.
(A gazda jelenlétében az agresszió nem lehetséges)
# 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 határozzuk meg az összes lehetséges cselekvést a gazda átkelése során oda-vissza.
Vihet magával farkast, kecskét vagy káposztát, vagy senkit, vagy pedig egyáltalán nem evez.
Nyilvánvaló, hogy gazda nélkül senki sem tud átkelni.
Ez kifejezésre kerül azzal, hogy a folyó, a csónak és az entitások következő állapota csak szigorúan korlátozott módon térhet el az előzőtől.
Legfeljebb 2 bit, és számos más korlátozással, mivel a gazda egyszerre csak egy entitást vihet át, és nem mindegyiket lehet együtt hagyni.
Utazás = [ Vagy(
És(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
És(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
És(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
És(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
És(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
És(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
És(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) for i in range(Num-1) ]
Indítsuk el a megoldást.
solve(Side + Start + Finish + Safe + Travel)
És megkapjuk a választ!
A Z3 konzisztenst talált, amely megfelel minden feltételnek.
Egyfajta négy dimenziós tér-idő lenyomat.
Nézzük meg, mi történt.
Látjuk, hogy végül mindenki átkelt, de először a gazdánk úgy döntött, hogy pihen, és az első 2 lépésben nem evez sehova.
Human_2 = 0
Human_3 = 0
Ez azt jelzi, hogy a választott állapotok száma túlzás, és a 8 teljesen elegendő lesz.
A mi esetünkben a gazda így járt el: indulás, pihenés, pihenés, kecske átkelése, vissza, káposzta átkelése, vissza kecskével, farkas átkelése, vissza egyedül, kecske újabb szállítása.
De a végeredmény a feladat megoldása.
#Старт.
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 bizonyítani, hogy nincs megoldás.
Ehhez a farkasunkat vegetáriánusnak nevezjük el, és megpróbálja megenni a káposztát.
Ez összehasonlítható azzal az esettel, amikor célunk az alkalmazás védelme, és meg kell győződnünk arról, hogy nincsenek rései.
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:
nincs megoldás
Ez azt jelenti, hogy valóban nincsenek megoldások.
Ezzel tehát programozott módon bizonyítottuk a mindenevő farkas átkelésének lehetetlenségét a gazda vesztesége nélkül.
Ha a közönség érdekesnek találja ezt a témát, a következő cikkekben elmondom, hogyan lehet egy szokásos programot vagy funkciót formális módszerekkel kompatibilissé alakítani, és megoldani azt, ezáltal felfedezve mind a legitim forgatókönyveket, mind a sérülékenységeket. Kezdetben ugyanazzal a feladattal, de már programformában bemutatva, majd fokozatosan nehezedve és átérve a szoftverfejlesztés világából származó aktuális példákra.
A következő cikk már elkészült:
Ebben átmegyek a feladatok formális ellenőrzéséről a programokra, és leírom,
hogyan lehet őket automatikusan formális szabályrendszerré alakítani.
Forrás: habr.com
