Podle mého názoru je v ruské části internetu téma formální verifikace nedostatečně pokryto, a zejména chybí jednoduché a názorné příklady.
Přivedu takový příklad z zahraničního zdroje a doplním svým vlastním řešením známého úkolu o přepravě vlka, kozy a zelí na druhou stranu řeky.
Ale nejprve stručně popíšu, co si formální verifikace představuje a proč je potřebná.
Pod formální verifikací se obvykle rozumí kontrola jednoho programu nebo algoritmu pomocí jiného.
To je nezbytné, abychom se ujistili, že chování programu odpovídá očekávanému, a také zajistili jeho bezpečnost.
Formální verifikace je nejmocnějším nástrojem pro hledání a odstraňování zranitelností: umožňuje nalézt všechny existující chyby a bugy v programu, nebo dokázat, že žádné nejsou.
Je třeba poznamenat, že v některých případech to může být nemožné, jako například v úloze o 8 dámách se šířkou desky 1000 polí: vše spočívá v algoritmické složitosti nebo problému zastavení.
Nicméně v každém případě bude získán jeden ze tří odpovědí: program je správný, nesprávný, nebo — výpočet odpovědi nebyl možný.
V případě nemožnosti nalezení odpovědi je často možné přepracovat nejasné části programu, čímž se sníží jejich algoritmická složitost, abychom získali konkrétní odpověď ano nebo ne.
Formální verifikace se používá například v jádru Windows a v operačních systémech bezpilotních letadel Darpa pro zajištění maximální úrovně ochrany.
Budeme používat Z3Prover, velmi mocný nástroj pro automatizované dokazování tvrzení a řešení rovnic.
Z3 totiž skutečně řeší rovnice, a ne hledá jejich hodnoty hrubým brute-forcem.
To znamená, že je schopen nalézt odpověď i v případech, kdy je kombinací vstupních variant 10^100.
A přitom jde jen o přibližně tucet vstupních argumentů typu Integer, a podobné se často v praxi vyskytují.
Úloha o 8 dámách (Vzato z anglicky ).
# 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)
Spuštěním Z3 získáme řešení:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Úloha o dámách je srovnatelná s programem, který bere jako vstup souřadnice 8 dam a vrací odpověď, zda se dámy navzájem zasahují.
Pokud bychom tento problém řešili pomocí formální verifikace, pak bychom oproti úkolu potřebovali pouze udělat ještě jeden krok, a to transformaci kódu programu na rovnici: ta by v zásadě vyšla stejná jako naše (samozřejmě pokud je program napsán bez chyb).
To samé se bude dít i při hledání zranitelností: pouze zadáme požadované výstupní podmínky, například heslo administrátora, převedeme zdrojový nebo dekompilovaný kód na rovnice kompatibilní s verifikací, a pak dostaneme odpověď na to, jaká data je třeba zadat jako vstup pro dosažení cíle.
Podle mého názoru je úkol o vlkovi, kozě a zelí ještě zajímavější, protože pro jeho řešení je potřeba už mnoho (7) kroků.
Pokud je úkol o dámě srovnatelný s variantou, kdy lze proniknout na server pomocí jediného GET nebo POST požadavku, pak vlk, koza a zelí demonstruje příklad z mnohem složitější a rozšířené kategorie, ve které lze cíl dosáhnout pouze několika požadavky.
To se dá přirovnat například ke scénáři, kdy je potřeba najít SQL injekci, přes ni zapsat soubor, poté zvýšit svá oprávnění a teprve pak získat heslo.
Podmínky úkolu a jeho rozluštěníFarmář musí převést přes řeku vlka, kozu a zelí. Farmář má loď, do které se vedle něj vejde pouze jeden objekt. Vlk sežere kozu a koza sežere zelí, pokud je farmář nechá bez dozoru.
Rozluštění spočívá v tom, že v 4. kroku bude muset farmář odvézt kozu zpět.
Nyní se pustíme do řešení programovým způsobem.
Označíme farmáře, vlka, kozu a zelí jako 4 proměnné, které mohou nabývat hodnotu pouze 0 nebo 1. Nula znamená, že jsou na levém břehu, a jednička, že jsou na pravém.
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) ]
# Každá bytost může být pouze na levé (0) nebo pravé straně (1) v každém stavu
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 — je počet kroků potřebných k řešení. Každý krok představuje stav řeky, lodi a všech entit.
Zatím zvolíme jeho náhodně a s rezervou, vezmeme 10.
Každá entita je představena ve 10 kopiích - to je její hodnota na každé z 10 úrovní.
Nyní nastavíme podmínky pro start a cíl.
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 ]
Poté nastavíme podmínky, kde vlk sežere kozu, nebo koza sežere kapustu, jako omezení v rovnici.
(V přítomnosti farmáře není agrese možná)
# 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) ]
A nakonec nastavíme všechny možné akce farmáře při přepravě tam nebo zpět.
Může buď vzít s sebou vlka, kozu nebo kapustu, nebo nikoho nebrat, nebo nikam neplout.
Samozřejmě, bez farmáře se nikdo přepravit nemůže.
To bude vyjádřeno tím, že každý následující stav řeky, lodi a entit může být od předchozího odlišný pouze striktně omezeným způsobem.
Ne více než o 2 bity, a s mnoha dalšími limity, protože farmář může přepravit najednou pouze jednu entitu a ne všechny je možné nechat spolu.
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) ]
Spusťme řešení.
solve(Side + Start + Finish + Safe + Travel)
A máme odpověď!
Z3 našel konzistentní, a všem podmínkám vyhovující soubor stavů.
Jakýsi čtyřrozměrný otisk prostoru-času.
Pojďme si objasnit, co se vlastně stalo.
Vidíme, že nakonec všichni přešli, jen na začátku se náš farmář rozhodl odpočinout a v prvních 2 krocích nikam nepluje.
Human_2 = 0
Human_3 = 0
To naznačuje, že jsme zvolili nadbytečný počet stavů, a 8 bude zcela dostačující.
V našem případě farmář postupoval takto: start, odpočinek, odpočinek, přeprava kozy, přeprava zpět, přeprava kapusty, návrat s kozou, přeprava vlka, návrat zpět osamoceně, opětovná přeprava kozy.
Ale nakonec byla úloha vyřešena.
#Старт.
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
Nyní se pokusíme změnit podmínky a dokázat, že řešení neexistuje.
Abychom toho dosáhli, obdaříme našeho vlka býložravostí, a on se pokusí sníst kapustu.
Tohoto lze přirovnat k situaci, kdy naší cílem je ochrana aplikace a musíme se ujistit, že zde nejsou žádné mezery.
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 nám dal následující odpověď:
žádné řešení
To znamená, že řešení skutečně neexistuje.
Tímto jsme programově dokázali, že přechod s všežravým vlkem je nemožný, aniž by farmer něco ztratil.
Pokud audience považuje toto téma za zajímavé, v dalších článcích povím, jak převést obyčejný program nebo funkci na rovnici kompatibilní s formálními metodami, a vyřešit ji, přičemž tím odhalím jak legitimizované scénáře, tak i zranitelnosti. Nejprve na stejné úloze, ale prezentované již jako program, a poté postupně zkomplikovat a přejít k aktuálním příkladům ze světa vývoje softwaru.
Další článek je již připraven:
V něm přecházím od formální verifikace úloh k programům a popisuji,
jak je možné je automaticky převádět na systémy formálních pravidel.
Zdroj: habr.com
