Enligt min åsikt är ämnet formell verifiering inte tillräckligt täckt i den ryskspråkiga sektorn på Internet, och det saknas särskilt enkla och tydliga exempel.
Jag kommer att ge ett exempel från utländsk källa och lägga till min egen lösning på det välkända problemet med att korsa en varg, en get och en kål till andra sidan floden.
Men först ska jag kort beskriva vad formell verifiering är och varför den behövs.
Formell verifiering innebär vanligtvis att man kontrollerar ett program eller en algoritm med ett annat.
Detta är nödvändigt för att säkerställa att programmet beter sig som förväntat och även för att säkerställa dess säkerhet.
Formell verifiering är det kraftfullaste sättet att hitta och eliminera sårbarheter: det låter dig hitta alla befintliga hål och buggar i ett program, eller bevisa att de inte existerar.
Det är värt att notera att i vissa fall är detta omöjligt, som i problemet med 8 damer med en brädbredd på 1000 rutor: allt beror på algoritmisk komplexitet eller stoppproblemet.
Men i alla fall kommer ett av tre svar att tas emot: programmet är korrekt, felaktigt eller det gick inte att beräkna svaret.
Om det är omöjligt att hitta ett svar är det ofta möjligt att omarbeta oklara delar av programmet, vilket minskar deras algoritmiska komplexitet, för att få ett specifikt ja eller nej svar.
Och formell verifiering används till exempel i Windows-kärnan och Darpa-drönaroperativsystemen, för att säkerställa maximal skyddsnivå.
Vi kommer att använda Z3Prover, ett mycket kraftfullt verktyg för automatiserad teorembevisande och ekvationslösning.
Dessutom löser Z3 ekvationer och väljer inte deras värden med brute force.
Det betyder att den kan hitta svaret, även i fall där det finns 10^100 kombinationer av inmatningsalternativ.
Men detta handlar bara om ett dussin inmatningsargument av typen Integer, och detta påträffas ofta i praktiken.
Problem om 8 drottningar (Tat från engelska ).
# 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ör 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]
Drottningsproblemet är jämförbart med ett program som tar koordinaterna för 8 damer som indata och ger svaret på huruvida damerna slår varandra.
Om vi skulle lösa ett sådant program med formell verifiering, jämfört med problemet, skulle vi helt enkelt behöva ta ett steg till i form av att konvertera programkoden till en ekvation: den skulle visa sig vara i huvudsak identisk med vår ( naturligtvis om programmet skrevs korrekt).
Nästan samma sak kommer att hända vid sökning efter sårbarheter: vi ställer bara in de utdatavillkor vi behöver, till exempel administratörslösenordet, omvandlar källkoden eller den dekompilerade koden till ekvationer som är kompatibla med verifiering, och får sedan svar på vad data måste tillhandahållas som input för att uppnå målet.
Enligt min mening är problemet med vargen, geten och kålen ännu mer intressant, eftersom att lösa det redan kräver många (7) steg.
Om drottningsproblemet är jämförbart med fallet där du kan penetrera en server med en enda GET- eller POST-förfrågan, så visar vargen, geten och kålen ett exempel från en mycket mer komplex och utbredd kategori, där målet endast kan uppnås genom flera förfrågningar.
Detta är till exempel jämförbart med ett scenario där du behöver hitta en SQL-injektion, skriva en fil genom den, sedan höja dina rättigheter och först då få ett lösenord.
Villkor för problemet och dess lösningBonden behöver transportera en varg, en get och kål över floden. Bonden har en båt som bara kan ta emot ett föremål, förutom bonden själv. Vargen kommer att äta geten och geten kommer att äta kålen om bonden lämnar dem utan uppsikt.
Lösningen är att i steg 4 kommer bonden att behöva ta tillbaka geten.
Låt oss nu börja lösa det programmatiskt.
Låt oss beteckna bonden, vargen, geten och kålen som 4 variabler som tar värdet endast 0 eller 1. Noll betyder att de är på vänster strand, och en betyder att de är på höger.
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 är antalet steg som krävs för att lösa. Varje steg representerar tillståndet för floden, båten och alla enheter.
För nu, låt oss välja det slumpmässigt och med en marginal, ta 10.
Varje enhet representeras i 10 exemplar - detta är dess värde vid vart och ett av de 10 stegen.
Låt oss nu ställa in förutsättningarna för start och 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 ]
Sedan sätter vi villkoren där vargen äter geten, eller geten äter kålen, som begränsningar i ekvationen.
(I närvaro av en bonde är aggression omöjlig)
# 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) ]
Och slutligen kommer vi att definiera alla möjliga handlingar för bonden när han korsar dit eller tillbaka.
Han kan antingen ta med sig en varg, en get eller en kål, eller inte ta någon, eller inte segla någonstans alls.
Naturligtvis kan ingen passera utan en bonde.
Detta kommer att uttryckas av det faktum att varje efterföljande tillstånd av floden, båten och enheter kan skilja sig från den föregående endast på ett strikt begränsat sätt.
Inte mer än 2 bitar, och med många andra gränser, eftersom bonden bara kan transportera en enhet åt gången och inte alla kan lämnas tillsammans.
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) ]
Låt oss köra lösningen.
solve(Side + Start + Finish + Safe + Travel)
Och vi får svaret!
Z3 hittade en konsekvent uppsättning tillstånd som uppfyller alla villkor.
En sorts fyrdimensionell gjutning av rum-tid.
Låt oss ta reda på vad som hände.
Vi ser att alla till slut korsade, bara först bestämde sig vår bonde för att vila, och i de första 2 stegen simmar han ingenstans.
Human_2 = 0
Human_3 = 0
Detta tyder på att antalet stater vi valde är för stort, och 8 kommer att vara ganska tillräckligt.
I vårt fall gjorde bonden så här: starta, vila, vila, korsa bocken, korsa tillbaka, korsa kålen, återvända med geten, korsa vargen, återvända tillbaka ensam, återleverera geten.
Men till slut var 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
Låt oss nu försöka ändra förutsättningarna och bevisa att det inte finns några lösningar.
För att göra detta kommer vi att ge vår varg växtätande, och han kommer att vilja äta kål.
Detta kan jämföras med fallet där vårt mål är att säkra applikationen och vi måste se till att det inte finns några kryphål.
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 oss följande svar:
no solution
Det betyder att det verkligen inte finns några lösningar.
Därmed bevisade vi programmatiskt omöjligheten att korsa med en allätande varg utan förluster för bonden.
Om publiken tycker att det här ämnet är intressant, kommer jag i framtida artiklar att berätta hur man förvandlar ett vanligt program eller funktion till en ekvation som är kompatibel med formella metoder, och löser det, och avslöjar därmed både alla legitima scenarier och sårbarheter. Först på samma uppgift, men presenterad i form av ett program, för att sedan gradvis komplicera det och gå vidare till aktuella exempel från världen av mjukvaruutveckling.
Nästa artikel är redan klar:
I den går jag från formell verifiering av problem till program och beskriver
hur kan de automatiskt omvandlas till formella regelsystem.
Källa: will.com