Naar mijn mening is het onderwerp van formele verificatie in de Russische internetsector onvoldoende belicht, en vooral missen we eenvoudige en duidelijke voorbeelden.
Ik zal een dergelijk voorbeeld uit een buitenlandse bron geven en aanvullen met mijn eigen oplossing voor de bekende taak van het oversteken van de wolf, de geit en de kool aan de andere kant van de rivier.
Maar eerst zal ik kort beschrijven wat formele verificatie inhoudt en waarom het nodig is.
Met formele verificatie wordt meestal bedoeld dat één programma of algoritme wordt gecontroleerd met behulp van een ander.
Dit is nodig om te verifiëren of het gedrag van het programma overeenkomt met de verwachtingen en om de veiligheid te waarborgen.
Formele verificatie is het krachtigste middel om kwetsbaarheden te vinden en te verhelpen: het maakt het mogelijk om alle bestaande gaten en bugs in het programma te vinden of te bewijzen dat ze er niet zijn.
Het is belangrijk op te merken dat dit in sommige gevallen onmogelijk kan zijn, zoals bijvoorbeeld bij de taak van de 8 dames op een bord van 1000 velden: alles hangt af van de algoritmische complexiteit of het stopprobleem.
Toch zullen in elk geval een van de drie antwoorden worden verkregen: het programma is correct, incorrect, of het is niet mogelijk om een antwoord te berekenen.
In het geval dat het niet mogelijk is om een antwoord te vinden, kan het vaak helpen om onduidelijkheden in het programma opnieuw te bewerken, waardoor de algoritmische complexiteit wordt verminderd, om een concreet antwoord ja of nee te krijgen.
Formele verificatie wordt bijvoorbeeld toegepast in de Windows-kernel en in de operationele systemen van drones van Darpa, om het hoogste niveau van beveiliging te waarborgen.
We zullen Z3Prover gebruiken, een zeer krachtige tool voor geautomatiseerd bewijs van stellingen en het oplossen van vergelijkingen.
En Z3 lost daadwerkelijk vergelijkingen op, in plaats van hun waarden ruwweg te proberen door brute force.
Dit betekent dat het in staat is om een antwoord te vinden, zelfs in gevallen waar de combinaties van invoervarianten 10^100 bedragen.
En dat is gewoon een paar binnenargumenten van het type Integer, wat vaak in de praktijk voorkomt.
De taak van de 8 dames (genomen uit een Engelstalige ).
# 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)
Bij het starten van Z3 krijgen we de oplossing:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
De taak van de dames is te vergelijken met een programma dat de coördinaten van 8 dames als invoer accepteert en het antwoord geeft of de dames elkaar aanvallen.
Als we zo'n programma met formele verificatie zouden benaderen, dan zouden we in vergelijking met de taak gewoon nog een stap moeten zetten in de vorm van het omzetten van de programmatuur naar een vergelijking: deze zou in wezen identiek zijn aan onze, mits de programmatuur foutloos is geschreven.
Bij het zoeken naar kwetsbaarheden zal vrijwel hetzelfde gebeuren: we stellen simpelweg de gewenste uitgangsvoorwaarden, zoals het admin-wachtwoord, vast, zetten de oorspronkelijke of gedecompileerde code om in verificatie-compatibele vergelijkingen en krijgen dan als resultaat welke gegevens we als invoer moeten geven om ons doel te bereiken.
Naar mijn mening is de taak van de wolf, de geit en de kool zelfs interessanter, aangezien er al veel (7) stappen nodig zijn om deze op te lossen.
Als de taak van de dames vergelijkbaar is met een situatie waarin je de server kunt binnendringen met één GET- of POST-verzoek, laat de wolf, de geit en de kool een voorbeeld zien van een veel complexere en wijdverspreide categorie waarin doelen alleen met meerdere verzoeken kunnen worden bereikt.
Dit is bijvoorbeeld vergelijkbaar met een scenario waarin je een SQL-injectie moet vinden, een bestand via deze injectie moet schrijven, vervolgens je rechten moet verhogen en pas daarna het wachtwoord kunt verkrijgen.
De voorwaarden van de taak en de oplossingDe boer moet een wolf, een geit en een kool over de rivier vervoeren. De boer heeft een boot waarin, behalve de boer zelf, slechts één object kan passen. De wolf eet de geit op, en de geit eet de kool op als de boer ze onbeheerd achterlaat.
De oplossing is dat de boer de geit op de 4e stap terug moet brengen.
Laten we nu beginnen met de oplossing via een programma.
Laten we de boer, wolf, geit en kool als 4 variabelen aanduiden die alleen de waarde 0 of 1 kunnen aannemen. Nul betekent dat ze op de linkeroever zijn, en één betekent dat ze op de rechteroever zijn.
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) ]
# Elke schepsel kan alleen aan de linkerkant (0) of rechterkant (1) zijn in elke staat
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 - is het aantal stappen dat nodig is om op te lossen. Elke stap vertegenwoordigt een toestand van de rivier, de boot en alle entiteiten.
Laten we voorlopig iets willekeurigs kiezen en 10 nemen.
Elke entiteit is vertegenwoordigd in 10 exemplaren — dit is zijn waarde in elk van de 10 stappen.
Laten we nu de voorwaarden voor start en finish definiëren.
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 ]
Vervolgens definiëren we de voorwaarden waaronder de wolf de geit eet, of de geit de kool, als beperkingen in de vergelijking.
(In aanwezigheid van de boer is agressie onmogelijk)
# 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) ]
En tot slot definiëren we alle mogelijke acties van de boer tijdens de oversteek heen of terug.
Hij kan de wolf, de geit of de kool meenemen, of niemand meenemen, of helemaal niet varen.
Natuurlijk kan niemand zonder de boer oversteek maken.
Dit zal tot uiting komen in het feit dat elke volgende staat van de rivier, de boot en de entiteiten alleen op strikt beperkte manieren kan afwijken van de vorige.
Niet meer dan 2 bits, en met nog veel andere limieten, aangezien de boer maar één entiteit tegelijk kan vervoeren en niet iedereen samen kan laten.
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])) voor i in range(Num-1) ]
Laten we de oplossing uitvoeren.
solve(Side + Start + Finish + Safe + Travel)
En we krijgen het antwoord!
Z3 vond een coherente en aan alle voorwaarden voldoend geheel van staten.
Een soort vierdimensionale afdruk van de ruimte-tijd.
Laten we bekijken wat er is gebeurd.
We zien dat uiteindelijk iedereen is overgestoken, maar in het begin besloot onze boer te rusten en in de eerste 2 stappen niet te varen.
Human_2 = 0
Human_3 = 0
Dit geeft aan dat het aantal gekozen staten overmatig is, en 8 zal volledig voldoende zijn.
In ons geval handelde de boer als volgt: start, rust, rust, overtocht van de geit, terugkeer, overtocht van de kool, terugkeer met de geit, overtocht van de wolf, alleen terugkeren, opnieuw de geit brengen.
Maar uiteindelijk is het probleem opgelost.
#Старт.
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
Laten we nu proberen de voorwaarden te veranderen en aan te tonen dat er geen oplossingen zijn.
Daarvoor voorzien we onze wolf van herbivoriteit, en zal hij de kool willen opeten.
Dit kan worden vergeleken met een situatie waarin ons doel is de bescherming van de applicatie en we moeten ervoor zorgen dat er geen achterdeurtjes zijn.
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 gaf ons het volgende antwoord:
geen oplossing
Dat betekent dat er werkelijk geen oplossingen zijn.
Zo hebben we programmatisch aangetoond dat de oversteek met de allesetende wolf niet mogelijk is, zonder verliezen voor de boer.
Als het publiek deze thematiek interessant vindt, zal ik in toekomstige artikelen uitleggen hoe je een gewone program of functie kunt omvormen tot een compatibel vergelijking met formele methoden en het op te lossen, waarbij zowel legitieme scenario's als kwetsbaarheden worden ontdekt. Eerst met exact dezelfde taak, maar deze al gepresenteerd in de vorm van een programma, en dan geleidelijk complexer wordend en overgaand naar actuele voorbeelden uit de wereld van softwareontwikkeling.
Het volgende artikel is al klaar:
Daarin ga ik van formele verificatie van taken naar programma's en beschrijf ik,
hoe ze automatisch kunnen worden omgezet in systemen van formele regels.
Bron: habr.com
