In my opinion, the topic of formal verification is not sufficiently covered in the Russian-speaking sector of the internet, and there is a particular lack of simple and illustrative examples.
I will provide such an example from a foreign source and complement it with my own solution to the well-known problem of transporting a wolf, a goat, and cabbage across a river.
But first, I will briefly describe what formal verification is and why it is needed.
Formal verification usually refers to the verification of a program or algorithm using another program.
This is necessary to ensure that the behavior of the program matches expectations and to guarantee its security.
Formal verification is the most powerful means of finding and eliminating vulnerabilities: it can identify all existing holes and bugs in a program or prove that none exist.
It is worth noting that in some cases this may be impossible, as in the 8 queens problem with a board width of 1000 cells: everything hinges on algorithmic complexity or the halting problem.
However, in any case, one of three answers will be received: the program is correct, incorrect, or it was not possible to compute the answer.
In cases where finding an answer is impossible, the unclear sections of the program can often be reworked, reducing their algorithmic complexity to achieve a specific yes or no answer.
For example, formal verification is used in the Windows kernel and in the operating systems of Darpa drones to ensure maximum security.
We will use Z3Prover, a very powerful tool for automated theorem proving and equation solving.
Moreover, Z3 specifically solves equations rather than brute-forcing values.
This means it can find answers even in cases where there are combinations of input options totaling 10^100.
This is just about a dozen input arguments of type Integer, which is often encountered in practice.
The 8 queens problem (taken from the English ).
# 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)
Running Z3, we obtain the solution:
[Q_5 = 1,
Q_8 = 7,
Q_3 = 8,
Q_2 = 2,
Q_6 = 3,
Q_4 = 6,
Q_7 = 5,
Q_1 = 4]
The queens problem is comparable to a program that takes the coordinates of 8 queens as input and outputs whether the queens attack each other.
If we were to solve such a problem using formal verification, we would just need to take one additional step of transforming the program code into an equation, which would essentially be identical to ours (of course, provided the program is error-free).
The same will practically happen in the case of searching for vulnerabilities: we simply set the required output conditions, such as the admin password, transform the source or decompiled code into equations compatible with verification, and then determine what input data is needed to achieve the goal.
In my opinion, the problem of the wolf, the goat, and the cabbage is even more interesting, as solving it requires many (7) steps.
If the chess piece problem is comparable to a scenario where one can access the server with a single GET or POST request, then the wolf, goat, and cabbage problem demonstrates an example from a much more complex and common category, where goals can only be achieved with several requests.
This is comparable, for example, to a scenario where one needs to find an SQL injection, use it to write a file, escalate privileges, and only then obtain the password.
Problem conditions and its solutionThe farmer needs to transport the wolf, goat, and cabbage across the river. The farmer has a boat that can only accommodate one object in addition to himself. The wolf will eat the goat, and the goat will eat the cabbage if the farmer leaves them unattended.
The solution lies in the fact that on the 4th step, the farmer needs to take the goat back.
Now, let's proceed to the solution programmatically.
We will designate the farmer, wolf, goat, and cabbage as 4 variables, which can only take the value 0 or 1. Zero means they are on the left bank, and one means they are on the right.
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 is the number of steps required for the solution. Each step represents the state of the river, the boat, and all entities.
For now, let's choose it at random and with a margin, we'll take 10.
Each entity is represented in 10 instances — this is its value at each of the 10 steps.
Now let's set the conditions for start and finish.
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 ]
Next, we'll set the conditions where the wolf eats the goat, or the goat eats the cabbage, as constraints in the equation.
(In the presence of the farmer, aggression is impossible)
# 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) ]
Finally, let's set all possible actions of the farmer when crossing back and forth.
He can take the wolf, the goat, or the cabbage with him, or take no one, or not go anywhere at all.
Of course, without the farmer, no one can cross.
This will be expressed in that each subsequent state of the river, boat, and entities can differ from the previous one only in a strictly limited way.
No more than 2 bits, and with many other limits, since the farmer can only transport one entity at a time and not everyone can be left together.
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) ]
Let's run the solution.
solve(Side + Start + Finish + Safe + Travel)
And we get an answer!
Z3 found a consistent set of states that satisfies all the conditions.
A sort of four-dimensional snapshot of space-time.
Let's figure out what happened.
We see that in the end, everyone crossed over, but initially, our farmer decided to rest and didn't go anywhere in the first 2 steps.
Human_2 = 0
Human_3 = 0
This indicates that we chose an excessive number of states, and 8 will be quite sufficient.
In our case, the farmer acted as follows: start, rest, rest, transporting the goat, returning back, transporting the cabbage, returning with the goat, transporting the wolf, returning back alone, and then delivering the goat again.
But in the end, the problem is solved.
#Старт.
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
Now let's try changing the conditions and prove that there are no solutions.
To do this, we will endow our wolf with herbivorous behavior, and he will want to eat the cabbage.
This can be compared to a case where our goal is application protection, and we must ensure that there are no loopholes.
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 gave us the following response:
no solution
It means that there are indeed no solutions.
Thus, we programmatically proved the impossibility of ferrying with an omnivorous wolf without losses for the farmer.
If the audience finds this topic interesting, in future articles I will explain how to transform an ordinary program or function into a form compatible with formal methods, and solve it, thus discovering both legitimate scenarios and vulnerabilities. Starting with this same problem, but presented as a program, and then gradually complicating and moving on to relevant examples from the software development world.
The next article is already ready:
In it, I transition from formal verification of tasks to programs, and describe how
one can automatically convert them into formal rule systems.
Source: habr.com
