Etter min mening, i den russiskspråklige sektoren av Internett, er ikke temaet formell verifisering tilstrekkelig dekket, og det er spesielt mangel på enkle og klare eksempler.
Jeg vil gi et eksempel fra en utenlandsk kilde, og legge til min egen løsning på det velkjente problemet med å krysse en ulv, en geit og en kål til den andre siden av elva.
Men først vil jeg kort beskrive hva formell verifisering er og hvorfor det er nødvendig.
Formell verifisering betyr vanligvis å sjekke ett program eller algoritme ved hjelp av et annet.
Dette er nødvendig for å sikre at programmet oppfører seg som forventet og også for å sikre sikkerheten.
Formell verifisering er den kraftigste måten å finne og eliminere sårbarheter: den lar deg finne alle eksisterende hull og feil i et program, eller bevise at de ikke eksisterer.
Det er verdt å merke seg at i noen tilfeller er dette umulig, for eksempel i problemet med 8 damer med en brettbredde på 1000 ruter: alt kommer ned til algoritmisk kompleksitet eller stoppproblemet.
Men uansett vil ett av tre svar mottas: programmet er riktig, feil, eller det var ikke mulig å beregne svaret.
Hvis det er umulig å finne et svar, er det ofte mulig å omarbeide uklare deler av programmet, redusere deres algoritmiske kompleksitet, for å få et spesifikt ja eller nei svar.
Og formell verifisering brukes for eksempel i Windows-kjernen og Darpa drone-operativsystemer, for å sikre maksimalt beskyttelsesnivå.
Vi vil bruke Z3Prover, et veldig kraftig verktøy for automatisert teorembevis og ligningsløsning.
Dessuten løser Z3 ligninger, og velger ikke verdiene deres ved å bruke brute force.
Dette betyr at den er i stand til å finne svaret, selv i tilfeller der det er 10^100 kombinasjoner av inndataalternativer.
Men dette dreier seg bare om et dusin input-argumenter av typen Integer, og dette støtes ofte på i praksis.
Oppgave om 8 dronninger (Tatt 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)
Når vi kjø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]
Dronningproblemet kan sammenlignes med et program som tar inn koordinatene til 8 damer og gir svaret på om dronningene slår hverandre.
Hvis vi skulle løse et slikt program ved hjelp av formell verifisering, ville vi, sammenlignet med problemet, ganske enkelt måtte ta ett steg til i form av å konvertere programkoden til en ligning: den ville vise seg å være i hovedsak identisk med vår ( selvfølgelig, hvis programmet ble skrevet riktig).
Nesten det samme vil skje ved søk etter sårbarheter: vi setter bare utgangsbetingelsene vi trenger, for eksempel admin-passordet, transformerer kildekoden eller dekompilerte koden til ligninger som er kompatible med verifisering, og får så svar på hva data må leveres som input for å nå målet.
Etter min mening er problemet med ulven, geiten og kålen enda mer interessant, siden å løse det allerede krever mange (7) trinn.
Hvis dronningproblemet er sammenlignbart med tilfellet der du kan trenge inn i en server ved å bruke en enkelt GET- eller POST-forespørsel, viser ulven, geiten og kålen et eksempel fra en mye mer kompleks og utbredt kategori, der målet bare kan oppnås etter flere forespørsler.
Dette kan for eksempel sammenlignes med et scenario der du trenger å finne en SQL-injeksjon, skrive en fil gjennom den, deretter heve rettighetene dine og først da få et passord.
Betingelsene for problemet og dets løsningBonden må frakte en ulv, en geit og kål over elva. Bonden har en båt som kun har plass til én gjenstand, foruten bonden selv. Ulven vil spise geiten og geiten vil spise kålen hvis bonden lar dem være uten tilsyn.
Løsningen er at i trinn 4 må bonden ta bukken tilbake.
La oss nå begynne å løse det programmatisk.
La oss betegne bonden, ulven, geiten og kålen som 4 variabler som tar verdien bare 0 eller 1. Null betyr at de er på venstre bredd, og en betyr at de er på høyre.
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
Tall er antall trinn som kreves for å løse. Hvert trinn representerer tilstanden til elven, båten og alle enheter.
For nå, la oss velge det tilfeldig og med en margin, ta 10.
Hver enhet er representert i 10 kopier - dette er verdien ved hvert av de 10 trinnene.
La oss nå sette betingelsene 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 ]
Deretter setter vi betingelsene der ulven spiser geita, eller geita spiser kålen, som begrensninger i ligningen.
(I nærvær av en bonde er aggresjon 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 til slutt vil vi definere alle mulige handlinger til bonden når han krysser dit eller tilbake.
Han kan enten ta med seg en ulv, en geit eller en kål, eller ikke ta noen, eller ikke seile noe sted i det hele tatt.
Selvfølgelig kan ingen krysse uten en bonde.
Dette vil bli uttrykt av det faktum at hver påfølgende tilstand av elven, båten og enhetene kan avvike fra den forrige bare på en strengt begrenset måte.
Ikke mer enn 2 biter, og med mange andre grenser, siden bonden bare kan transportere én enhet om gangen og ikke alle kan stå 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) ]
La oss kjøre løsningen.
solve(Side + Start + Finish + Safe + Travel)
Og vi får svaret!
Z3 fant et konsistent sett med tilstander som tilfredsstiller alle betingelser.
En slags firedimensjonal cast av rom-tid.
La oss finne ut hva som skjedde.
Vi ser at til slutt krysset alle, bare først bestemte bonden vår seg for å hvile, og i de første 2 trinnene svømmer han ikke noe sted.
Human_2 = 0
Human_3 = 0
Dette antyder at antallet stater vi valgte er for stort, og 8 vil være ganske tilstrekkelig.
I vårt tilfelle gjorde bonden dette: starte, hvile, hvile, krysse bukken, krysse tilbake, krysse kålen, returnere med bukken, krysse ulven, returnere tilbake alene, levere bukken på nytt.
Men til slutt ble 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
La oss nå prøve å endre betingelsene og bevise at det ikke finnes noen løsninger.
For å gjøre dette vil vi gi ulven vår planteetende, og han vil spise kål.
Dette kan sammenlignes med saken der målet vårt er å sikre applikasjonen og vi må sørge for at det ikke er smutthull.
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 ga oss følgende svar:
no solution
Det betyr at det egentlig ikke finnes noen løsninger.
Dermed beviste vi programmessig umuligheten av å krysse med en altetende ulv uten tap for bonden.
Hvis publikum synes dette emnet er interessant, vil jeg i fremtidige artikler fortelle deg hvordan du kan gjøre om et vanlig program eller funksjon til en ligning som er kompatibel med formelle metoder, og løse det, og dermed avsløre både alle legitime scenarier og sårbarheter. Først på samme oppgave, men presentert i form av et program, for så å komplisere det gradvis og gå videre til aktuelle eksempler fra programvareutviklingens verden.
Neste artikkel er allerede klar:
I den går jeg fra formell verifisering av problemer til programmer, og beskriver
hvordan kan de konverteres til formelle regelsystemer automatisk.
Kilde: www.habr.com