À mon avis, dans le secteur russophone de l'Internet, le thème de la vérification formelle n'est pas suffisamment abordé et il y a surtout un manque d'exemples simples et clairs.
Je vais donner un exemple provenant d'une source étrangère et ajouter ma propre solution au problème bien connu du passage d'un loup, d'une chèvre et d'un chou de l'autre côté de la rivière.
Mais d’abord, je décrirai brièvement ce qu’est la vérification formelle et pourquoi elle est nécessaire.
La vérification formelle consiste généralement à vérifier un programme ou un algorithme à l’aide d’un autre.
Cela est nécessaire pour garantir que le programme se comporte comme prévu et également pour assurer sa sécurité.
La vérification formelle est le moyen le plus puissant pour trouver et éliminer les vulnérabilités : elle permet de trouver tous les trous et bugs existants dans un programme, ou de prouver qu'ils n'existent pas.
Il convient de noter que dans certains cas, cela est impossible, comme dans le problème de 8 dames avec une largeur de 1000 cases : tout se résume à la complexité algorithmique ou au problème d'arrêt.
Cependant, dans tous les cas, l'une des trois réponses sera reçue : le programme est correct, incorrect ou il n'a pas été possible de calculer la réponse.
S'il est impossible de trouver une réponse, il est souvent possible de retravailler des parties peu claires du programme, réduisant ainsi leur complexité algorithmique, afin d'obtenir une réponse spécifique par oui ou par non.
Et la vérification formelle est utilisée, par exemple, dans le noyau Windows et dans les systèmes d'exploitation des drones Darpa, pour garantir un niveau de protection maximal.
Nous utiliserons Z3Prover, un outil très puissant pour la preuve automatisée de théorèmes et la résolution d'équations.
De plus, Z3 résout les équations et ne sélectionne pas leurs valeurs par force brute.
Cela signifie qu'il est capable de trouver la réponse, même dans les cas où il existe 10^100 combinaisons d'options de saisie.
Mais il ne s’agit que d’une douzaine d’arguments d’entrée de type Integer, ce qui est souvent rencontré dans la pratique.
Problème concernant 8 reines (tiré de l'anglais ).
# 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)
En exécutant Z3, nous obtenons la 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]
Le problème des reines est comparable à un programme qui prend en entrée les coordonnées de 8 reines et donne la réponse si les reines se battent entre elles.
Si nous devions résoudre un tel programme à l'aide d'une vérification formelle, alors par rapport au problème, nous aurions simplement besoin de faire une étape de plus sous la forme de la conversion du code du programme en équation : il s'avérerait essentiellement identique au nôtre ( bien sûr, si le programme a été écrit correctement).
Presque la même chose se produira dans le cas de la recherche de vulnérabilités : nous définissons simplement les conditions de sortie dont nous avons besoin, par exemple le mot de passe administrateur, transformons le code source ou décompilé en équations compatibles avec la vérification, puis obtenons une réponse sur ce que les données doivent être fournies en entrée pour atteindre l’objectif.
À mon avis, le problème du loup, de la chèvre et du chou est encore plus intéressant, puisque sa résolution nécessite déjà de nombreuses (7) étapes.
Si le problème de la reine est comparable au cas où vous pouvez pénétrer dans un serveur à l'aide d'une seule requête GET ou POST, alors le loup, la chèvre et le chou illustrent un exemple d'une catégorie beaucoup plus complexe et répandue, dans laquelle l'objectif ne peut être atteint que par plusieurs demandes.
Ceci est comparable, par exemple, à un scénario dans lequel vous devez trouver une injection SQL, y écrire un fichier, puis élever vos droits et ensuite seulement obtenir un mot de passe.
Conditions du problème et sa solutionLe fermier doit transporter un loup, une chèvre et un chou à travers la rivière. L'agriculteur dispose d'un bateau qui ne peut accueillir qu'un seul objet, en plus de l'agriculteur lui-même. Le loup mangera la chèvre et la chèvre mangera le chou si le fermier les laisse sans surveillance.
La solution est qu’à l’étape 4, l’agriculteur devra reprendre la chèvre.
Commençons maintenant à le résoudre par programme.
Notons le fermier, le loup, la chèvre et le chou comme 4 variables qui ne prennent que la valeur 0 ou 1. Zéro signifie qu'ils sont sur la rive gauche, et un signifie qu'ils sont sur la rive droite.
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 est le nombre d'étapes nécessaires pour résoudre. Chaque étape représente l'état du fleuve, du bateau et de toutes les entités.
Pour l'instant, choisissons-le au hasard et avec une marge, prenons-en 10.
Chaque entité est représentée en 10 exemplaires - c'est sa valeur à chacune des 10 étapes.
Définissons maintenant les conditions de départ et d'arrivée.
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 ]
Ensuite, nous définissons les conditions dans lesquelles le loup mange la chèvre, ou la chèvre mange le chou, comme contraintes dans l'équation.
(En présence d'un agriculteur, l'agression est 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) ]
Et enfin, nous définirons toutes les actions possibles de l'agriculteur lors de la traversée aller ou retour.
Il peut soit emmener avec lui un loup, une chèvre ou un chou, soit n'emmener personne, soit ne naviguer nulle part.
Bien sûr, personne ne peut traverser sans agriculteur.
Cela s'exprimera par le fait que chaque état ultérieur du fleuve, du bateau et des entités ne peut différer du précédent que de manière strictement limitée.
Pas plus de 2 bits, et avec bien d'autres limites, puisque le farmer ne peut transporter qu'une seule entité à la fois et qu'il ne peut pas toutes les laisser ensemble.
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) ]
Exécutons la solution.
solve(Side + Start + Finish + Safe + Travel)
Et nous obtenons la réponse !
Z3 a trouvé un ensemble cohérent d’états qui satisfait à toutes les conditions.
Une sorte de projection tridimensionnelle de l’espace-temps.
Voyons ce qui s'est passé.
On voit qu'à la fin tout le monde a traversé, seulement au début notre agriculteur a décidé de se reposer, et dans les 2 premiers pas il ne nage nulle part.
Human_2 = 0
Human_3 = 0
Cela suggère que le nombre d'États que nous avons choisis est excessif et que 8 seront tout à fait suffisants.
Dans notre cas, l'agriculteur a fait ceci : partir, se reposer, se reposer, traverser la chèvre, traverser en arrière, traverser le chou, revenir avec la chèvre, traverser le loup, revenir seul, re-livrer la chèvre.
Mais finalement le problème a été résolu.
#Старт.
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
Essayons maintenant de changer les conditions et de prouver qu’il n’y a pas de solutions.
Pour ce faire, nous donnerons à notre loup de l'herbivore, et il voudra manger du chou.
Cela peut être comparé au cas dans lequel notre objectif est de sécuriser l’application et nous devons nous assurer qu’il n’y a pas de failles.
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 nous a donné la réponse suivante :
no solution
Cela signifie qu’il n’y a vraiment aucune solution.
Ainsi, nous avons prouvé par programme l'impossibilité de croiser avec un loup omnivore sans pertes pour l'agriculteur.
Si le public trouve ce sujet intéressant, alors dans les prochains articles, je vous expliquerai comment transformer un programme ou une fonction ordinaire en une équation compatible avec les méthodes formelles et la résoudre, révélant ainsi à la fois tous les scénarios et vulnérabilités légitimes. D'abord sur la même tâche, mais présentée sous la forme d'un programme, puis en la compliquant progressivement et en passant à des exemples actuels du monde du développement logiciel.
Le prochain article est déjà prêt :
Dans ce document, je passe de la vérification formelle des problèmes aux programmes et je décris
comment peuvent-ils être automatiquement convertis en systèmes de règles formels.
Source: habr.com