Moim zdaniem temat formalnej weryfikacji w rosyjskojęzycznej przestrzeni internetowej jest niewystarczająco omawiany, a szczególnie brakuje prostych i obrazowych przykładów.
Podam przykład z zagranicznego źródła i uzupełnię własnym rozwiązaniem znanego zadania o przewozie wilka, kozy i kapusty na drugą stronę rzeki.
Jednak najpierw krótko opiszę, czym jest formalna weryfikacja i dlaczego jest potrzebna.
Formalna weryfikacja zazwyczaj oznacza sprawdzenie jednego programu lub algorytmu za pomocą innego.
Jest to potrzebne, aby upewnić się, że zachowanie programu odpowiada oczekiwaniom, a także zapewnić jego bezpieczeństwo.
Formalna weryfikacja jest najpotężniejszym narzędziem do wykrywania i usuwania podatności: pozwala znaleźć wszystkie istniejące błędy i luki w programie, lub dowieść, że ich nie ma.
Warto zauważyć, że w niektórych przypadkach jest to niemożliwe, jak na przykład w zadaniu o 8 hetmanach na planszy szerokiej na 1000 pól: wszystko sprowadza się do złożoności algorytmicznej lub problemu zatrzymywania.
Jednak w każdym przypadku otrzymuje się jedną z trzech odpowiedzi: program jest poprawny, niepoprawny lub - nie udało się obliczyć odpowiedzi.
W przypadku braku możliwości znalezienia odpowiedzi, często można przerobić niejasne fragmenty programu, zmniejszając ich złożoność algorytmiczną, aby uzyskać konkretną odpowiedź tak lub nie.
Formalna weryfikacja jest stosowana na przykład w jądrze systemu Windows i systemach operacyjnych dronów Darpa, aby zapewnić maksymalny poziom ochrony.
Będziemy korzystać z Z3Prover, bardzo potężnego narzędzia do zautomatyzowanego dowodzenia twierdzeń i rozwiązywania równań.
Z3 rzeczywiście rozwiązuje równania, a nie szuka ich wartości metodą brutalnego przeszukiwania.
Oznacza to, że jest w stanie znaleźć odpowiedź, nawet w przypadkach, gdy liczba kombinacji wejściowych wynosi 10^100.
A to zaledwie około tuzina argumentów wejściowych typu Integer, co często występuje w praktyce.
Zadanie o 8 hetmanach (czerpane z anglojęzycznego ).
# 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)
Uruchamiając Z3, otrzymujemy rozwiązanie:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Zadanie o hetmanach porównywalne jest z programem, który przyjmuje współrzędne 8 hetmanów i zwraca odpowiedź, czy hetmany się biją.
Gdybyśmy podeszli do tego programu przy pomocy formalnej weryfikacji, w porównaniu do zadania, potrzebowalibyśmy po prostu wykonać jeszcze jeden krok w postaci przekształcenia kodu programu w równanie: w istocie byłoby ono identyczne z naszym (oczywiście, o ile program został napisany bez błędów).
Podobnie będzie w przypadku poszukiwania luk: określamy tylko wymagane warunki wyjściowe, na przykład hasło admina, przekształcamy oryginalny lub zdekompilowany kod w równania zgodne z weryfikacją, a następnie uzyskujemy odpowiedź na to, jakie dane należy podać na wejściu, aby osiągnąć cel.
Moim zdaniem, zadanie o wilku, kozie i kapuście jest jeszcze ciekawsze, ponieważ do jego rozwiązania potrzebne są już liczne (7) kroki.
Jeśli zadanie o hetmanach porównać do sytuacji, w której można uzyskać dostęp do serwera przy pomocy jednego żądania GET lub POST, to wilk, koza i kapusta ilustruje przykład znacznie bardziej skomplikowanej i powszechnej kategorii, w której cele można osiągnąć tylko za pomocą kilku żądań.
To porównywalne, na przykład, ze scenariuszem, w którym należy znaleźć SQL injection, zapisać przez nią plik, a następnie podnieść swoje uprawnienia i dopiero potem uzyskać hasło.
Warunki zadania i jego rozwiązanieRolnik musi przewieźć przez rzekę wilka, kozę i kapustę. Rolnik ma łódź, która może pomieścić, oprócz samego rolnika, tylko jeden obiekt. Wilk zje kozę, a koza zje kapustę, jeśli rolnik zostawi je bez opieki.
Rozwiązanie polega na tym, że na czwartym kroku rolnik musi przewieźć kozę z powrotem.
Teraz przystąpmy do rozwiązania w sposób programistyczny.
Oznaczmy rolnika, wilka, kozę i kapustę jako 4 zmienne, które przyjmują wartość tylko 0 lub 1. Zero oznacza, że są na lewym brzegu, a jeden - że są na prawym.
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) ]
# Każda istota może być tylko po lewej (0) lub prawej stronie (1) w każdym stanie
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 — to liczba kroków potrzebnych do rozwiązania. Każdy krok reprezentuje stan rzeki, łodzi i wszystkich istot.
Na razie wybierzemy go losowo i z zapasem, weźmiemy 10.
Każda istota jest reprezentowana w 10 egzemplarzach — to jej wartość na każdym z 10 kroków.
Teraz ustalimy warunki dla startu i mety.
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 ]
Następnie ustalimy warunki, w których wilk zjada kozę lub koza kapustę, jako ograniczenia w równaniu.
(W obecności rolnika agresja jest niemożliwa)
# 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) ]
Wreszcie ustalimy wszystkie możliwe działania rolnika podczas przewozu w obie strony.
Może zabrać ze sobą wilka, kozę lub kapustę, lub nikogo nie zabierać, lub w ogóle nie płynąć.
Oczywiście, bez rolnika nikt nie może się przeprawić.
Będzie to wyrażone tym, że każde następne stan rzeki, łodzi i istot może różnić się od poprzedniego tylko w ściśle ograniczony sposób.
Nie więcej niż o 2 bity, i z wieloma innymi ograniczeniami, ponieważ rolnik może przewieźć na raz tylko jedną istotę i nie można zostawić wszystkich razem.
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) ]
Uruchomimy rozwiązanie.
solve(Side + Start + Finish + Safe + Travel)
I otrzymujemy odpowiedź!
Z3 znalazł niesprzeczny, spełniający wszystkie warunki zbiór stanów.
Taki czterowymiarowy odcisk czasoprzestrzeni.
Zobaczmy, co się stało.
Widzimy, że w końcu wszyscy się przeprawili, ale na początku nasz rolnik postanowił odpocząć i przez pierwsze 2 kroki nigdzie nie płynął.
Human_2 = 0
Human_3 = 0
To wskazuje, że wybraliśmy nadmiarową liczbę stanów, a 8 będzie wystarczające.
W naszym przypadku rolnik postąpił w ten sposób: start, odpoczynek, odpoczynek, przeprawa kozy, przeprawa z powrotem, przeprawa kapusty, powrót z kozą, przeprawa wilka, powrót z powrotem sam, ponowna dostawa kozy.
Ale ostatecznie zadanie zostało rozwiązane.
#Старт.
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
Teraz spróbujmy zmienić warunki i udowodnić, że nie ma rozwiązań.
W tym celu nadamy naszemu wilkowi roślinożerność i będzie chciał zjeść kapustę.
Można to porównać do sytuacji, w której naszym celem jest ochrona aplikacji, a my musimy upewnić się, że nie ma żadnych luk.
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 zwrócił nam następującą odpowiedź:
brak rozwiązania
Oznacza to, że rzeczywiście nie ma rozwiązań.
W ten sposób programowo udowodniliśmy niemożność przetransportowania z omnibusem wilkiem, bez strat dla farmera.
Jeśli odbiorcy uznają ten temat za interesujący, w kolejnych artykułach opowiem, jak przekształcić zwykły program lub funkcję w zgodne z formalnymi metodami równanie i je rozwiązać, odkrywając tym samym zarówno wszystkie legalne scenariusze, jak i luki. Najpierw na tym samym zadaniu, ale przedstawionym już w postaci programu, a następnie stopniowo komplikując i przechodząc do bieżących przykładów z obszaru rozwoju oprogramowania.
Kolejny artykuł jest już gotowy:
W nim przechodzę od formalnej weryfikacji zadań do programów i opisuję,
w jaki sposób można je automatycznie konwertować na systemy formalnych reguł.
Źródło: habr.com
