Formal Verification on the Example of the Wolf, Goat, and Cabbage Problem

In my opinion, in the Russian-speaking sector of the Internet, the subject of formal verification is not covered enough, and especially there are not enough simple and illustrative examples.

I will give such an example from a foreign source, and add my own solution to the well-known problem of crossing 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 is usually understood as the verification of 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, as well as to ensure its safety.

Formal verification is the most powerful tool for finding and eliminating vulnerabilities: it allows you to find all existing holes and bugs in the program, or to prove that they do not exist.
It is worth noting that in some cases this is impossible, as, for example, in the problem of 8 queens with a board width of 1000 cells: everything rests on the algorithmic complexity or the stopping problem.

However, in any case, one of 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 an answer, it is often possible to rework the obscure parts of the program by reducing their algorithmic complexity in order to get a specific yes or no answer.

And formal verification is used, for example, in the Windows kernel and operating systems of Darpa drones, to ensure the maximum level of protection.

We will be using Z3Prover, a very powerful tool for automated theorem proving and equation solving.

Moreover, Z3 just solves the equations, and does not select their values ​​​​by brute force.
This means that he is able to find the answer, even in cases where the combinations of input options and 10 ^ 100.

But this is only about a dozen input arguments of type Integer, and this often occurs 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 problem about queens is comparable to a program that takes the coordinates of 8 queens as input and outputs the answer whether the queens beat each other.

If we were to solve such a program using formal verification, then compared to the problem, we would simply need to take one more 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 is written without errors).

Almost the same thing will happen in the case of searching for vulnerabilities: we just set the output conditions we need, for example, the admin password, transform the source or decompiled code into equations compatible with verification, and then get an answer about what data needs to be input to achieve the goal.

In my opinion, the wolf, goat and cabbage problem is even more interesting, since it takes many (7) steps to solve it.

If the problem of queens is comparable to the case where you can penetrate the server with a single GET or POST request, then the wolf, goat and cabbage shows an example from a much more complex and common category, in which the goal can be achieved with only a few requests.

This is comparable, for example, to a scenario where you need to find an SQL injection, write a file through it, then elevate your rights, and only then get a password.

Conditions of the problem and its solutionThe farmer needs to transport a wolf, a goat and a cabbage across the river. The farmer has a boat that can fit only one object besides the peasant himself. The wolf will eat the goat and the goat will eat the cabbage if the farmer leaves them unattended.

The answer is that in step 4 the farmer will need to take the goat back.
Now let's start solving programmatically.

Let's designate a farmer, a wolf, a goat, and a cabbage as 4 variables that only take a value of 0 or 1. Zero means that they are on the left bank, and one means that 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 needed to solve. 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, take 10.

Each entity is represented in 10 instances - this is its value at each of the 10 steps.

Now let's set the start and finish conditions.

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 conditions where the wolf eats the goat, or the 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, let's define all the possible actions of the farmer when crossing there or back.
He can either take a wolf, a goat or a cabbage with him, or take no one, or go nowhere 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 only transport one essence 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) ]

Let's run the solution.

solve(Side + Start + Finish + Safe + Travel)

And we get the answer!

Z3 found a consistent and satisfying set of states.
A kind of four-dimensional cast of space-time.

Let's figure out what happened.

We see that in the end everyone crossed, only at the beginning our farmer decided to rest, and he doesn’t swim anywhere on the first 2 steps.

Human_2 = 0
Human_3 = 0

This suggests that we have chosen an excessive number of states, and 8 will be quite enough.

In our case, the farmer did this: start, rest, rest, ferry the goat, ferry back, ferry the cabbage, return with the goat, ferry the wolf, return back alone, re-deliver 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 herbivory, and he will want to eat cabbage.
This can be compared to a 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 response:

 no solution

It means that there really are no solutions.

Thus, we programmatically proved the impossibility of crossing with an omnivorous wolf, without loss 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 already presented in the form of a program, and then gradually complicating it and moving on to actual examples from the world of software development.

The next article is ready:
Creating a Formal Verification System from Scratch: Writing a Symbolic VM in PHP and Python

In it, I move from formal verification of problems, to programs, and describe,
how you can convert them into systems of formal rules automatically.

Source: habr.com