Moim zdaniem w rosyjskojęzycznym sektorze Internetu temat weryfikacji formalnej nie jest wystarczająco omówiony, a zwłaszcza brakuje prostych i jasnych przykładów.
Podam przykład z zagranicznego źródła i dodam własne rozwiązanie znanego problemu przeprawy wilka, kozy i kapusty na drugą stronę rzeki.
Najpierw jednak krótko opiszę, czym jest weryfikacja formalna i dlaczego jest potrzebna.
Weryfikacja formalna zwykle oznacza sprawdzenie jednego programu lub algorytmu przy użyciu innego.
Jest to konieczne, aby program działał zgodnie z oczekiwaniami, a także aby zapewnić jego bezpieczeństwo.
Formalna weryfikacja jest najpotężniejszą metodą wyszukiwania i eliminowania luk: pozwala znaleźć wszystkie istniejące dziury i błędy w programie lub udowodnić, że one nie istnieją.
Warto zauważyć, że w niektórych przypadkach jest to niemożliwe, jak np. w zadaniu 8 hetmanów o szerokości planszy 1000 kwadratów: wszystko sprowadza się do złożoności algorytmicznej lub problemu zatrzymania.
Jednak w każdym przypadku otrzymana zostanie jedna z trzech odpowiedzi: program jest poprawny, błędny lub nie można było obliczyć odpowiedzi.
Jeśli nie da się znaleźć odpowiedzi, często można przerobić niejasne fragmenty programu, zmniejszając ich złożoność algorytmiczną, aby uzyskać konkretną odpowiedź tak lub nie.
A weryfikacja formalna stosowana jest na przykład w jądrze Windows i systemach operacyjnych dronów Darpa, aby zapewnić maksymalny poziom ochrony.
Będziemy używać Z3Prover, bardzo potężnego narzędzia do automatycznego dowodzenia twierdzeń i rozwiązywania równań.
Co więcej, Z3 rozwiązuje równania, a nie dobiera ich wartości za pomocą brutalnej siły.
Oznacza to, że jest w stanie znaleźć odpowiedź, nawet w przypadkach, gdy istnieje 10^100 kombinacji opcji wejściowych.
Ale to tylko kilkanaście argumentów wejściowych typu Integer i często spotyka się to w praktyce.
Problem dotyczący 8 królowych (zaczerpnięte z języka angielskiego ).
# 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]
Problem królowej można porównać do programu, który jako dane wejściowe pobiera współrzędne 8 królowych i podaje odpowiedź, czy królowe się biją.
Gdybyśmy mieli rozwiązać taki program za pomocą weryfikacji formalnej, to w porównaniu z problemem musielibyśmy po prostu zrobić jeszcze jeden krok w postaci przekształcenia kodu programu w równanie: okazałoby się, że jest on w zasadzie identyczny z naszym ( oczywiście, jeśli program został napisany poprawnie).
Prawie to samo stanie się w przypadku wyszukiwania podatności: po prostu ustawiamy potrzebne nam warunki wyjściowe, np. hasło administratora, przekształcamy kod źródłowy lub dekompilowany na równania zgodne z weryfikacją, a następnie otrzymujemy odpowiedź, co dane muszą zostać dostarczone jako dane wejściowe, aby osiągnąć cel.
Moim zdaniem problem wilka, kozy i kapusty jest jeszcze ciekawszy, gdyż jego rozwiązanie wymaga już wielu (7) kroków.
Jeśli problem królowej jest porównywalny do przypadku, w którym można przeniknąć do serwera za pomocą pojedynczego żądania GET lub POST, to wilk, koza i kapusta demonstrują przykład z kategorii znacznie bardziej złożonej i powszechnej, w której cel można osiągnąć jedynie przez kilka próśb.
Można to porównać na przykład do scenariusza, w którym trzeba znaleźć zastrzyk SQL, zapisać przez niego plik, następnie podnieść swoje uprawnienia i dopiero wtedy uzyskać hasło.
Warunki problemu i jego rozwiązanieRolnik musi przewieźć przez rzekę wilka, kozę i kapustę. Rolnik ma łódź, która może pomieścić tylko jeden przedmiot, oprócz samego rolnika. Wilk zje kozę, a koza zje kapustę, jeśli rolnik zostawi je bez opieki.
Rozwiązaniem jest to, że w kroku 4 rolnik będzie musiał zabrać kozę z powrotem.
Teraz zacznijmy rozwiązywać to programowo.
Oznaczmy rolnika, wilka, kozę i kapustę jako 4 zmienne, które przyjmują tylko wartość 0 lub 1. Zero oznacza, że są na lewym brzegu, a jeden oznacza, ż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) ]
# 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
Liczba to liczba kroków wymaganych do rozwiązania. Każdy krok reprezentuje stan rzeki, łodzi i wszystkich bytów.
Na razie wybierzmy to losowo i z marginesem weźmy 10.
Każdy byt jest reprezentowany w 10 egzemplarzach – taka jest jego wartość na każdym z 10 kroków.
Teraz ustalmy warunki 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 ustalamy warunki, w których wilk zjada kozę lub koza zjada 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) ]
Na koniec zdefiniujemy wszystkie możliwe działania rolnika podczas przejazdu tam lub z powrotem.
Może albo zabrać ze sobą wilka, kozę, albo kapustę, albo nikogo nie zabrać, albo w ogóle nigdzie nie pływać.
Oczywiście nikt nie może przejść bez rolnika.
Wyrazem tego będzie fakt, że każdy kolejny stan rzeki, łodzi i bytów może różnić się od poprzedniego jedynie w ściśle ograniczony sposób.
Nie więcej niż 2 bity i z wieloma innymi ograniczeniami, ponieważ rolnik może przewozić tylko jedną jednostkę na raz i nie można wszystkich zostawić 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) ]
Uruchommy rozwiązanie.
solve(Side + Start + Finish + Safe + Travel)
I otrzymaliśmy odpowiedź!
Z3 znalazł spójny zbiór stanów, który spełnia wszystkie warunki.
Rodzaj czterowymiarowego rzutu czasoprzestrzeni.
Zastanówmy się, co się stało.
Widzimy, że w końcu wszyscy przeszli, tylko na początku nasz rolnik postanowił odpocząć, a na pierwszych 2 stopniach nigdzie nie pływał.
Human_2 = 0
Human_3 = 0
Sugeruje to, że liczba wybranych przez nas państw jest nadmierna i 8 będzie w zupełności wystarczające.
W naszym przypadku rolnik zrobił tak: start, odpoczynek, odpoczynek, przejście przez kozę, przejście z powrotem, przejście przez kapustę, powrót z kozą, przejście przez wilka, powrót sam, ponowne dostarczenie kozy.
Ale w końcu problem został rozwiązany.
#Старт.
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
Spróbujmy teraz zmienić warunki i udowodnić, że nie ma rozwiązań.
Aby to zrobić, damy naszemu wilkowi roślinożercę, a on będzie chciał jeść kapustę.
Można to porównać do przypadku, w którym naszym celem jest zabezpieczenie aplikacji i musimy zadbać o to, aby nie było w niej 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 dał nam następującą odpowiedź:
no solution
Oznacza to, że tak naprawdę nie ma rozwiązań.
W ten sposób programowo udowodniliśmy niemożność skrzyżowania się z wszystkożernym wilkiem bez strat dla rolnika.
Jeśli odbiorcy uznają ten temat za interesujący, w przyszłych artykułach powiem, jak zamienić zwykły program lub funkcję w równanie zgodne z metodami formalnymi i rozwiązać je, ujawniając w ten sposób zarówno wszystkie uzasadnione scenariusze, jak i luki. Najpierw na tym samym zadaniu, ale przedstawionym w formie programu, a następnie stopniowo je komplikując i przechodząc do aktualnych przykładów ze świata tworzenia oprogramowania.
Kolejny artykuł jest już gotowy:
Przechodzę w nim od formalnej weryfikacji problemów do programów i opisu
w jaki sposób można je automatycznie przekształcić w formalne systemy reguł.
Źródło: www.habr.com