À mon avis, dans le secteur russophone d'Internet, le sujet de la vérification formelle n'est pas suffisamment traité et, en particulier, des exemples simples et clairs font défaut.
Je vais donner un tel exemple d'une source étrangère et compléter ma propre solution au problème bien connu du transport 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 signifie généralement la vérification d'un programme ou d'un algorithme à l'aide d'un autre.
Cela est nécessaire pour s'assurer que le comportement du programme est conforme aux attentes, et également pour garantir sa sécurité.
La vérification formelle est le moyen le plus puissant pour trouver et éliminer les vulnérabilités: elle vous permet de trouver tous les trous et bogues existants dans le programme, ou de prouver qu'ils ne sont pas là.
Il convient de noter que dans certains cas, cela est impossible, comme dans le problème de 8 reines avec une largeur de carte de 1000 cellules: tout dépend de la complexité algorithmique ou du problème de l'arrêt.
Cependant, dans tous les cas, l'une des trois réponses sera reçue: le programme est correct, incorrect ou la réponse n'a pas pu être calculée.
S'il est impossible de trouver une réponse, il est souvent possible de retravailler des endroits obscurs dans le programme, en réduisant leur complexité algorithmique afin d'obtenir une réponse spécifique, oui ou non.
Et la vérification formelle est utilisée, par exemple, dans les systèmes d'exploitation du noyau Windows et des drones Darpa, pour fournir le 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 exactement les équations et ne sélectionne pas leurs valeurs avec force brute.
Cela signifie qu'il est capable de trouver la réponse, même dans les cas où les combinaisons d'options de saisie et 10 ^ 100.
Mais cela ne représente qu'une douzaine d'arguments d'entrée de type Integer, et cela se retrouve souvent dans la pratique.
Le problème de 8 reines (tiré du
manuel 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 de la reine est comparable à un programme qui prend les coordonnées de 8 reines et affiche la réponse si les reines se battent.
Si nous devions résoudre un tel programme en utilisant une vérification formelle, alors par rapport à la tâche, nous aurions juste besoin de franchir une autre étape sous la forme de la conversion du code du programme en une équation: il se révélerait être essentiellement identique au nôtre (bien sûr, si le programme était écrit correctement).
Presque la même chose se produira lors de la recherche de vulnérabilités: nous ne définissons que les conditions de sortie dont nous avons besoin, par exemple, le mot de passe administrateur, convertissons le code source ou décompilé en équations compatibles avec la vérification, puis nous obtenons la réponse quelles données doivent être entrées pour atteindre l'objectif.
À mon avis, le problème du loup, de la chèvre et du chou est encore plus intéressant, car de nombreuses (7) étapes sont déjà nécessaires pour le résoudre.
Si la tâche des reines est comparable à l'option lorsque vous pouvez pénétrer le serveur à l'aide d'une seule demande 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 seules quelques demandes peuvent être atteintes.
C'est comparable, par exemple, avec le scénario où vous devez trouver l'injection SQL, écrire un fichier à travers elle, puis augmenter vos droits et ensuite seulement obtenir le mot de passe.
Conditions du problème et sa solutionL'agriculteur doit transporter le loup, la chèvre et le chou à travers la rivière. L'agriculteur a un bateau dans lequel un seul objet peut rentrer, à l'exception du paysan lui-même. Le loup mangera la chèvre, et la chèvre mangera du 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 la solution par programme.
Nous désignons l'agriculteur, le loup, la chèvre et le chou comme 4 variables, qui ne prennent la valeur que 0 ou 1. Zéro signifie qu'ils sont sur la rive gauche et un signifie que sur la 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 est un état d'une rivière, d'un bateau et de toutes les entités.
Pour l'instant, choisissez-le au hasard et avec une marge, prenez 10.
Chaque entité est représentée en 10 exemplaires - c'est sa valeur à chacune des 10 étapes.
Nous définissons maintenant les conditions de début et de fin.
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 fixons les conditions dans lesquelles le loup mange la chèvre, ou le chou de chèvre, comme restrictions dans l'équation.
(En présence de l'agriculteur, l'agression n'est pas 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) ]
Et enfin, nous demandons toutes les actions possibles de l'agriculteur lors de son déplacement là-bas ou en arrière.
Il peut soit emmener avec lui un loup, une chèvre ou un chou, soit n'emmener personne, ni même aller nulle part.
Bien sûr, personne ne peut traverser sans agriculteur.
Cela se traduira 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 de nombreuses autres limites, car l'agriculteur ne peut transporter qu'une seule entité à la fois et tous ne peuvent pas être laissés 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écutez la solution.
solve(Side + Start + Finish + Safe + Travel)
Et nous obtenons la réponse!
Z3 a trouvé un ensemble de conditions cohérent et satisfaisant.
Une sorte de distribution de l'espace-temps en quatre dimensions.
Voyons ce qui s'est passé.
On voit qu'à la fin tout le monde s'est croisé, seulement au début notre fermier a décidé de se détendre, et ne nage nulle part dans les 2 premières étapes.
Human_2 = 0 Human_3 = 0
Cela suggère que le nombre d'États que nous avons choisis est excessif et 8 suffira amplement.
Dans notre cas, l'agriculteur a fait cela: commencer, 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, remettre la chèvre.
Mais au final, le problème est 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 prouvons qu'il n'y a pas de solutions.
Pour ce faire, nous doterons notre loup d'herbivore, et il voudra manger du chou.
Cela peut être comparé au cas où notre objectif est de protéger l'application et nous devons nous assurer qu'il n'y a pas d'échappatoires.
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 pas de solutions.
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, je vous dirai dans les prochains articles comment transformer un programme ou une fonction ordinaire en une équation compatible avec les méthodes formelles et le 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 déjà sous la forme d'un programme, puis en compliquant progressivement et en passant à des exemples pertinents du monde du développement logiciel.
L'article suivant est prêt:
Création d'un système de vérification formel à partir de zéro: nous écrivons une machine virtuelle de caractères en PHP et PythonDans ce document, je passe de la vérification formelle des tâches aux programmes et je décris
comment les convertir automatiquement en systèmes de règles formels.