În opinia mea, în sectorul de limbă rusă al internetului, subiectul verificării oficiale nu este suficient acoperit și există în special o lipsă de exemple simple și clare.
Voi da un exemplu dintr-o sursă străină și voi adăuga propria mea soluție la binecunoscuta problemă a trecerii unui lup, o capră și o varză pe malul celălalt al râului.
Dar mai întâi, voi descrie pe scurt ce este verificarea formală și de ce este necesară.
Verificarea formală înseamnă de obicei verificarea unui program sau algoritm folosind altul.
Acest lucru este necesar pentru a ne asigura că programul se comportă conform așteptărilor și, de asemenea, pentru a asigura securitatea acestuia.
Verificarea formală este cel mai puternic mijloc de găsire și eliminare a vulnerabilităților: vă permite să găsiți toate găurile și erorile existente într-un program sau să demonstrați că acestea nu există.
Este de remarcat faptul că în unele cazuri acest lucru este imposibil, cum ar fi în problema celor 8 dame cu o lățime de tablă de 1000 de pătrate: totul se reduce la complexitatea algoritmică sau la problema opririi.
Cu toate acestea, în orice caz, va fi primit unul dintre cele trei răspunsuri: programul este corect, incorect sau nu a fost posibil să se calculeze răspunsul.
Dacă este imposibil să găsiți un răspuns, este adesea posibil să reluați părți neclare ale programului, reducându-le complexitatea algoritmică, pentru a obține un răspuns specific da sau nu.
Iar verificarea formală este folosită, de exemplu, în kernel-ul Windows și sistemele de operare pentru drone Darpa, pentru a asigura nivelul maxim de protecție.
Vom folosi Z3Prover, un instrument foarte puternic pentru demonstrarea automată a teoremelor și rezolvarea ecuațiilor.
Mai mult, Z3 rezolvă ecuații și nu le selectează valorile folosind forța brută.
Aceasta înseamnă că este capabil să găsească răspunsul, chiar și în cazurile în care există 10^100 de combinații de opțiuni de intrare.
Dar acesta este doar aproximativ o duzină de argumente de intrare de tip Integer și acest lucru este adesea întâlnit în practică.
Problemă despre 8 regine (luat din 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)
Rulând 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 matcilor este comparabilă cu un program care ia ca intrare coordonatele a 8 matci și dă răspunsul dacă mătcile se bat între ele.
Dacă ar fi să rezolvăm un astfel de program utilizând verificarea formală, atunci, în comparație cu problema, ar trebui pur și simplu să mai facem un pas sub forma conversiei codului programului într-o ecuație: s-ar dovedi a fi în esență identic cu al nostru ( desigur, dacă programul a fost scris corect).
Aproape același lucru se va întâmpla în cazul căutării vulnerabilităților: doar setăm condițiile de ieșire de care avem nevoie, de exemplu, parola de administrator, transformăm codul sursă sau decompilat în ecuații compatibile cu verificarea și apoi obținem un răspuns despre ce datele trebuie furnizate ca intrare pentru a atinge obiectivul.
După părerea mea, problema lupului, caprei și varzei este și mai interesantă, deoarece rezolvarea ei necesită deja mulți (7) pași.
Dacă problema reginei este comparabilă cu cazul în care poți pătrunde un server cu o singură cerere GET sau POST, atunci lupul, capra și varza demonstrează un exemplu dintr-o categorie mult mai complexă și mai răspândită, în care scopul poate fi atins doar prin mai multe cereri.
Acest lucru este comparabil, de exemplu, cu un scenariu în care trebuie să găsiți o injecție SQL, să scrieți un fișier prin ea, apoi să vă ridicați drepturile și abia apoi să obțineți o parolă.
Condițiile problemei și soluționarea acesteiaFermierul trebuie să transporte un lup, o capră și varză peste râu. Fermierul are o barcă care poate găzdui un singur obiect, în afară de fermierul însuși. Lupul va mânca capra, iar capra va mânca varza dacă fermierul le lasă nesupravegheate.
Soluția este că la pasul 4 fermierul va trebui să ia capra înapoi.
Acum să începem să o rezolvăm programatic.
Să notăm fermierul, lupul, capra și varza ca 4 variabile care iau valoarea doar 0 sau 1. Zero înseamnă că sunt pe malul stâng, iar unul înseamnă că sunt pe dreapta.
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 este numărul de pași necesari pentru rezolvare. Fiecare pas reprezintă starea râului, a bărcii și a tuturor entităților.
Deocamdată, să-l alegem la întâmplare și cu o marjă, luăm 10.
Fiecare entitate este reprezentată în 10 copii - aceasta este valoarea sa la fiecare dintre cei 10 pași.
Acum să stabilim condițiile pentru început și sfârșit.
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 stabilim condițiile în care lupul mănâncă capra, sau capra mănâncă varza, ca constrângeri în ecuație.
(În prezența unui fermier, 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, vom defini toate acțiunile posibile ale fermierului atunci când traversează acolo sau înapoi.
Poate fie să ia cu el un lup, o capră sau o varză, fie să nu ia pe nimeni, fie să nu navigheze nicăieri.
Desigur, nimeni nu poate traversa fără fermier.
Acest lucru va fi exprimat prin faptul că fiecare stare ulterioară a râului, ambarcațiunii și entităților poate diferi de cea anterioară doar într-un mod strict limitat.
Nu mai mult de 2 biți și cu multe alte limite, deoarece fermierul poate transporta doar o entitate la un moment dat și nu pot fi lăsate toate î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ă rulăm soluția.
solve(Side + Start + Finish + Safe + Travel)
Și primim răspunsul!
Z3 a găsit un set consistent de stări care satisface toate condițiile.
Un fel de distribuție cu patru dimensiuni a spațiu-timpului.
Să ne dăm seama ce s-a întâmplat.
Vedem ca pana la urma toata lumea a traversat, doar la inceput fermierul nostru a decis sa se odihneasca, iar in primii 2 pasi nu inoata nicaieri.
Human_2 = 0
Human_3 = 0
Acest lucru sugerează că numărul de state pe care le-am ales este excesiv și 8 va fi destul de suficient.
În cazul nostru, fermierul a făcut așa: începe, odihnește, odihnește, încrucișează capra, traversează înapoi, traversează varza, se întorc cu capra, traversează lupul, se întorc singur înapoi, preda din nou capra.
Dar până la 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ă dovedim că nu există soluții.
Pentru a face acest lucru, îi vom oferi lupului nostru erbivor, iar el va dori să mănânce varză.
Acest lucru poate fi comparat cu cazul în care scopul nostru este să securizăm aplicația și trebuie să ne asigurăm că nu există lacune.
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:
no solution
Înseamnă că într-adevăr nu există soluții.
Astfel, am demonstrat programatic imposibilitatea încrucișării cu un lup omnivor fără pierderi pentru fermier.
Dacă publicul consideră acest subiect interesant, atunci în articolele viitoare vă voi spune cum să transformați un program sau o funcție obișnuită într-o ecuație compatibilă cu metodele formale și să o rezolvați, dezvăluind astfel atât toate scenariile legitime, cât și vulnerabilitățile. Mai întâi, pe aceeași sarcină, dar prezentată sub forma unui program, apoi complicând treptat și trecând la exemplele actuale din lumea dezvoltării software.
Următorul articol este deja gata:
În ea trec de la verificarea formală a problemelor la programe și descriu
cum pot fi convertite automat în sisteme de reguli formale.
Sursa: www.habr.com