Podle mého názoru není v ruskojazyčném sektoru internetu téma formálního ověřování dostatečně pokryto a zejména chybí jednoduché a jasné příklady.
Uvedu příklad ze zahraničního zdroje a přidám vlastní řešení známého problému přechodu vlka, kozy a zelí na druhou stranu řeky.
Nejprve ale stručně popíšu, co je formální ověření a proč je potřeba.
Formální ověření obvykle znamená kontrolu jednoho programu nebo algoritmu pomocí jiného.
To je nezbytné pro zajištění toho, aby se program choval podle očekávání, a také pro zajištění jeho bezpečnosti.
Formální ověření je nejúčinnějším prostředkem k nalezení a odstranění zranitelných míst: umožňuje vám najít všechny existující díry a chyby v programu nebo prokázat, že neexistují.
Stojí za zmínku, že v některých případech je to nemožné, jako například v problému 8 dam s šířkou desky 1000 polí: to vše závisí na složitosti algoritmu nebo na problému zastavení.
V každém případě však obdržíte jednu ze tří odpovědí: program je správný, nesprávný nebo nebylo možné odpověď vypočítat.
Pokud není možné najít odpověď, je často možné přepracovat nejasné části programu, snížit jejich algoritmickou složitost, a získat tak konkrétní odpověď ano nebo ne.
A formální ověření se používá například v operačních systémech Windows kernel a Darpa drone, aby byla zajištěna maximální úroveň ochrany.
Použijeme Z3Prover, velmi výkonný nástroj pro automatizované dokazování vět a řešení rovnic.
Z3 navíc řeší rovnice a nevybírá jejich hodnoty pomocí hrubé síly.
To znamená, že je schopen najít odpověď i v případech, kdy existuje 10^100 kombinací vstupních možností.
Ale to je jen asi tucet vstupních argumentů typu Integer a v praxi se s tím často setkáváme.
Problém o 8 královnách (převzato z angl ).
# 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]
Problém královny je srovnatelný s programem, který bere jako vstup souřadnice 8 královen a vydává odpověď, zda se královny navzájem porazily.
Pokud bychom takový program řešili pomocí formální verifikace, pak bychom oproti problému jednoduše potřebovali udělat ještě jeden krok v podobě převodu programového kódu do rovnice: ukázalo by se, že je v podstatě identický s naším ( samozřejmě, pokud byl program napsán správně).
Téměř totéž se stane v případě hledání zranitelností: pouze nastavíme výstupní podmínky, které potřebujeme, například heslo správce, transformujeme zdrojový nebo dekompilovaný kód do rovnic kompatibilních s ověřením a poté dostaneme odpověď, co data je třeba dodat jako vstup pro dosažení cíle.
Podle mého názoru je problém s vlkem, kozou a zelí ještě zajímavější, protože jeho vyřešení již vyžaduje mnoho (7) kroků.
Pokud je problém královny srovnatelný s případem, kdy můžete proniknout na server pomocí jediného požadavku GET nebo POST, pak vlk, koza a zelí ukazuje příklad z mnohem složitější a rozšířenější kategorie, ve které lze cíle dosáhnout pouze několika žádostmi.
To je srovnatelné například se scénářem, kdy potřebujete najít SQL injekci, napsat přes něj soubor, poté povýšit svá práva a teprve poté získat heslo.
Podmínky problému a jeho řešeníFarmář potřebuje převézt vlka, kozu a zelí přes řeku. Farmář má loď, která pojme pouze jeden předmět, kromě samotného farmáře. Vlk sežere kozu a koza sežere zelí, pokud je farmář nechá bez dozoru.
Odpověď je, že v kroku 4 bude muset farmář vzít kozu zpět.
Nyní to začneme řešit programově.
Označme farmáře, vlka, kozu a zelí jako 4 proměnné, které mají hodnotu pouze 0 nebo 1. Nula znamená, že jsou na levém břehu a jedna znamená, ž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) ]
# 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 je počet kroků potřebných k vyřešení. Každý krok představuje stav řeky, lodi a všech entit.
Zatím to vyberme náhodně a s rezervou, vezměte 10.
Každá entita je zastoupena v 10 kopiích – toto je její hodnota v každém z 10 kroků.
Nyní si 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, kdy vlk žere kozu nebo koza žere zelí, jako omezení v rovnici.
(V přítomnosti farmáře je agrese nemož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 si nadefinujeme všechny možné akce farmáře při přejezdu tam nebo zpět.
Buď si s sebou může vzít vlka, kozu nebo zelí, nebo nebrat nikoho, nebo vůbec nikam nedoplout.
Samozřejmě, že nikdo nemůže přejít bez farmáře.
To bude vyjádřeno tím, že každý následující stav řeky, lodi a entit se může od předchozího lišit pouze přísně omezeným způsobem.
Ne více než 2 bity as mnoha dalšími limity, protože farmář může přepravovat pouze jednu entitu najednou a ne všechny mohou zůstat pohromadě.
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) ]
Spustíme řešení.
solve(Side + Start + Finish + Safe + Travel)
A dostáváme odpověď!
Z3 našel konzistentní sadu stavů, která splňuje všechny podmínky.
Jakési čtyřrozměrné obsazení časoprostoru.
Pojďme zjistit, co se stalo.
Vidíme, že nakonec přešli všichni, jen náš farmář se nejprve rozhodl odpočívat a v prvních 2 krocích nikam neplave.
Human_2 = 0
Human_3 = 0
To naznačuje, že počet států, které jsme zvolili, je přehnaný a 8 bude zcela dostačujících.
V našem případě farmář udělal toto: začít, odpočívat, odpočívat, přejít kozu, přejít zpět, přejít zelí, vrátit se s kozou, přejít vlka, vrátit se sám, znovu doručit kozu.
Ale nakonec byl problém vyřešen.
#Старт.
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í zkusme změnit podmínky a dokázat, že řešení neexistují.
K tomu dáme našemu vlkovi býložravost a on bude chtít jíst zelí.
Dá se to přirovnat k případu, kdy je naším cílem zabezpečit aplikaci a musíme se ujistit, že neexistují žá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ěď:
no solution
To znamená, že ve skutečnosti neexistují žádná řešení.
Programově jsme tak prokázali nemožnost křížení s všežravým vlkem bez ztrát pro farmáře.
Pokud bude toto téma pro diváky zajímavé, pak vám v budoucích článcích řeknu, jak z obyčejného programu nebo funkce udělat rovnici kompatibilní s formálními metodami a vyřešit ji, čímž odhalím všechny legitimní scénáře i zranitelnosti. Nejprve na stejném úkolu, ale prezentovaném formou programu a následně jej postupně komplikovat a přecházet na aktuální příklady ze světa vývoje softwaru.
Další článek je již připraven:
V něm přecházím od formálního ověřování problémů k programům a popisuji
jak je můžete automaticky převést na systémy formálních pravidel.
Zdroj: www.habr.com