April 22, 2019 at 15:42Formal verification on the example of the wolf, goat and cabbage problem
In my opinion, in the Russian-speaking sector of the Internet, the topic of formal verification is not sufficiently covered, and especially simple and clear examples are lacking.
I will give such an example from a foreign source, and supplement my own solution to the well-known problem of transporting a wolf, goat and cabbage to the other side of the river.
But first, I will briefly describe what formal verification is and why it is needed.
Formal verification usually means checking one program or algorithm using another.
This is necessary in order to make sure that the behavior of the program is as expected, and also to ensure its safety.
Formal verification is the most powerful means of finding and eliminating vulnerabilities: it allows you to find all existing holes and bugs in the program, or to prove that they are not there.
It is worth noting that in some cases this is impossible, such as in the problem of 8 queens with a board width of 1000 cells: everything depends on algorithmic complexity or the problem of stopping.
However, in any case, one of the three answers will be received: the program is correct, incorrect, or the answer could not be calculated.
If it is impossible to find an answer, it is often possible to rework obscure places in the program, reducing their algorithmic complexity in order to get a specific answer, yes or no.
And formal verification is used, for example, in the Windows kernel and Darpa drones operating systems, to provide the maximum level of protection.
We will use Z3Prover, a very powerful tool for automated proof of theorems and solving equations.
Moreover, Z3 exactly solves the equations, and does not select their values with brute force.
This means that he is able to find the answer, even in cases where combinations of input options and 10 ^ 100.
But this is only about a dozen input arguments of type Integer, and this is often found in practice.
The problem of 8 queens (Taken from the English manual ).
Running Z3, we get the solution:
The queen problem is comparable to a program that takes in the coordinates of 8 queens and displays the answer if the queens beat each other.
If we were to solve such a program using formal verification, then compared to the task, we would just need to take another step in the form of converting the program code into an equation: it would turn out to be essentially identical to ours (of course, if the program was written correctly).
Almost the same thing will happen when searching for vulnerabilities: we only set the output conditions that we need, for example, the admin password, convert the source or decompiled code into equations compatible with verification, and then we get the answer what data needs to be input to achieve the goal.
In my opinion, the problem of the wolf, goat and cabbage is even more interesting, since many (7) steps are already needed to solve it.
If the queen problem is comparable to the option when you can penetrate the server using one GET or POST request, then the wolf, goat and cabbage demonstrate an example from a much more complex and widespread category in which only a few requests can be reached.
This is comparable, for example, with the scenario where you need to find the SQL injection, write a file through it, then increase your rights and only then get the password.
Now let's start the solution programmatically.
We designate the farmer, the wolf, the goat and the cabbage as 4 variables, which take the value only 0 or 1. Zero means that they are on the left bank, and one means that on the right.
Num is the number of steps needed to solve. Each step is a state of a river, boat and all entities.
For now, choose it at random and with a margin, take 10.
Each entity is presented in 10 copies - this is its value at each of 10 steps.
Now we set the conditions for start and finish.
Then we set the conditions where the wolf eats the goat, or goat cabbage, as restrictions in the equation.
(In the presence of the farmer, aggression is not possible)
And finally, we ask all the possible actions of the farmer when moving there or back.
He can either take a wolf, a goat or a cabbage with him, or take no one, or even not go anywhere.
Of course, no one can cross without a farmer.
This will be expressed by the fact 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 all can be left together.
Run the solution.
And we get the answer!
Z3 found a consistent and satisfying set of conditions.
A kind of four-dimensional cast of space-time.
Let's see what happened.
We see that in the end everyone crossed, only at the beginning our farmer decided to relax, and does not swim anywhere in the first 2 steps.
This suggests that the number of states we have chosen is excessive, and 8 will be quite enough.
In our case, the farmer did this: start, rest, rest, crossing the goat, crossing back, crossing the cabbage, returning with the goat, crossing the wolf, returning back alone, re-delivering the goat.
But in the end, the problem is solved.
Now let's try to change the conditions and prove that there are no solutions.
To do this, we will endow our wolf with herbivore, and he will want to eat cabbage.
This can be compared to the case in which our goal is to protect the application and we need to make sure that there are no loopholes.
Z3 gave us the following answer:
It means that there really are no solutions.
Thus, we have programmatically proved the impossibility of crossing with an omnivorous wolf, without losses for the farmer.
If the audience finds this topic interesting, then in future articles I will tell you how to turn an ordinary program or function into an equation compatible with formal methods and solve it, thereby revealing both all legitimate scenarios and vulnerabilities. First, on the same task, but presented already in the form of a program, and then gradually complicating and moving on to relevant examples from the world of software development.
The following article is already ready:
Creating a formal verification system from scratch: We write a symbolic VM in PHP and Python.
In it, I move from formal verification of tasks to programs, and describe
how to convert them into formal rule systems automatically.
I will give such an example from a foreign source, and supplement my own solution to the well-known problem of transporting a wolf, goat and cabbage to the other side of the river.
But first, I will briefly describe what formal verification is and why it is needed.
Formal verification usually means checking one program or algorithm using another.
This is necessary in order to make sure that the behavior of the program is as expected, and also to ensure its safety.
Formal verification is the most powerful means of finding and eliminating vulnerabilities: it allows you to find all existing holes and bugs in the program, or to prove that they are not there.
It is worth noting that in some cases this is impossible, such as in the problem of 8 queens with a board width of 1000 cells: everything depends on algorithmic complexity or the problem of stopping.
However, in any case, one of the three answers will be received: the program is correct, incorrect, or the answer could not be calculated.
If it is impossible to find an answer, it is often possible to rework obscure places in the program, reducing their algorithmic complexity in order to get a specific answer, yes or no.
And formal verification is used, for example, in the Windows kernel and Darpa drones operating systems, to provide the maximum level of protection.
We will use Z3Prover, a very powerful tool for automated proof of theorems and solving equations.
Moreover, Z3 exactly solves the equations, and does not select their values with brute force.
This means that he is able to find the answer, even in cases where combinations of input options and 10 ^ 100.
But this is only about a dozen input arguments of type Integer, and this is often found in practice.
The problem of 8 queens (Taken from the English manual ).
# 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 get 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 queen problem is comparable to a program that takes in the coordinates of 8 queens and displays the answer if the queens beat each other.
If we were to solve such a program using formal verification, then compared to the task, we would just need to take another step in the form of converting the program code into an equation: it would turn out to be essentially identical to ours (of course, if the program was written correctly).
Almost the same thing will happen when searching for vulnerabilities: we only set the output conditions that we need, for example, the admin password, convert the source or decompiled code into equations compatible with verification, and then we get the answer what data needs to be input to achieve the goal.
In my opinion, the problem of the wolf, goat and cabbage is even more interesting, since many (7) steps are already needed to solve it.
If the queen problem is comparable to the option when you can penetrate the server using one GET or POST request, then the wolf, goat and cabbage demonstrate an example from a much more complex and widespread category in which only a few requests can be reached.
This is comparable, for example, with the scenario where you need to find the SQL injection, write a file through it, then increase your rights and only then get the password.
Problem conditions and its solution
The farmer needs to transport the wolf, goat and cabbage across the river. The farmer has a boat in which only one object can fit, except for the peasant himself. The wolf will eat the goat, and the goat will eat cabbage if the farmer leaves them unattended.
The solution is that in step 4, the farmer will need to take the goat back.
The solution is that in step 4, the farmer will need to take the goat back.
Now let's start the solution programmatically.
We designate the farmer, the wolf, the goat and the cabbage as 4 variables, which take the value only 0 or 1. Zero means that they are on the left bank, and one means that 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 needed to solve. Each step is a state of a river, boat and all entities.
For now, choose it at random and with a margin, take 10.
Each entity is presented in 10 copies - this is its value at each of 10 steps.
Now we 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 ]
Then we set the conditions where the wolf eats the goat, or goat cabbage, as restrictions in the equation.
(In the presence of the farmer, aggression is not possible)
# 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) ]
And finally, we ask all the possible actions of the farmer when moving there or back.
He can either take a wolf, a goat or a cabbage with him, or take no one, or even not go anywhere.
Of course, no one can cross without a farmer.
This will be expressed by the fact 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 all 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) ]
Run the solution.
solve(Side + Start + Finish + Safe + Travel)
And we get the answer!
Z3 found a consistent and satisfying set of conditions.
A kind of four-dimensional cast of space-time.
Let's see what happened.
We see that in the end everyone crossed, only at the beginning our farmer decided to relax, and does not swim anywhere in the first 2 steps.
Human_2 = 0
Human_3 = 0
This suggests that the number of states we have chosen is excessive, and 8 will be quite enough.
In our case, the farmer did this: start, rest, rest, crossing the goat, crossing back, crossing the cabbage, returning with the goat, crossing the wolf, returning back alone, re-delivering the goat.
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 to change the conditions and prove that there are no solutions.
To do this, we will endow our wolf with herbivore, and he will want to eat cabbage.
This can be compared to the case in which our goal is to protect the application and we need to make sure 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 answer:
no solution
It means that there really are no solutions.
Thus, we have programmatically proved the impossibility of crossing with an omnivorous wolf, without losses for the farmer.
If the audience finds this topic interesting, then in future articles I will tell you how to turn an ordinary program or function into an equation compatible with formal methods and solve it, thereby revealing both all legitimate scenarios and vulnerabilities. First, on the same task, but presented already in the form of a program, and then gradually complicating and moving on to relevant examples from the world of software development.
The following article is already ready:
Creating a formal verification system from scratch: We write a symbolic VM in PHP and Python.
In it, I move from formal verification of tasks to programs, and describe
how to convert them into formal rule systems automatically.