Формальная верификация на примере задачи о волке, козе и капусте

На мой взгляд, в русскоязычном секторе интернета тематика формальной верификации освещена недостаточно, и особенно не хватает простых и наглядных примеров.

Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую сторону реки.

Но вначале вкратце опишу, что из себя представляет формальная верификация и зачем она нужна.

Под формальной верификацией обычно понимают проверку одной программы либо алгоритма с помощью другой.

Это нужно для того, чтобы удостовериться, что поведение программы соответствует ожидаемому, а также обеспечить её безопасность.

Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
Стоит заметить, что в некоторых случаях это бывает невозможно, как например, в задаче о 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 переменные, которые принимают значение только 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

Он означает, что решений действительно нет.

Таким образом мы программным способом доказали невозможность переправы со всеядным волком, без потерь для фермера.

Если аудитория сочтёт эту тематику интересной, то в дальнейших статьях я расскажу, как превратить обычную программу или функцию в совместимое с формальными методами уравнение, и решить его, обнаружив тем самым как все легитимные сценарии, так и уязвимости. Сначала на этой же задаче, но представленной уже в виде программы, а затем постепенно усложняя и переходя к актуальным примерам из мира разработки ПО.

Автор: smart77

Источник