În opinia mea, în sectorul de limbă rusă al internetului, tema verificării formale este insuficient acoperită, și mai ales lipsesc exemple simple și clare.
Voi aduce un exemplu dintr-o sursă străină și voi completa cu propria soluție pentru problema cunoscută a transportului lupului, caprei și verzei pe cealaltă parte a râului.
Dar mai întâi voi descrie pe scurt ce reprezintă verificarea formală și de ce este nevoie de ea.
Prin verificarea formală se înțelege de obicei verificarea unei programe sau algoritm cu ajutorul altuia.
Acest lucru este necesar pentru a ne asigura că comportamentul programului corespunde așteptărilor și pentru a-i asigura securitatea.
Verificarea formală este cel mai puternic instrument pentru identificarea și eliminarea vulnerabilităților: permite găsirea tuturor scurgerilor și bug-urilor din program, sau dovedirea faptului că acestea nu există.
Este important de menționat că în unele cazuri acest lucru este imposibil, cum ar fi în problema celor 8 regine cu o latură de tablă de 1000 de pătrate: totul se reducem la complexitatea algoritmică sau la problema opririi.
Cu toate acestea, în orice caz se va obține una dintre cele trei răspunsuri: programul este corect, incorect sau nu a fost posibilă calcularea răspunsului.
În caz de imposibilitate de a găsi un răspuns, de multe ori este posibil să se refacă părțile neclare ale programului, reducându-le complexitatea algoritmică, pentru a obține un răspuns concret, da sau nu.
Verificarea formală este utilizată, de exemplu, în nucleul Windows și în sistemele de operare ale dronelor Darpa, pentru a asigura cel mai înalt nivel de protecție.
Vom folosi Z3Prover, un instrument foarte puternic pentru dovedirea automată a teoremelor și rezolvarea ecuațiilor.
Și Z3, de fapt, rezolvă ecuații, nu le caută valorile prin brute force.
Aceasta înseamnă că este capabil să găsească un răspuns, chiar și în cazurile când combinațiile de variante de intrare sunt de 10^100.
Și aceasta este doar o duzină de argumente de intrare de tip Integer, iar astfel de situații sunt adesea întâlnite în practică.
Problema celor 8 regine (Preluată din manualul în limba engleză ).
# 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)
După ce am pornit Z3, obținem soluția:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Problema reginelor este comparabilă cu un program care primește coordonatele celor 8 regine ca intrare și returnează un răspuns dacă reginele se atacă între ele.
Dacă am rezolva un astfel de program prin verificare formală, în comparație cu problema, ar trebui doar să facem un pas în plus prin transformarea codului programului într-o ecuație: aceasta ar fi în esență identică cu a noastră (desigur, dacă programul este scris fără erori).
Practic același lucru se va întâmpla în cazul căutării vulnerabilităților: trebuie doar să stabilim condițiile de ieșire dorite, de exemplu, parola administratorului, transformăm codul sursă sau decompilat în ecuații compatibile cu verificarea și apoi obținem răspunsul la ce date trebuie furnizate ca intrare pentru a atinge scopul.
Din punctul meu de vedere, problema lupului, caprei și verzei este și mai interesantă, deoarece pentru a o rezolva sunt necesari deja mulți (7) pași.
Dacă problema reginelor este comparabilă cu situația în care poți pătrunde pe server cu o singură cerere GET sau POST, atunci lupul, capra și varza demonstrează un exemplu dintr-o categorie mult mai complexă și mai comună, în care scopurile pot fi atinse doar prin câteva cereri.
Aceasta este comparabilă, de exemplu, cu un scenariu în care trebuie să găsești o injecție SQL, să scrii un fișier prin ea, apoi să îți crești privilegiile și abia apoi să obții parola.
Condițiile problemei și soluția acesteiaFerma trebuie să transporte prin râu lupul, capra și varza. Fermierul are o barcă în care poate încăpea, în afară de el, doar un singur obiect. Lupul va mânca capra, iar capra va mânca varza dacă fermierul le lasă nesupravegheate.
Soluția constă în faptul că în pasul 4 fermierul va trebui să aducă capra înapoi.
Acum vom începe să rezolvăm prin metode programatice.
Să notăm fermierul, lupul, capra și varza ca 4 variabile, care pot lua doar valoarea 0 sau 1. Zero înseamnă că se află pe malul stâng, iar unu că pe malul drept.
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) ]
# Fiecare creatură poate fi doar pe malul stâng (0) sau pe malul drept (1) în fiecare stare
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 — este numărul de pași necesari pentru soluționare. Fiecare pas reprezintă o stare a râului, bărcii și a tuturor entităților.
Pentru început, să-l alegem la întâmplare și cu un surplus, să luăm 10.
Fiecare entitate este reprezentată în 10 exemplare — aceasta este valoarea sa la fiecare dintre cele 10 etape.
Acum să stabilim condițiile pentru start și finish.
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 ]
Apoi, vom stabili condițiile în care lupul mănâncă capra, sau capra mănâncă varza, ca restricții în ecuație.
(În prezența fermierului, agresiunea este imposibilă)
# 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) ]
Și, în final, să stabilim toate acțiunile posibile ale fermierului la traversare înainte sau înapoi.
El poate lua cu sine fie lupul, capra sau varza, fie să nu ia pe nimeni, fie să nu navigheze deloc.
Desigur, fără fermier, nimeni nu poate traversa.
Aceasta va fi exprimată prin faptul că fiecare următor stadiu al râului, bărcii și entităților poate diferi de precedentul doar într-un mod strict limitat.
Nu mai mult de 2 biți, și cu multe alte limite, deoarece fermierul poate transporta o singură entitate deodată, iar nu toate pot fi lăsate împreună.
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) ]
Să lansăm soluția.
solve(Side + Start + Finish + Safe + Travel)
Și obținem răspunsul!
Z3 a găsit o colecție de stări consistentă, care satisface toate condițiile.
O așa-numită amprentă patru-dimensională a spațiu-timpului.
Hai să vedem ce s-a întâmplat.
Observăm că, în cele din urmă, toți au traversat, doar că la început fermierul nostru a decis să se odihnească și nu a navigat deloc în primele 2 pași.
Human_2 = 0
Human_3 = 0
Aceasta indică faptul că numărul stărilor pe care le-am ales este excesiv, iar 8 va fi suficient.
În cazul nostru, fermierul a procedat astfel: start, odihnă, odihnă, traversare caprei, revenire, traversare verzei, întoarcere cu capra, traversare lupului, revenire singur, livrarea repetată a caprei.
Dar, în cele din urmă, problema a fost rezolvată.
#Старт.
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
Acum să încercăm să schimbăm condițiile și să demonstrăm că nu există soluții.
Pentru aceasta, vom dota lupul nostru cu erbivorism și va dori să mănânce varza.
Acest lucru poate fi comparat cu o situație în care obiectivul nostru este protecția aplicației și trebuie să ne asigurăm că nu există breșe.
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 ne-a dat următorul răspuns:
nu există soluție
Aceasta înseamnă că nu există într-adevăr soluții.
Astfel, am demonstrat programatic imposibilitatea transportului cu un lup omnivor, fără pierderi pentru fermier.
Dacă publicul consideră că acest subiect este interesant, în articolele viitoare voi explica cum să transformi un program sau o funcție obișnuită într-o ecuație compatibilă cu metodele formale și să o rezolvi, descoperind astfel atât scenariile legitime, cât și vulnerabilitățile. Mai întâi, pe aceeași problemă, dar prezentată deja sub formă de program, și apoi treptat complicând și trecând la exemple relevante din lumea dezvoltării software.
Articolul următor este deja pregătit:
În acesta trec de la verificarea formală a problemelor, la programe și descriu,
în ce mod pot fi convertite automat în sisteme de reguli formale.
Sursa: habr.com
