Podľa môjho názoru je téma formálnej verifikácie v ruskojazyčnej časti internetu nedostatočne pokrytá a najmä chýbajú jednoduché a názorné príklady.
Uvediem taký príklad zo zahraničného zdroja a doplním vlastným riešením známej úlohy o preprave vlka, kozy a kapusty na druhú stranu rieky.
Ale najprv stručne opíšem, čo formálna verifikácia predstavuje a na čo je potrebná.
Formálna verifikácia sa obvykle chápe ako kontrola jedného programu alebo algoritmu pomocou iného.
Je to potrebné na to, aby sme sa uistili, že správanie programu zodpovedá očakávaniam a tiež zabezpečili jeho bezpečnosť.
Formálna verifikácia je najúčinnejším prostriedkom na vyhľadávanie a odstránenie zraniteľností: umožňuje nájsť všetky existujúce nedostatky a bugy v programe alebo dokázať, že neexistujú.
Je potrebné poznamenať, že v niektorých prípadoch to môže byť nemožné, ako napríklad v úlohe o 8 dámach s šírkou dosky 1000 polí: všetko závisí od algoritmickej náročnosti alebo problému zastavenia.
V každom prípade bude získaný jeden z troch odpovedí: program je korektný, nekorektný alebo sa odpoveď získať nepodarilo.
V prípade nemožnosti nájsť odpoveď je často možné prepracovať nejasné časti programu, znížením ich algoritmickej náročnosti, aby sa dosiahla konkrétna odpoveď áno alebo nie.
Formálna verifikácia sa používa napríklad v jadre Windows a v operačných systémoch bezpilotných lietadiel Darpa, na zabezpečenie maximálnej úrovne ochrany.
Budeme používať Z3Prover, veľmi mocný nástroj na automatizované dokazovanie teórií a riešenie rovníc.
Z3 totiž rieši rovnice, a nie len odhaduje ich hodnoty hrubým brutálnym spôsobom.
To znamená, že dokáže nájsť odpoveď, aj v prípadoch, keď kombinácií vstupných možností je 10^100.
A veď to je len okolo tucta vstupných argumentov typu Integer, a takéto situácie sa často vyskytujú v praxi.
Úloha o 8 dámach (Vzata z anglického ).
# 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 dostávame 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]
Úloha o dámach je porovnateľná s programom, ktorý prijíma súradnice 8 dám a vyhodnocuje, či sa dámy navzájom ohrozujú.
Ak by sme túto úlohu riešili pomocou formálnej verifikácie, v porovnaní s úlohou by sme museli spraviť iba jeden ďalší krok, a to prekonvertovať kód programu na rovnicu: tá by bola v podstate identická s našou (samozrejme, ak je program napísaný bez chýb).
Takmer to isté sa bude diať aj pri hľadaní zraniteľností: jednoducho zadáme požadované výstupné podmienky, napríklad administrátorské heslo, prekonvertujeme pôvodný alebo dekompilovaný kód na so verifikáciou kompatibilné rovnice a potom dostaneme odpoveď, aké údaje treba poskytnúť ako vstup na dosiahnutie cieľa.
Podľa môjho názoru je úloha o vlkovi, koze a kapuste ešte zaujímavejšia, pretože na jej vyriešenie je potrebných už veľa (7) krokov.
Ak je úloha o dámach porovnateľná s variantom, kde sa môžeme dostať na server s jediným GET alebo POST požiadavkou, tak úloha o vlkovi, koze a kapuste ukazuje príklad z oveľa zložitejšej a rozšírenejšej kategórie, v ktorej je možné dosiahnuť ciele iba niekoľkými požiadavkami.
Je to porovnateľné napríklad so scénárom, kde treba nájsť SQL injekciu, zapísať cez ňu súbor, potom zvýšiť svoje práva a až potom získať heslo.
Podmienky úlohy a jej riešenieFarmárovi je potrebné prepraviť cez rieku vlka, kozu a kapustu. Farmár má loď, do ktorej sa môže zmestiť, okrem samého farmára, len jeden objekt. Vlk zje kozu, a koza zje kapustu, ak ju farmár nechá bez dohľadu.
Riešenie spočíva v tom, že na 4. kroku farmár vracia kozu späť.
Teraz prejdeme k riešeniu programovým spôsobom.
Označíme farmára, vlka, kozu a kapustu ako 4 premenné, ktoré môžu nadobúdať hodnotu iba 0 alebo 1. Nula znamená, že sú na ľavom brehu, a jedna, že sú na pravom.
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ý tvor môže byť iba na ľavej (0) alebo pravej strane (1) v každom stave
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, člna a všetkých entít.
Doteraz si ho vyberieme náhodne a s rezervou, vezmeme 10.
Každá entita je zastúpená v 10 exemplároch — to je jej hodnota na každom z 10 krokov.
Teraz nastavíme 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, kde vlk zož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, nastavíme všetky možné akcie farmára pri preprave tam alebo späť.
Môže si vziať so sebou vlka, kozu alebo kapustu, alebo nikoho nevziať, alebo vôbec nikam neplávať.
Samozrejme, bez farmára sa nikto nemôže prepraviť.
To sa vyjadrí tým, že každý nasledujúci stav rieky, člna a entít sa môže líšiť od predchádzajúceho iba striktne obmedzeným spôsobom.
Nie viac ako o 2 bity, a so množstvom ďalších limitov, pretože farmár môže za raz previezť len jednu entitu a nie všetkých je možné nechať 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 nezrozumiteľnú, a uspokojivú všetkým podmienkam sústavu stavov.
Akýsi štvordimenzionálny odtlačok priestoru- času.
Poďme sa pozrieť, čo sa vlastne stalo.
Vidíme, že nakoniec sa všetci prepravili, len na začiatku sa náš farmár rozhodol oddychovať a v prvých 2 krokoch nikam nepláva.
Human_2 = 0
Human_3 = 0
To naznačuje, že sme zvolili nadbytočný počet stavov, a 8 bude úplne postačovať.
V našom prípade farmár postupoval takto: štart, oddych, oddych, preprava kozy, preprava späť, preprava kapusty, návrat s kozou, preprava vlka, návrat späť osamote, opätovná dodávka kozy.
Ale nakoniec je úloha vyrieš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
Teraz sa pokúsime zmeniť podmienky a dokázať, že neexistujú žiadne riešenia.
Za týmto účelom obdaríme nášho vlka bylinožravosťou, a ten sa bude chcieť najesť kapusty.
Toto možno porovnať so situáciou, kde náš cieľ je ochrana aplikácie a musíme sa uistiť, že nie sú žiadne diery.
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 poskytol nasledujúcu odpoveď:
žiadne riešenie
To znamená, že naozaj neexistujú žiadne riešenia.
Týmto spôsobom sme programovo dokázali nemožnosť prepravy s mäsožravým vlkom, bez strát pre poľnohospodára.
Ak si publikum považuje túto tému za zaujímavú, v ďalších článkoch vám poviem, ako premeniť obyčajný program alebo funkciu na kompatibilné s formálnymi metódami rovnice a vyriešiť ju, čím objavíme ako legálne scenáre, tak aj zraniteľnosti. Najprv na tej istej úlohe, ale predstavené už vo forme programu, a potom postupne komplikujúc a prechádzajúc k aktuálnym príkladom zo sveta softvérového vývoja.
Ďalší článok je už pripravený:
V ňom prechádzam od formálnej verifikácie úloh k programom a popisujem,
akým spôsobom možno automaticky konvertovať ich na systémy formálnych pravidiel.
Zdroj: habr.com
