Formal verification using the wolf, goat and cabbage problem
In my opinion, in the Russian-speaking sector of the Internet, the subject of formal verification is not sufficiently covered, and especially there are not enough simple and clear examples.
I will give such an example from a foreign source, and I will supplement with my own solution the well-known problem of crossing a wolf, a goat and a cabbage to the other side of a river.
But first I will briefly describe what formal verification is and why it is needed.
')
Formal verification is usually understood as checking one program or algorithm with the help of another.
This is necessary in order to make sure that the behavior of the program is as expected and to ensure its safety.
Formal verification is the most powerful tool for finding and fixing vulnerabilities: it allows you to find all existing holes and bugs in the program, or to prove that they are not.
It is worth noting that in some cases it is impossible, as for example, in the problem of 8 queens with a board width of 1000 cells: everything depends on the 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 it was not possible to calculate the answer.
If it is impossible to find the answer, it is often possible to rework the obscure parts of the program, reducing their algorithmic complexity in order to get a specific answer yes or no.
A formal verification is used, for example, in the Windows kernel and Darpa drone operating systems to ensure the maximum level of protection.
We will use Z3Prover, a very powerful tool for automated proof of theorems and solving equations.
Moreover, Z3 solves the equations, and does not select their values with coarse brute force.
This means that it is able to find the answer, even in cases where combinations of input variants and 10 ^ 100.
But this is only about a dozen Integer input arguments, and this is often the case in practice.
The task of 8 queens (Taken from the English manual ).
Running Z3, we get the solution:
The problem of queens is comparable to a program that takes the coordinates of 8 queens as input and displays the answer whether the queens beat each other.
If we solved such a program with the help of formal verification, then compared to the task, we would just need to take one more step in the form of converting the program code into the equation: it would turn out to be essentially identical to ours (of course, if the program was written correctly).
Practically the same thing will happen if we look for vulnerabilities: we just set the output conditions we need, for example, the admin password, convert the source or decompiled code into equations compatible with verification, and then we get an answer about what data we need to submit to the input to achieve the goal.
In my opinion, the problem of wolf, goat and cabbage is even more interesting, since many (7) steps are needed to solve it.
If the problem of queens is comparable to the option when you can get to the server with one GET or POST request, wolf, goat and cabbage show an example from a much more complex and common category in which goals can be achieved only with a few requests.
This is comparable, for example, with a script where you need to find a SQL injection, write a file through it, then elevate your rights and then get a password.
Now let's get to the solution programmatically.
We denote a farmer, a wolf, a goat and a cabbage as 4 variables that take the value of only 0 or 1. Zero means that they are on the left bank, and one means that they are on the right bank.
Num is the number of steps required to solve. Each step represents the state of a river, a boat, and all entities.
So far, we choose it at random and with a margin, take 10.
Each entity is presented in 10 copies - this is its value in each of the 10 steps.
Now let's set the conditions for the start and finish.
Then we set the conditions where the wolf eats the goat, or goat cabbage, as constraints in the equation.
(In the presence of a farmer aggression is impossible)
And finally, we will set all possible actions of the farmer when crossing there or back.
He can either take a wolf, a goat or cabbage, or not take anyone, or not swim at all.
Of course, no one can cross without a farmer.
This will be expressed by the fact that each next 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 transport only 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 all conditions set of states.
A kind of four-dimensional cast of space-time.
Let's see what happened.
We see that in the end everything was ferried, only at the beginning our farmer decided to rest, and did not swim anywhere in the first 2 steps.
This suggests that the number of states we have chosen is redundant, 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 cabbage, returning back alone, crossing the wolf.
But in the end the problem is solved.
Now we will try to change the conditions and prove that there are no solutions.
To do this, we will give our wolf herbivores, and now he wants to eat cabbage.
This can be compared with the case in which our goal is to protect the application and we must make sure that there are no loopholes.
Z3 Gave us the following answer:
It means that there really is no solution.
Thus, we programmatically proved the impossibility of crossing with an omnivorous wolf, without loss for the farmer.
If the audience finds this topic interesting, I will tell you in future articles how to turn an ordinary program or function into an equation compatible with formal methods, and solve it, thus finding both all legitimate scenarios and vulnerabilities. First, on the same task, but presented in the form of a program, and then gradually complicating and moving on to actual examples from the world of software development.
I will give such an example from a foreign source, and I will supplement with my own solution the well-known problem of crossing a wolf, a goat and a cabbage to the other side of a river.
But first I will briefly describe what formal verification is and why it is needed.
')
Formal verification is usually understood as checking one program or algorithm with the help of another.
This is necessary in order to make sure that the behavior of the program is as expected and to ensure its safety.
Formal verification is the most powerful tool for finding and fixing vulnerabilities: it allows you to find all existing holes and bugs in the program, or to prove that they are not.
It is worth noting that in some cases it is impossible, as for example, in the problem of 8 queens with a board width of 1000 cells: everything depends on the 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 it was not possible to calculate the answer.
If it is impossible to find the answer, it is often possible to rework the obscure parts of the program, reducing their algorithmic complexity in order to get a specific answer yes or no.
A formal verification is used, for example, in the Windows kernel and Darpa drone operating systems to ensure the maximum level of protection.
We will use Z3Prover, a very powerful tool for automated proof of theorems and solving equations.
Moreover, Z3 solves the equations, and does not select their values with coarse brute force.
This means that it is able to find the answer, even in cases where combinations of input variants and 10 ^ 100.
But this is only about a dozen Integer input arguments, and this is often the case in practice.
The task 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 problem of queens is comparable to a program that takes the coordinates of 8 queens as input and displays the answer whether the queens beat each other.
If we solved such a program with the help of formal verification, then compared to the task, we would just need to take one more step in the form of converting the program code into the equation: it would turn out to be essentially identical to ours (of course, if the program was written correctly).
Practically the same thing will happen if we look for vulnerabilities: we just set the output conditions we need, for example, the admin password, convert the source or decompiled code into equations compatible with verification, and then we get an answer about what data we need to submit to the input to achieve the goal.
In my opinion, the problem of wolf, goat and cabbage is even more interesting, since many (7) steps are needed to solve it.
If the problem of queens is comparable to the option when you can get to the server with one GET or POST request, wolf, goat and cabbage show an example from a much more complex and common category in which goals can be achieved only with a few requests.
This is comparable, for example, with a script where you need to find a SQL injection, write a file through it, then elevate your rights and then get a password.
Problem conditions and its solution
A farmer needs to transport a wolf, a goat and a cabbage across the river. The farmer has a boat in which only one object can fit, in addition to the peasant himself. A wolf will eat a goat and a goat will eat cabbage if the farmer leaves them unattended.
The answer is that at step 4, the farmer will need to take the goat back.
The answer is that at step 4, the farmer will need to take the goat back.
Now let's get to the solution programmatically.
We denote a farmer, a wolf, a goat and a cabbage as 4 variables that take the value of only 0 or 1. Zero means that they are on the left bank, and one means that they are on the right bank.
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 to solve. Each step represents the state of a river, a boat, and all entities.
So far, we choose it at random and with a margin, take 10.
Each entity is presented in 10 copies - this is its value in each of the 10 steps.
Now let's set the conditions for the 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 constraints in the equation.
(In the presence of a 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) ]
And finally, we will set all possible actions of the farmer when crossing there or back.
He can either take a wolf, a goat or cabbage, or not take anyone, or not swim at all.
Of course, no one can cross without a farmer.
This will be expressed by the fact that each next 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 transport only 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 all conditions set of states.
A kind of four-dimensional cast of space-time.
Let's see what happened.
We see that in the end everything was ferried, only at the beginning our farmer decided to rest, and did 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 redundant, 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 cabbage, returning back alone, crossing the wolf.
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 we will try to change the conditions and prove that there are no solutions.
To do this, we will give our wolf herbivores, and now he wants to eat cabbage.
This can be compared with the case in which our goal is to protect the application and we must 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 is no solution.
Thus, we programmatically proved the impossibility of crossing with an omnivorous wolf, without loss for the farmer.
If the audience finds this topic interesting, I will tell you in future articles how to turn an ordinary program or function into an equation compatible with formal methods, and solve it, thus finding both all legitimate scenarios and vulnerabilities. First, on the same task, but presented in the form of a program, and then gradually complicating and moving on to actual examples from the world of software development.
Source: https://habr.com/ru/post/449002/
All Articles