Naar mijn mening wordt in de Russischtalige sector van het internet het onderwerp formele verificatie niet voldoende behandeld, en is er vooral een gebrek aan eenvoudige en duidelijke voorbeelden.
Ik zal een voorbeeld uit een buitenlandse bron geven en mijn eigen oplossing toevoegen aan het bekende probleem van het oversteken van een wolf, een geit en een kool naar de andere kant van de rivier.
Maar eerst zal ik kort beschrijven wat formele verificatie is en waarom dit nodig is.
Formele verificatie betekent meestal dat het ene programma of algoritme wordt gecontroleerd met behulp van een ander programma of algoritme.
Dit is nodig om ervoor te zorgen dat het programma zich gedraagt zoals verwacht en om de veiligheid ervan te garanderen.
Formele verificatie is het krachtigste middel om kwetsbaarheden op te sporen en te elimineren: het stelt je in staat alle bestaande gaten en bugs in een programma te vinden, of te bewijzen dat ze niet bestaan.
Het is vermeldenswaard dat dit in sommige gevallen onmogelijk is, zoals bij het probleem van 8 vrouwen met een bordbreedte van 1000 vierkanten: het komt allemaal neer op algoritmische complexiteit of het stopprobleem.
In ieder geval wordt echter één van de drie antwoorden ontvangen: het programma is correct, onjuist of het was niet mogelijk om het antwoord te berekenen.
Als het onmogelijk is om een antwoord te vinden, is het vaak mogelijk om onduidelijke delen van het programma te herwerken, waardoor hun algoritmische complexiteit wordt verminderd, om een specifiek ja of nee-antwoord te verkrijgen.
En formele verificatie wordt bijvoorbeeld gebruikt in de Windows-kernel en de Darpa-dronebesturingssystemen om het maximale beschermingsniveau te garanderen.
We zullen Z3Prover gebruiken, een zeer krachtig hulpmiddel voor het geautomatiseerd bewijzen van stellingen en het oplossen van vergelijkingen.
Bovendien lost Z3 vergelijkingen op en selecteert de waarden ervan niet met brute kracht.
Dit betekent dat het het antwoord kan vinden, zelfs in gevallen waarin er 10^100 combinaties van invoeropties zijn.
Maar dit zijn slechts een tiental invoerargumenten van het type Integer, en dit kom je in de praktijk vaak tegen.
Probleem over 8 koninginnen (overgenomen uit het Engels ).
# 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)
Met 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]
Het koninginnenprobleem is vergelijkbaar met een programma dat de coördinaten van 8 koninginnen als invoer neemt en het antwoord geeft of de koninginnen elkaar verslaan.
Als we een dergelijk programma zouden oplossen met behulp van formele verificatie, zouden we, vergeleken met het probleem, eenvoudigweg nog een stap moeten zetten in de vorm van het omzetten van de programmacode in een vergelijking: deze zou in essentie identiek blijken te zijn aan de onze ( natuurlijk, als het programma correct is geschreven).
Bijna hetzelfde zal gebeuren bij het zoeken naar kwetsbaarheden: we stellen gewoon de uitvoervoorwaarden in die we nodig hebben, bijvoorbeeld het beheerderswachtwoord, transformeren de broncode of de gedecompileerde code in vergelijkingen die compatibel zijn met verificatie, en krijgen dan antwoord op de vraag wat Om het doel te bereiken moeten gegevens als input worden aangeleverd.
Naar mijn mening is het probleem rond de wolf, de geit en de kool zelfs nog interessanter, omdat het oplossen ervan al veel (7) stappen vereist.
Als het koninginprobleem vergelijkbaar is met het geval waarin je een server kunt binnendringen met een enkel GET- of POST-verzoek, dan demonstreert de wolf, geit en kool een voorbeeld uit een veel complexere en wijdverbreidere categorie, waarin het doel alleen kan worden bereikt door meerdere verzoeken.
Dit is bijvoorbeeld vergelijkbaar met een scenario waarin je een SQL-injectie moet vinden, er een bestand doorheen moet schrijven, vervolgens je rechten moet verhogen en pas dan een wachtwoord moet krijgen.
Condities van het probleem en de oplossing ervanDe boer moet een wolf, een geit en kool over de rivier vervoeren. De boer heeft een boot waar naast de boer zelf maar één object in kan. De wolf zal de geit opeten en de geit zal de kool opeten als de boer ze onbeheerd achterlaat.
De oplossing is dat de boer in stap 4 de geit terug moet nemen.
Laten we het nu programmatisch oplossen.
Laten we de boer, wolf, geit en kool aanduiden als 4 variabelen die slechts de waarde 0 of 1 aannemen. Nul betekent dat ze zich op de linkeroever bevinden, en één betekent dat ze zich op de rechteroever bevinden.
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 is het aantal stappen dat nodig is om op te lossen. Elke stap vertegenwoordigt de toestand van de rivier, de boot en alle entiteiten.
Laten we het voorlopig willekeurig kiezen en met een marge 10 nemen.
Elke entiteit wordt weergegeven in 10 exemplaren - dit is de waarde ervan bij elk van de 10 stappen.
Laten we nu de voorwaarden voor de start en finish instellen.
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 stellen we de voorwaarden waarin de wolf de geit eet, of de geit de kool, als beperkingen in de vergelijking.
(In aanwezigheid van een 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 ten slotte zullen we alle mogelijke acties van de boer definiëren bij het oversteken heen of terug.
Hij kan een wolf, een geit of een kool meenemen, of niemand meenemen, of helemaal nergens heen varen.
Natuurlijk kan niemand zonder boer oversteken.
Dit zal tot uiting komen in het feit dat elke volgende toestand van de rivier, de boot en de entiteiten slechts in strikt beperkte mate van de vorige kan verschillen.
Niet meer dan 2 bits, en met veel andere limieten, omdat de boer slechts één entiteit tegelijk kan vervoeren en niet alles bij elkaar 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])) for i in range(Num-1) ]
Laten we de oplossing uitvoeren.
solve(Side + Start + Finish + Safe + Travel)
En wij krijgen het antwoord!
Z3 heeft een consistente reeks toestanden gevonden die aan alle voorwaarden voldoet.
Een soort vierdimensionale weergave van ruimte-tijd.
Laten we uitzoeken wat er is gebeurd.
We zien dat uiteindelijk iedereen overstak, alleen besloot onze boer eerst te rusten, en in de eerste 2 stappen zwemt hij nergens heen.
Human_2 = 0
Human_3 = 0
Dit wijst erop dat het aantal door ons gekozen staten buitensporig groot is, en dat acht ruimschoots voldoende zal zijn.
In ons geval deed de boer dit: starten, rusten, rusten, de geit oversteken, terug oversteken, de kool oversteken, terug met de geit, de wolf oversteken, alleen teruggaan, de geit opnieuw afleveren.
Maar uiteindelijk was 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 omstandigheden te veranderen en te bewijzen dat er geen oplossingen zijn.
Om dit te doen, zullen we onze wolf herbivoor geven, en hij zal kool willen eten.
Dit kan worden vergeleken met het geval waarin het ons doel is om de applicatie te beveiligen en we ervoor moeten zorgen dat er geen mazen in de wet 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:
no solution
Het betekent dat er eigenlijk geen oplossingen zijn.
Zo hebben we programmatisch de onmogelijkheid bewezen om met een allesetende wolf over te steken zonder verliezen voor de boer.
Als het publiek dit onderwerp interessant vindt, zal ik je in toekomstige artikelen vertellen hoe je van een gewoon programma of functie een vergelijking kunt maken die compatibel is met formele methoden, en hoe je deze kunt oplossen, waardoor zowel alle legitieme scenario's als kwetsbaarheden aan het licht komen. Eerst met dezelfde taak, maar gepresenteerd in de vorm van een programma, om het vervolgens geleidelijk ingewikkelder te maken en verder te gaan met actuele voorbeelden uit de wereld van softwareontwikkeling.
Het volgende artikel is al klaar:
Daarin ga ik van formele verificatie van problemen naar programma's en beschrijvingen
hoe kunnen ze automatisch worden omgezet in formele regelsystemen?
Bron: www.habr.com