À mon avis, le secteur francophone de l'internet aborde insuffisamment le thème de la vérification formelle, et il manque particulièrement des exemples simples et explicites.
Je vais donner un exemple tiré d'une source étrangère, et compléter avec ma propre solution bien connue à la problématique du transport du loup, de la chèvre et du 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.
Par vérification formelle, on entend généralement la vérification d'un programme ou d'un algorithme à l'aide d'un autre.
Cela permet de s'assurer que le comportement du programme correspond à ce qui est attendu, et de garantir sa sécurité.
La vérification formelle est le moyen le plus puissant pour détecter et éliminer les vulnérabilités : elle permet de trouver toutes les failles et les bogues existants dans le programme, ou de prouver qu'ils n'existent pas.
Il convient de noter que dans certains cas, cela peut s'avérer impossible, comme dans le problème des 8 reines sur un échiquier de 1000 cases : tout cela dépend de la complexité algorithmique ou du problème de l'arrêt.
Cependant, dans tous les cas, une des trois réponses sera obtenue : le programme est correct, incorrect, ou il n'a pas été possible de calculer la réponse.
En cas d'impossibilité de trouver une réponse, il est souvent possible de retravailler les zones ambiguës du programme, en réduisant leur complexité algorithmique, afin d'obtenir une réponse concrète, oui ou non.
La vérification formelle est utilisée, par exemple, dans le noyau de Windows et dans les systèmes d'exploitation des drones Darpa, pour assurer le plus haut niveau de protection.
Nous allons utiliser 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 précisément les équations, et non pas en essayant de deviner leurs valeurs par brute force.
Cela signifie qu'il est capable de trouver une réponse, même dans des cas où il y aurait 10^100 combinaisons d'entrées.
Et cela ne représente qu'une douzaine d'arguments d'entrée de type Integer, ce qui est couramment rencontré en pratique.
Le problème des 8 reines (tiré d'un manuel anglophone ).
# 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 lançant 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 renvoie comme réponse si les reines se battent entre elles.
Si nous devions résoudre ce programme à l'aide de la vérification formelle, il nous suffirait de faire un pas supplémentaire, celui de transformer le code du programme en équation : elle serait fondamentalement identique à la nôtre (bien sûr, à condition que le programme soit écrit sans erreurs).
Cela se passerait pratiquement de la même manière lors de la recherche de vulnérabilités : nous définissons simplement les conditions de sortie que nous souhaitons, par exemple le mot de passe administrateur, transformons le code source ou décompilé en équations compatibles avec la vérification, puis obtenons la réponse sur les données à fournir en entrée pour atteindre notre objectif.
À mon avis, le problème du loup, de la chèvre et du chou est encore plus intéressant, car sa résolution nécessite déjà beaucoup (7) d'étapes.
Si le problème des reines est comparable à la situation où l'on peut pénétrer sur un serveur par une seule requête GET ou POST, le loup, la chèvre et le chou démontre un exemple d'une catégorie beaucoup plus complexe et répandue, où les objectifs ne peuvent être atteints qu'avec plusieurs requêtes.
C'est comparable, par exemple, à un scénario où il faut trouver une injection SQL, écrire un fichier par ce biais, puis élever ses privilèges et enfin obtenir le mot de passe.
Les conditions du problème et sa résolutionUn fermier doit traverser la rivière avec un loup, une chèvre et un chou. Le fermier a un bateau qui ne peut transporter, en plus du paysan lui-même, qu'un seul objet. Le loup mangera la chèvre, et la chèvre mangera le chou si le fermier les laisse sans surveillance.
La solution est que, lors du 4ème pas, le fermier devra ramener la chèvre.
Nous allons maintenant commencer la résolution par un moyen programmatique.
Nous désignerons le fermier, le loup, la chèvre et le chou comme 4 variables ayant pour valeur seulement 0 ou 1. Zéro signifie qu'ils sont sur la rive gauche, et un signifie qu'ils sont 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) ]
# Chaque créature peut être sur le côté gauche (0) ou le côté droit (1) à chaque état
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 — c'est le nombre d'étapes nécessaires pour résoudre. Chaque étape représente un état de la rivière, du bateau et de toutes les entités.
Pour l'instant, choisissons-le au hasard et avec une marge, prenons 10.
Chaque entité est représentée par 10 exemplaires — c'est sa valeur à chacune des 10 étapes.
Définissons maintenant les conditions de départ et d'arrivée.
Départ = [ Human[0] == 0, Wolf[0] == 0, Goat[0] == 0, Cabbage[0] == 0 ]
Arrivée = [ Human[9] == 1, Wolf[9] == 1, Goat[9] == 1, Cabbage[9] == 1 ]
Ensuite, définissons les conditions où le loup mange la chèvre, ou la chèvre mange le chou, comme restrictions dans l'équation.
(En présence du fermier, 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) ]
Enfin, définissons toutes les actions possibles du fermier lors du transport là-bas ou en retour.
Il peut soit prendre avec lui le loup, la chèvre ou le chou, soit ne prendre personne, soit ne pas se déplacer du tout.
Évidemment, sans le fermier, personne ne peut traverser.
Cela sera exprimé par le fait que chaque état suivant de la rivière, du bateau et des entités peut différer de l'état précédent seulement de manière strictement limitée.
Pas plus de 2 bits, et avec de nombreuses autres limites, car le fermier ne peut transporter qu'une seule entité à la fois et il n'est pas possible de laisser tout le monde ensemble.
Voyage = [ Ou(
Et(Human[i] == Human[i+1] + 1, Wolf[i] == Wolf[i+1] + 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
Et(Human[i] == Human[i+1] + 1, Goat[i] == Goat[i+1] + 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
Et(Human[i] == Human[i+1] + 1, Cabbage[i] == Cabbage[i+1] + 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
Et(Human[i] == Human[i+1] - 1, Wolf[i] == Wolf[i+1] - 1, Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1]),
Et(Human[i] == Human[i+1] - 1, Goat[i] == Goat[i+1] - 1, Wolf[i] == Wolf[i+1], Cabbage[i] == Cabbage[i+1]),
Et(Human[i] == Human[i+1] - 1, Cabbage[i] == Cabbage[i+1] - 1, Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1]),
Et(Wolf[i] == Wolf[i+1], Goat[i] == Goat[i+1], Cabbage[i] == Cabbage[i+1])) pour i dans range(Num-1) ]
Lançons la solution.
solve(Side + Start + Finish + Safe + Travel)
Et nous obtenons la réponse !
Z3 a trouvé un ensemble d'états cohérent et satisfaisant toutes les conditions.
Une sorte d'empreinte spatio-temporelle en quatre dimensions.
Voyons donc ce qui s'est passé.
Nous voyons qu'au final tout le monde est traversé, mais au départ, notre fermier a décidé de se reposer et ne s'est pas déplacé durant les 2 premiers pas.
Human_2 = 0
Human_3 = 0
Cela indique que nous avons choisi un nombre d'états excessif, et 8 suffiront amplement.
Dans notre cas, le fermier a agi ainsi : départ, repos, repos, transport de la chèvre, retour, transport du chou, retour avec la chèvre, transport du loup, retour seul, livraison répétée de la chèvre.
Mais au final, la tâche est résolue.
#Старт.
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 cela, nous allons doter notre loup d'herbivorisme, et il voudra manger le chou.
Cela peut être comparé à une situation où notre objectif est de protéger une 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 :
pas de solution
Cela signifie qu'il n'y a vraiment pas de solutions.
Ainsi, nous avons prouvé par programmation l'impossibilité de transporter avec un loup omnivore, sans perte pour le fermier.
Si le public trouve ce sujet intéressant, dans de futurs articles, je raconterai comment transformer un programme ou une fonction ordinaire en une équation compatible avec des méthodes formelles et la résoudre, découvrant ainsi à la fois les scénarios légitimes et les vulnérabilités. D'abord sur ce même problème, mais présenté sous forme de programme, puis en compliquant progressivement et en passant à des exemples pertinents du monde du développement logiciel.
Le prochain article est déjà prêt :
Dans celui-ci, 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 formelles.
À mon avis, le thème de la vérification formelle est insuffisamment couvert dans le secteur russophone de l'Internet, et il manque particulièrement des exemples simples et visuels. Je donnerai un tel exemple provenant d'une source étrangère, et.
Source : habr.com
