Според мен в рускоезичния сектор на Интернет темата за формалната проверка не е достатъчно засегната и особено липсват прости и ясни примери.
Ще дам пример от чуждестранен източник и ще добавя свое собствено решение на добре познатия проблем с преминаването на вълк, коза и зеле от другата страна на реката.
Но първо ще опиша накратко какво представлява формалната проверка и защо е необходима.
Официалната проверка обикновено означава проверка на една програма или алгоритъм с помощта на друга.
Това е необходимо, за да се гарантира, че програмата се държи според очакванията, както и за да се гарантира нейната сигурност.
Официалната проверка е най-мощното средство за намиране и елиминиране на уязвимости: тя ви позволява да намерите всички съществуващи дупки и грешки в програма или да докажете, че те не съществуват.
Струва си да се отбележи, че в някои случаи това е невъзможно, като например при проблема с 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) ]
# 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 е броят стъпки, необходими за решаване. Всяка стъпка представлява състоянието на реката, лодката и всички обекти.
Засега нека го изберем на случаен принцип и с марж, вземете 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 ни даде следния отговор:
no solution
Това означава, че наистина няма решения.
Така програмно доказахме невъзможността за кръстосване с всеяден вълк без загуби за фермера.
Ако аудиторията намери тази тема за интересна, тогава в бъдещи статии ще ви кажа как да превърнете обикновена програма или функция в уравнение, съвместимо с формални методи, и да го решите, като по този начин разкриете както всички законни сценарии, така и уязвимости. Първо върху същата задача, но представена под формата на програма, а след това постепенно я усложнявайки и преминавайки към актуални примери от света на разработката на софтуер.
Следващата статия вече е готова:
В него преминавам от формална проверка на проблеми към програми и описвам
как можете автоматично да ги конвертирате в системи от формални правила.
Източник: www.habr.com