На мій погляд, у російськомовному секторі інтернету тематика формальної верифікації висвітлена недостатньо, і особливо не вистачає простих та наочних прикладів.
Я наведу такий приклад із зарубіжного джерела, і доповню власним рішенням відомого завдання про переправу вовка, кози та капусти на інший бік річки.
Але спочатку коротко опишу, що собою представляє формальна верифікація і навіщо вона потрібна.
Під формальної верифікацією зазвичай розуміють перевірку однієї програми чи алгоритму з допомогою інший.
Це потрібно для того, щоб переконатися, що поведінка програми відповідає очікуваному, а також забезпечити її безпеку.
Формальна верифікація є найпотужнішим засобом пошуку та усунення вразливостей: вона дозволяє знайти всі існуючі дірки та баги у програмі, або ж довести, що їх немає.
Варто зауважити, що в деяких випадках це буває неможливо, як, наприклад, у задачі про 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 знайшов несуперечливу, і задовольняє всім умовам сукупність станів.
Такий собі чотиривимірний зліпок простору-часу.
Давайте розберемося, що сталося.
Ми бачимо, що в результаті всі переправилися, ось тільки спочатку наш фермер вирішив відпочити, і нікуди на перших двох кроках не пливе.
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
Він означає, що рішень справді немає.
Таким чином, ми програмним способом довели неможливість переправи з всеїдним вовком, без втрат для фермера.
Якщо аудиторія визнає цю тематику цікавою, то в подальших статтях я розповім, як перетворити звичайну програму або функцію на сумісне з формальними методами рівняння, і вирішити його, виявивши тим самим як усі легітимні сценарії, так і вразливості. Спочатку на цій же задачі, але представленої вже у вигляді програми, а потім поступово ускладнюючи та переходячи до актуальних прикладів зі світу розробки ПЗ.
Наступна стаття вже готова:
У ній я переходжу від формальної верифікації завдань, до програм і описую,
як можна конвертувати в системи формальних правил автоматично.
Джерело: habr.com