Podľa môjho názoru nie je v ruskojazyčnom sektore internetu téma formálneho overovania dostatočne pokrytá a chýbajú najmä jednoduché a jasné príklady.
Uvediem príklad zo zahraničného zdroja a pridám vlastné riešenie známeho problému prechodu vlka, kozy a kapusty na druhú stranu rieky.
Najprv však stručne popíšem, čo je formálne overenie a prečo je potrebné.
Formálne overenie zvyčajne znamená kontrolu jedného programu alebo algoritmu pomocou iného.
Je to potrebné, aby sa zabezpečilo, že sa program bude správať podľa očakávania a tiež bude zabezpečená jeho bezpečnosť.
Formálne overenie je najúčinnejším prostriedkom na nájdenie a odstránenie slabých miest: umožňuje vám nájsť všetky existujúce diery a chyby v programe alebo dokázať, že neexistujú.
Stojí za zmienku, že v niektorých prípadoch je to nemožné, ako napríklad v prípade 8 dám so šírkou dosky 1000 políčok: všetko závisí od algoritmickej zložitosti alebo problému zastavenia.
V každom prípade však dostanete jednu z troch odpovedí: program je správny, nesprávny alebo nebolo možné odpoveď vypočítať.
Ak nie je možné nájsť odpoveď, často je možné prepracovať nejasné časti programu, čím sa zníži ich algoritmická zložitosť, s cieľom získať konkrétnu odpoveď áno alebo nie.
A formálne overenie sa používa napríklad v operačnom systéme Windows kernel a drone Darpa, aby sa zabezpečila maximálna úroveň ochrany.
Použijeme Z3Prover, veľmi výkonný nástroj na automatizované dokazovanie viet a riešenie rovníc.
Okrem toho Z3 rieši rovnice a nevyberá ich hodnoty pomocou hrubej sily.
To znamená, že je schopný nájsť odpoveď aj v prípadoch, keď existuje 10^100 kombinácií vstupných možností.
Ale to je len asi tucet vstupných argumentov typu Integer a v praxi sa s tým často stretávame.
Problém o 8 kráľovnách (Prevzaté z angličtiny ).
# 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)
Spustením Z3 dostaneme riešenie:
[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 s dámou je porovnateľný s programom, ktorý berie ako vstup súradnice 8 dám a dáva odpoveď, či sa dámy navzájom porazili.
Ak by sme takýto program riešili pomocou formálnej verifikácie, tak v porovnaní s problémom by sme jednoducho potrebovali urobiť ešte jeden krok v podobe prevodu programového kódu na rovnicu: ukázalo by sa, že je v podstate identický s naším ( samozrejme, ak bol program napísaný správne).
Takmer to isté sa stane v prípade hľadania zraniteľností: len nastavíme výstupné podmienky, ktoré potrebujeme, napríklad heslo správcu, transformujeme zdrojový alebo dekompilovaný kód do rovníc kompatibilných s overením a potom dostaneme odpoveď, čo údaje je potrebné dodať ako vstup na dosiahnutie cieľa.
Problém s vlkom, kozou a kapustou je podľa mňa ešte zaujímavejší, keďže jeho vyriešenie si už vyžaduje veľa (7) krokov.
Ak je problém kráľovnej porovnateľný s prípadom, keď môžete preniknúť na server pomocou jedinej požiadavky GET alebo POST, potom vlk, koza a kapusta demonštruje príklad z oveľa zložitejšej a rozšírenejšej kategórie, v ktorej sa cieľ dá dosiahnuť iba niekoľkými žiadosťami.
Je to porovnateľné napríklad so scenárom, keď potrebujete nájsť injekciu SQL, napísať cez ňu súbor, potom povýšiť svoje práva a až potom získať heslo.
Podmienky problému a jeho riešenieFarmár potrebuje previezť cez rieku vlka, kozu a kapustu. Farmár má loď, do ktorej sa okrem farmára zmestí len jeden predmet. Vlk zožerie kozu a koza kapustu, ak ich farmár nechá bez dozoru.
Riešením je, že v kroku 4 bude musieť farmár vziať kozu späť.
Teraz to začneme riešiť programovo.
Označme farmára, vlka, kozu a kapustu ako 4 premenné, ktoré majú hodnotu len 0 alebo 1. Nula znamená, že sú na ľavom brehu a jedna znamená, že sú na pravom brehu.
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 krokov potrebných na vyriešenie. Každý krok predstavuje stav rieky, lode a všetkých entít.
Zatiaľ to vyberieme náhodne a s rezervou, vezmime 10.
Každá entita je zastúpená v 10 kópiách – toto je jej hodnota v každom z 10 krokov.
Teraz si stanovme podmienky pre štart a cieľ.
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 ]
Potom nastavíme podmienky, kedy vlk žerie kozu alebo koza kapustu, ako obmedzenia v rovnici.
(V prítomnosti farmára je agresia 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 nakoniec si zadefinujeme všetky možné akcie farmára pri prechode tam alebo späť.
Buď si môže vziať so sebou vlka, kozu alebo kapustu, alebo nebrať nikoho, alebo sa vôbec nikam nedoplaviť.
Samozrejme, nikto nemôže prejsť bez farmára.
To bude vyjadrené skutočnosťou, že každý nasledujúci stav rieky, lode a entít sa môže líšiť od predchádzajúceho iba striktne obmedzeným spôsobom.
Nie viac ako 2 bity as mnohými ďalšími limitmi, pretože farmár môže prepravovať iba jednu entitu naraz a nie všetky môžu zostať 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) ]
Spustíme riešenie.
solve(Side + Start + Finish + Safe + Travel)
A dostaneme odpoveď!
Z3 našiel konzistentný súbor stavov, ktorý spĺňa všetky podmienky.
Akýsi štvorrozmerný odliatok časopriestoru.
Poďme zistiť, čo sa stalo.
Vidíme, že nakoniec prešli všetci, len náš farmár sa najprv rozhodol oddychovať a v prvých 2 krokoch nikam nepláva.
Human_2 = 0
Human_3 = 0
To naznačuje, že počet štátov, ktoré sme si vybrali, je nadmerný a 8 bude úplne postačujúcich.
V našom prípade farmár urobil toto: naštartovať, odpočívať, odpočívať, prejsť cez kozu, prejsť späť, prejsť cez kapustu, vrátiť sa s kozou, prejsť vlka, vrátiť sa sám, znova doručiť kozu.
Ale nakoniec sa problém vyriešil.
#Старт.
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
Teraz skúsme zmeniť podmienky a dokázať, že riešenia neexistujú.
K tomu dáme nášmu vlkovi bylinožravosť a on bude chcieť jesť kapustu.
Dá sa to prirovnať k prípadu, v ktorom je naším cieľom zabezpečiť aplikáciu a musíme sa uistiť, že neexistujú žiadne medzery.
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 nasledujúcu odpoveď:
no solution
To znamená, že v skutočnosti neexistujú žiadne riešenia.
Tým sme programovo dokázali nemožnosť kríženia so všežravým vlkom bez strát pre farmára.
Ak bude táto téma pre divákov zaujímavá, v budúcich článkoch vám poviem, ako premeniť obyčajný program alebo funkciu na rovnicu kompatibilnú s formálnymi metódami a vyriešiť ju, čím odhalím všetky legitímne scenáre a zraniteľné miesta. Najprv na tú istú úlohu, ale prezentovanú vo forme programu, a potom ju postupne komplikovať a prejsť na aktuálne príklady zo sveta vývoja softvéru.
Ďalší článok je už pripravený:
V nej prechádzam od formálneho overovania problémov k programom a popisujem
ako ich možno automaticky previesť na systémy formálnych pravidiel.
Zdroj: hab.com