Efter min mening er emnet formel verifikation ikke dækket tilstrækkeligt i den russisksprogede sektor af internettet, og der mangler især enkle og klare eksempler.
Jeg vil give et eksempel fra en udenlandsk kilde og tilføje min egen løsning på det velkendte problem med at krydse en ulv, en ged og en kål til den anden side af floden.
Men først vil jeg kort beskrive, hvad formel verifikation er, og hvorfor det er nødvendigt.
Formel verifikation betyder normalt at kontrollere et program eller en algoritme ved hjælp af et andet.
Dette er nødvendigt for at sikre, at programmet opfører sig som forventet, og også for at sikre dets sikkerhed.
Formel verifikation er det mest kraftfulde middel til at finde og eliminere sårbarheder: det giver dig mulighed for at finde alle eksisterende huller og fejl i et program eller bevise, at de ikke eksisterer.
Det er værd at bemærke, at i nogle tilfælde er dette umuligt, såsom i problemet med 8 dronninger med en brætbredde på 1000 felter: det hele kommer ned til algoritmisk kompleksitet eller stopproblemet.
Men under alle omstændigheder vil et af tre svar blive modtaget: programmet er korrekt, forkert, eller det var ikke muligt at beregne svaret.
Hvis det er umuligt at finde et svar, er det ofte muligt at omarbejde uklare dele af programmet, hvilket reducerer deres algoritmiske kompleksitet, for at få et specifikt ja eller nej svar.
Og formel verifikation bruges for eksempel i Windows-kernen og Darpa drone-operativsystemerne for at sikre det maksimale beskyttelsesniveau.
Vi vil bruge Z3Prover, et meget kraftfuldt værktøj til automatiseret teorembevis og ligningsløsning.
Desuden løser Z3 ligninger og vælger ikke deres værdier ved hjælp af brute force.
Det betyder, at den er i stand til at finde svaret, selv i tilfælde, hvor der er 10^100 kombinationer af inputmuligheder.
Men dette er kun omkring et dusin input-argumenter af typen Integer, og dette støder man ofte på i praksis.
Opgave om 8 dronninger (Tattet fra engelsk ).
# 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)
Ved at køre Z3 får vi løsningen:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Dronningproblemet kan sammenlignes med et program, der tager koordinaterne for 8 dronninger som input og udsender svaret, om dronningerne slår hinanden.
Hvis vi skulle løse et sådant program ved hjælp af formel verifikation, ville vi i forhold til problemet simpelthen være nødt til at tage et skridt mere i form af at konvertere programkoden til en ligning: den ville vise sig at være i det væsentlige identisk med vores ( selvfølgelig, hvis programmet er skrevet korrekt).
Næsten det samme vil ske i tilfælde af søgning efter sårbarheder: vi indstiller bare de outputbetingelser, vi har brug for, for eksempel admin-adgangskoden, transformerer kildekoden eller dekompilerede kode til ligninger, der er kompatible med verifikation, og får så svar på, hvad data skal leveres som input for at nå målet.
Efter min mening er problemet med ulven, geden og kålen endnu mere interessant, da løsningen af det allerede kræver mange (7) trin.
Hvis dronningeproblemet kan sammenlignes med det tilfælde, hvor du kan trænge ind på en server ved hjælp af en enkelt GET- eller POST-anmodning, så demonstrerer ulven, geden og kålen et eksempel fra en meget mere kompleks og udbredt kategori, hvor målet kun kan nås ved flere anmodninger.
Dette kan for eksempel sammenlignes med et scenarie, hvor du skal finde en SQL-injektion, skrive en fil igennem den, så hæve dine rettigheder og først derefter få en adgangskode.
Betingelser for problemet og dets løsningLandmanden skal transportere en ulv, en ged og kål over floden. Landmanden har en båd, der kun kan rumme én genstand, udover bonden selv. Ulven vil æde geden, og geden vil æde kålen, hvis landmanden efterlader dem uden opsyn.
Løsningen er, at i trin 4 skal landmanden tage bukken tilbage.
Lad os nu begynde at løse det programmatisk.
Lad os betegne bonden, ulven, ged og kål som 4 variable, der kun tager værdien 0 eller 1. Nul betyder, at de er på venstre bred, og en betyder, at de er på højre.
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
Tal er antallet af trin, der kræves for at løse. Hvert trin repræsenterer tilstanden af floden, båden og alle enheder.
Indtil videre, lad os vælge det tilfældigt og med en margen, tage 10.
Hver enhed er repræsenteret i 10 kopier - dette er dens værdi ved hvert af de 10 trin.
Lad os nu sætte betingelserne for start og må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 ]
Derefter sætter vi betingelserne, hvor ulven spiser bukken, eller bukken spiser kålen, som begrænsninger i ligningen.
(I nærværelse af en landmand er aggression umulig)
# 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) ]
Og endelig vil vi definere alle mulige handlinger fra landmanden, når de krydser dertil eller tilbage.
Han kan enten tage en ulv, en ged eller en kål med sig, eller ikke tage nogen eller slet ikke sejle nogen steder.
Selvfølgelig kan ingen krydse uden en landmand.
Dette vil blive udtrykt ved det faktum, at hver efterfølgende tilstand af floden, båden og enheder kan afvige fra den foregående kun på en strengt begrænset måde.
Ikke mere end 2 bits, og med mange andre grænser, da landmanden kun kan transportere én enhed ad gangen, og ikke alle kan efterlades samlet.
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) ]
Lad os køre løsningen.
solve(Side + Start + Finish + Safe + Travel)
Og vi får svaret!
Z3 fandt et konsistent sæt tilstande, der opfylder alle betingelser.
En slags firedimensionel afstøbning af rum-tid.
Lad os finde ud af, hvad der skete.
Vi ser, at til sidst krydsede alle, kun først besluttede vores landmand at hvile sig, og i de første 2 trin svømmer han ingen steder.
Human_2 = 0
Human_3 = 0
Dette tyder på, at antallet af stater, vi valgte, er for stort, og 8 vil være ganske tilstrækkeligt.
I vores tilfælde gjorde bonden dette: start, hvile, hvile, kryds geden, kryds tilbage, kryds kålen, vend tilbage med geden, kryds ulven, vend tilbage alene, aflever geden igen.
Men til sidst blev problemet løst.
#Старт.
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
Lad os nu prøve at ændre betingelserne og bevise, at der ikke er nogen løsninger.
For at gøre dette vil vi give vores ulv planteædende, og han vil gerne spise kål.
Dette kan sammenlignes med det tilfælde, hvor vores mål er at sikre applikationen, og vi skal sikre os, at der ikke er smuthuller.
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 gav os følgende svar:
no solution
Det betyder, at der reelt ikke er nogen løsninger.
Således beviste vi programmæssigt umuligheden af at krydse med en altædende ulv uden tab for landmanden.
Hvis publikum finder dette emne interessant, så vil jeg i fremtidige artikler fortælle dig, hvordan du omdanner et almindeligt program eller en funktion til en ligning, der er kompatibel med formelle metoder, og løser det, og derved afslører både alle legitime scenarier og sårbarheder. Først på den samme opgave, men præsenteret i form af et program, for derefter gradvist at komplicere det og gå videre til aktuelle eksempler fra softwareudviklingens verden.
Den næste artikel er allerede klar:
I den bevæger jeg mig fra formel verifikation af problemer til programmer, og beskriver
hvordan kan de automatisk konverteres til formelle regelsystemer.
Kilde: www.habr.com