Jeg mener, at emnet for formel validering ikke er tilstrækkeligt dækket i den russisktalende del af internettet, og der mangler særligt enkle og illustrative eksempler.
Jeg vil give et eksempel fra en udenlandsk kilde og supplere med min egen løsning på den kendte opgave med at transportere ulven, geden og kålen over floden.
Men først vil jeg kort beskrive, hvad formel validering er, og hvorfor den er nødvendig.
Med formel validering forstår man normalt at kontrollere et program eller en algoritme ved hjælp af et andet.
Dette er nødvendigt for at sikre, at programmets adfærd svarer til forventningerne, samt at sikre dens sikkerhed.
Formel validering er det mest kraftfulde middel til at finde og fjerne sårbarheder: det gør det muligt at finde alle eksisterende fejl og bugs i programmet eller at bevise, at de ikke findes.
Det skal bemærkes, at i visse tilfælde kan dette være umuligt, som i tilfellet med de 8 dronninger og en bræddebredde på 1000 felter: alt afhænger af den algoritmiske kompleksitet eller stopproblemet.
Men i enhver situation vil man få et af tre svar: programmet er korrekt, ikke korrekt, eller det var ikke muligt at beregne svaret.
I tilfælde af, at svaret ikke kan findes, kan man ofte omarbejde de uklare dele af programmet for at reducere deres algoritmiske kompleksitet, for at få et konkret ja eller nej.
Formel validering anvendes for eksempel i Windows-kernen og i styresystemer for droner fra Darpa for at sikre det højeste beskyttelsesniveau.
Vi vil bruge Z3Prover, et meget kraftfuldt værktøj til automatiseret bevis af sætninger og løsning af ligninger.
Z3 løser nemlig ligninger, og finder ikke blot deres værdier gennem brute force.
Det betyder, at det er i stand til at finde svaret, selv i tilfælde hvor der er 10^100 kombinationer af indgangsvarianter.
Og det er vel kun omkring et dusin indgangsargumenter af typen Integer, og sådanne situationer forekommer ofte i praksis.
Opgaven om de 8 dronninger (taget fra en engelsksproget ).
# 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)
Når vi kører 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]
Opgaven om dronningerne kan sammenlignes med et program, der tager koordinaterne for 8 dronninger som input og giver svaret om, de angriber hinanden.
Hvis vi skulle løse et sådant program ved hjælp af formel verifikation, ville vi i forhold til opgaven simpelthen have været nødt til at tage endnu et skridt i form af at omdanne programmets kode til en ligning: det ville i sin essens være identisk med vores (selvfølgelig, hvis programmet er skrevet uden fejl).
Praktisk talt det samme vil ske i tilfælde af at finde sårbarheder: vi angiver blot de ønskede outputbetingelser, for eksempel administratorens adgangskode, omdanner den originale eller dekompilerede kode til verifikationskompatible ligninger, og derefter får vi svaret om, hvilke data der skal gives som input for at nå målet.
Efter min mening er opgaven om ulven, gedden og kålen endda mere interessant, da det i denne løsning kræves mange (7) skridt.
Hvis opgaven om dronningerne er sammenlignelig med varianten, hvor man kan få adgang til serveren med én GET eller POST anmodning, så viser ulven, gedden og kålen et eksempel fra en meget mere kompleks og udbredt kategori, hvor målene kun kan nås gennem flere anmodninger.
Det er sammenligneligt eksempelvis med et scenarie, hvor man skal finde en SQL-injektion, skrive en fil via den, hæve sine rettigheder og kun derefter få adgangskoden.
Opgavens betingelser og dens løsningLandmanden skal transportere en ulv, en ged og en kål over floden. Landmanden har en båd, som kun kan rumme ham selv og ét objekt. Ulven vil spise geden, og geden vil spise kålen, hvis landmanden lader dem være uden opsyn.
Løsningen er, at landmanden ved det 4. skridt skal tage geden tilbage.
Lad os nu begynde at løse det programmatisk.
Lad os betegne landmanden, ulven, geden og kålen som 4 variable, som kun kan have værdien 0 eller 1. Nul betyder, at de er på venstre bred, og en betyder, at de er på højre bred.
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) ]
# Hver skabning kan kun være på venstre (0) eller højre side (1) i hver tilstand
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 — dette er antallet af skridt, der er nødvendige for at løse. Hvert skridt repræsenterer en tilstand af floden, båden og alle entiteterne.
Lad os vælge den tilfældigt og med lidt overmål, vi tager 10.
Hver enhed præsenteres i 10 eksemplarer — det er dens værdi på hver af de 10 trin.
Nu sætter vi 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 angiver vi betingelserne, hvor ulven spiser gedden, eller geden spiser kålen som begrænsninger i ligningen.
(I nærvær af landmanden 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 sætter vi alle mulige handlinger, landmanden kan tage, når han transporterer.
Han kan tage ulven, geden eller kålen med sig, eller han kan vælge ikke at tage nogen, eller slet ikke sejle.
Naturligvis kan ingen transporteres uden landmanden.
Dette udtrykkes ved, at hver efterfølgende tilstand af floden, båden og enhederne kun kan adskille sig fra den forrige på en strengt begrænset måde.
Ikke mere end 2 enheder, og med mange andre begrænsninger, fordi landmanden kun kan transportere én enhed ad gangen, og ikke alle kan efterlades sammen.
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 starte løsningen.
solve(Side + Start + Finish + Safe + Travel)
Og vi får svaret!
Z3 fandt en konsistent mængde tilstande, der opfylder alle betingelser.
En slags fire-dimensionelt aftryk af rumtid.
Lad os finde ud af, hvad der skete.
Vi ser, at alle er blevet transporteret, men i starten valgte vores landmand at tage en pause og sejlede ikke de første 2 skridt.
Human_2 = 0
Human_3 = 0
Dette indikerer, at antallet af tilstande, vi valgte, er overflødigt, og 8 vil være mere end tilstrækkeligt.
I vores tilfælde handlede landmanden således: start, hvil, hvil, transport af geden, transport tilbage, transport af kålen, retur med geden, transport af ulven, tilbage alene, gentagen levering af geden.
Men til sidst blev opgaven 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 dette vil vi give vores ulv herbivoritet, og han ønsker at spise kålen.
Dette kan sammenlignes med en situation, hvor vores mål er at beskytte applikationen, og vi skal sikre os, at der ikke er nogen svagheder.
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:
ingen løsning
Det betyder, at der virkelig ikke findes nogen løsninger.
Hermed har vi programmatisk bevist umuligheden af at transportere en altædende ulv uden tab for landmanden.
Hvis publikum finder dette emne interessant, vil jeg i fremtidige artikler fortælle, hvordan man kan transformere et almindeligt program eller funktion til et der er kompatibelt med formelle metoder, og løse det, hvilket vil afsløre både legitime scenarier og sårbarheder. Først med denne samme opgave præsenteret som et program, og derefter gradvist kompliceret og gående videre til aktuelle eksempler fra softwareudviklingsverdenen.
Den næste artikel er allerede klar:
I den skifter jeg fra formel verifikation af opgaver til programmer og beskriver,
hvordan de kan konverteres til systemer med formelle regler automatisk.
Kilde: habr.com
