Според мен, в рускоговорещия сектор на интернет темата за формална верификация е недостатъчно обсъдена, особено липсват ясни и нагледни примери.
Ще дам такъв пример от чуждестранен източник и ще допълня със собствено решение на известната задача за прехвърляне на вълка, козата и капустата на другия бряг на реката.
Но първо накратко ще опиша какво представлява формалната верификация и защо е необходима.
Под формалната верификация обикновено се разбира проверка на една програма или алгоритъм с помощта на друга.
Това е необходимо, за да се уверим, че поведението на програмата отговаря на очакваното, а също така да се осигури нейната безопасност.
Формалната верификация е най-мощното средство за намиране и отстраняване на уязвимости: тя позволява да се открият всички съществуващи дупки и бъгове в програмата или да се докаже, че няма такива.
Необходимо е да се отбележи, че в някои случаи това е невъзможно, както например в задачата за 8 ферзи с ширина на дъска 1000 клетки: всичко опира до алгоритмичната сложност или проблема на спиране.
Във всеки случай ще се получи един от трите отговора: програмата е коректна, некоректна или пък — не е било възможно да се пресметне отговорът.
В случай на невъзможност да се намери отговор, често е възможно да се преработят неясните места в програмата, намалявайки тяхната алгоритмична сложност, за да се получи конкретен отговор да или не.
Формалната верификация се прилага например в ядрото на Windows и операционните системи на безпилотници Darpa, за да се осигури максимално ниво на защита.
Ние ще използваме Z3Prover, много мощен инструмент за автоматизирано доказване на теореми и решаване на уравнения.
И Z3 именно решава уравнения, а не подбира техните стойности грубо с брутен форс.
Това означава, че той е способен да намира отговор, дори в случаи, когато комбинациите на входните варианти достигат 10^100.
А всъщност това е само около дузина входни аргументи от тип Integer, и подобно често се среща на практика.
Задачата за 8 ферзи (взета от англоязичния ).
# 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)
Когато стартираме Z3, получаваме решение:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
Задачата за ферзите е сравнима с програма, която приема координатите на 8 ферзи и извежда отговора дали ферзите се нападат един друг.
Ако решавахме програма с помощта на формална верификация, в сравнение с задачата, просто щеше да трябва да направим още една стъпка под формата на преобразуване на кода на програмата в уравнение: по същество то щеше да бъде идентично на нашето (разбира се, ако програмата е написана без грешки).
Практически същото ще се случи и при търсенето на уязвимости: ние просто задаваме необходимите изходни условия, например парола за администратор, преобразуваме оригиналния или декомпилиран код в уравнения, съвместими с верификацията, и след това получаваме отговор на въпроса какви данни трябва да подадем на входа за постигане на целта.
Според мен, задачата с вълка, козата и зеле е дори по-интригуваща, тъй като за нейното решаване са необходими много (7) стъпки.
Ако задачата с ферзите е сравнима с вариант, при който може да се проникне на сървъра с помощта на едно GET или POST запитване, то задачата с вълка, козата и зелето демонстрира пример от много по-сложна и разпространена категория, в която целите могат да бъдат постигнати само с няколко запитвания.
Това е съпоставимо, например, със сценарий, при който трябва да се намери SQL инжекция, да се запише файл чрез нея, след това да се повишат правата и едва след това да се получи паролата.
Условия на задачата и нейното решаванеФермерът трябва да пренесе през реката вълк, коза и зеле. Фермерът има лодка, в която могат да се вместят, освен самия фермер, само един обект. Вълкът ще изяде козата, а козата ще изяде зелето, ако фермерът ги остави без наблюдение.
Решението е в това, че на 4-та стъпка фермерът ще трябва да отведе козата обратно.
Сега ще започнем да решаваме с програма.
Обозначаваме фермера, вълка, козата и зелето като 4 променливи, които могат да приемат стойност само 0 или 1. Нула означава, че са на левия бряг, а единица - че са на десния.
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) ]
# Всяко същество може да бъде само на левия (0) или десния бряг (1) в всяко състояние
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 — това е броят стъпки, необходими за решението. Всяка стъпка представя състояние на реката, лодката и всички същности.
За сега ще го изберем произволно и с резерв, ще вземем 10.
Всяка същност е представена в 10 екземпляра — това е нейното значение на всяка от 10 стъпки.
Сега ще зададем условията за старт и финал.
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 ]
След това ще зададем условия, при които вълкът изяжда козата, или козата — зелето, като ограничения в уравнението.
(В присъствието на фермера агресията е невъзможна)
# 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) ]
И накрая, ще зададем всички възможни действия на фермера при пресяването напред или назад.
Той може да вземе с себе си вълка, козата или зелето, или пък никого да не взима, или изобщо да не пътува.
Разбира се, без фермера никой не може да се прехвърли.
Това ще бъде изразено с факта, че всяко следващо състояние на реката, лодката и съществата може да се различава от предишното само по строго ограничен начин.
Не повече от 2 бита, и с много други ограничения, тъй като фермерът може да прехвърли само едно същество на веднъж и не всички могат да останат заедно.
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) ]
Нека стартираме решението.
solve(Side + Start + Finish + Safe + Travel)
И получаваме отговор!
Z3 намери консистентен и удовлетворяващ всички условия набор от състояния.
Такъв четиримерен отпечатък на пространство-времето.
Нека разберем какво всъщност се е случило.
Виждаме, че в крайна сметка всички преминаха, само че в началото нашият фермер реши да си почине и не плува в първите 2 стъпки.
Human_2 = 0
Human_3 = 0
Това показва, че броят на състоянията, които избрахме, е излишен и 8 ще бъде напълно достатъчни.
В нашия случай фермерът действа по следния начин: старт, почивка, почивка, прехвърляне на козата, прехвърляне обратно, прехвърляне на зелето, връщане с козата, прехвърляне на вълка, връщане обратно сам, повторно пренасяне на козата.
Но в крайна сметка задачата е решена.
#Старт.
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
Сега ще опитаме да променим условията и да докажем, че решения няма.
За това ще надарим нашия вълк с тревопасност и той ще иска да изяде зелето.
Това може да се сравни с ситуация, в която целта ни е защитата на приложението и трябва да се уверим, че няма пробиви.
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 ни даде следния отговор:
няма решение
Той означава, че наистина няма решения.
По този начин програмно доказахме невъзможността за пренос с всеядния вълк, без загуби за фермера.
Ако аудиторията намери тази тема интересна, в следващите статии ще разкажа как да превърнем обикновена програма или функция в съвместимо с формалните методи уравнение и да го решим, откривайки по този начин както легитимни сценарии, така и уязвимости. Първо на същата задача, но представена в програмен вид, а след това постепенно ще усложняваме и ще преминем към актуални примери от света на софтуерната разработка.
Следващата статия вече е готова:
В нея преминавам от формалната верификация на задачи към програми и описвам,
по какъв начин могат да се конвертират в системи на формални правила автоматично.
Източник: habr.com
