En min mening är ämnet för formell verifiering inte tillräckligt belyst inom den rysktalande delen av internet, och det saknas särskilt enkla och tydliga exempel.
Jag kommer att ge ett exempel från en utländsk källa och komplettera det med min egen lösning på den kända uppgiften om att transportera vargen, geten och kålen över floden.
Men först kommer jag kort att beskriva vad formell verifiering innebär och varför det är viktigt.
Med formell verifiering avses vanligtvis att kontrollera ett program eller en algoritm med hjälp av ett annat.
Detta behövs för att säkerställa att programmets beteende överensstämmer med det förväntade, samt för att garantera dess säkerhet.
Formell verifiering är det mest kraftfulla verktyget för att hitta och åtgärda sårbarheter: den gör det möjligt att identifiera alla existerande hål och buggar i programmet, eller bevisa att de inte finns.
Det är värt att notera att detta i vissa fall kan vara omöjligt, som till exempel i uppgiften om 8 drottningar med en bräda som är 1000 rutor bred: allt beror på algoritmisk komplexitet eller stoppproblemet.
Men i alla fall kommer ett av tre svar att fås: programmet är korrekt, inkorrekt, eller så kunde inget svar beräknas.
Vid oförmåga att hitta ett svar kan man ofta omarbeta oklarheterna i programmet för att minska dess algoritmiska komplexitet, så att man får ett konkret svar ja eller nej.
Formell verifiering tillämpas till exempel i Windows-kärnan och i Darpa:s operativsystem för obemannade flygfarkoster för att säkerställa högsta skyddsnivå.
Vi kommer att använda Z3Prover, ett väldigt kraftfullt verktyg för automatiserad bevisföring och lösning av ekvationer.
Z3 löser nämligen ekvationer, inte genom att pröva värden bruteforce.
Detta innebär att den kan hitta ett svar, även i fall där antalet kombinationer av ingångsvärden är 10^100.
Och det handlar egentligen bara om ett dussin ingångsargument av typen Integer, vilket ofta förekommer i praktiken.
Uppgiften om 8 drottningar (Tagen från en engelskspråkig ).
# 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]
Uppgiften om drottningarna kan jämföras med ett program som tar in koordinaterna för 8 drottningar och ger svaret på om drottningarna slår varandra.
Om vi skulle lösa ett sådant program med hjälp av formell verifiering, skulle vi i jämförelse med uppgiften bara behöva ta ett steg till i form av att omvandla programmets kod till en ekvation: den skulle i sin kärna bli identisk med vår (förutsatt att programmet är skrivet felfritt).
I stort sett samma sak skulle hända vid sårbarhetssökning: vi anger bara de utdata vi behöver, till exempel administratörslösenordet, omvandlar den ursprungliga eller dekompilerade koden till verifieringskompatibla ekvationer och får sedan svaret på vilka data som måste matas in för att nå målet.
Enligt min uppfattning är uppgiften om vargen, geten och kålen ännu mer intressant, eftersom det krävs många (7) steg för att lösa den.
Om uppgiften om damen är jämförbar med ett scenario där man kan penetrera servern med en enda GET- eller POST-begäran, så visar vargen, geten och kålen exempel på en mycket mer komplex och vanlig kategori, där målen bara kan uppnås med flera begärningar.
Det är jämförbart med ett scenario där man behöver hitta en SQL-injektion, skriva en fil genom den, höja sina behörigheter och först därefter få tillgång till lösenordet.
Villkoren för uppgiften och dess lösning.Bonden måste föra vargen, geten och kålen över floden. Bonden har en båt som kan rymma, förutom bonden själv, endast ett objekt. Vargen kommer att äta geten, och geten kommer att äta kålen om bonden lämnar dem utan tillsyn.
Lösningen är att bonden i det fjärde steget måste föra geten tillbaka.
Nu går vi till lösningen med hjälp av programvara.
Låt oss beteckna bonden, vargen, geten och kålen som 4 variabler som kan anta värdet 0 eller 1. Noll betyder att de är på vänster sida, och ett betyder att de är på höger sida.
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) ]
# Varje varelse kan endast vara på vänster (0) eller höger sida (1) vid varje tillstånd
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 — det är antalet steg som krävs för att lösa uppgiften. Varje steg representerar ett tillstånd av floden, båten och alla entiteter.
Låt oss först välja honom slumpmässigt och med en reserv, vi tar 10.
Varje entitet representeras i 10 exemplar — detta är dess värde vid var och en av de 10 stegen.
Nu låt oss ställa upp 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 ]
Därefter ställer vi förutsättningarna där vargen äter geten, eller geten äter kålen, som begränsningar i ekvationen.
(I närvaro av bonden ä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, låt oss lista alla möjliga handlingar som bonden kan vid överfarten dit eller tillbaka.
Han kan antingen ta med sig vargen, geten eller kålen, eller ta ingen, eller inte åka någonstans alls.
Naturligtvis kan ingen korsa utan bonden.
Detta kommer att uttryckas genom att varje nytt tillstånd av floden, båten och entiteterna kan skilja sig från det föregående endast på ett strikt begränsat sätt.
Inte mer än 2 bitar, och med många andra begränsningar, eftersom bonden bara kan transportera en entitet å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 konsistent och tillfredsställande uppsättning tillstånd.
En slags fyrdimensionell avbildning av rum-tid.
Låt oss reda ut vad som hände.
Vi ser att alla har korsat, men i början bestämde sig vår bonde för att vila, och åkte ingenstans under de första 2 stegen.
Human_2 = 0
Human_3 = 0
Detta innebär att antalet tillstånd vi valt är överflödigt, och 8 kommer att vara mer än nog.
I vårt fall gjorde bonden så här: start, vila, vila, överfart av geten, överfart tillbaka, överfart av kålen, återkomst med geten, överfart av vargen, återkomst ensam, och upprepad leverans av geten.
Men resultatet är att uppgiften är 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
Nu ska vi försöka ändra villkoren och bevisa att det inte finns några lösningar.
För detta ska vi ge vår varg herbivoriska egenskaper, och han kommer att vilja äta kålen.
Det kan jämföras med en situation där vårt mål är att skydda en applikation och vi måste säkerställa 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:
ingen lösning
Det betyder att det faktiskt inte finns några lösningar.
Således har vi programvarumässigt bevisat att det är omöjligt att transportera med den allätande vargen utan förluster för bonden.
Om publiken tycker att detta ämne är intressant, kommer jag i framtida artiklar att berätta hur man kan omvandla ett vanligt program eller en funktion till en som är kompatibel med formella metoder, och lösa det, därigenom upptäcka både legitima scenarier och sårbarheter. Först med samma uppgift, men presenterad som ett program, och sedan gradvis öka komplexiteten och gå vidare till aktuella exempel från mjukvaruutvecklingens värld.
Nästa artikel är redan klar:
I den går jag från formell verifiering av uppgifter till program och beskriver,
hur man automatiskt kan konvertera dem till system av formella regler.
Källa: habr.com
