La vérification formelle est la vérification d'un programme ou d'un algorithme à l'aide d'un autre.
C'est l'une des méthodes les plus puissantes qui vous permet de trouver toutes les vulnérabilités d'un programme ou de prouver qu'elles n'existent pas.
Une description plus détaillée de la vérification formelle peut être vue dans l'exemple de résolution du problème de dans mon article précédent.
Dans cet article, je passe de la vérification formelle des problèmes aux programmes et je décris comment
comment peuvent-ils être automatiquement convertis en systèmes de règles formels.
Pour ce faire, j'ai écrit mon propre analogue d'une machine virtuelle, en utilisant des principes symboliques.
Il analyse le code du programme et le traduit en un système d'équations (SMT), qui peut déjà être résolu par programme.
Étant donné que les informations sur les calculs symboliques sont présentées sur Internet de manière plutôt fragmentaire,
Je vais décrire brièvement ce que c'est.
Le calcul symbolique est un moyen d'exécuter simultanément un programme sur un large éventail de données et constitue le principal outil de vérification formelle du programme.
Par exemple, nous pouvons définir des conditions d'entrée dans lesquelles le premier argument peut prendre n'importe quelle valeur positive, le deuxième négatif, le troisième zéro et l'argument de sortie, par exemple 42.
Des calculs symboliques en une seule fois nous donneront la réponse quant à savoir s'il nous est possible d'obtenir le résultat souhaité et un exemple d'un ensemble de tels paramètres d'entrée. Ou la preuve qu’il n’existe pas de tels paramètres.
De plus, nous pouvons définir les arguments d'entrée sur tous les arguments possibles et sélectionner uniquement ceux de sortie, par exemple le mot de passe administrateur.
Dans ce cas, nous trouverons toutes les vulnérabilités du programme ou obtiendrons la preuve que le mot de passe de l’administrateur est sécurisé.
On peut noter que l’exécution classique d’un programme avec des données d’entrée spécifiques est un cas particulier d’exécution symbolique.
Par conséquent, ma VM de personnage peut également fonctionner en mode émulation d’une machine virtuelle standard.
Dans les commentaires de l'article précédent, on peut trouver une critique juste de la vérification formelle avec une discussion de ses faiblesses.
Les principaux problèmes sont :
- Explosion combinatoire, puisque la vérification formelle se résume finalement à P=NP
- Le traitement des appels vers le système de fichiers, les réseaux et autres stockages externes est plus difficile à vérifier
- Bogues dans la spécification, lorsque le client ou le programmeur avait l'intention d'une chose, mais ne l'a pas décrit avec suffisamment de précision dans la spécification technique.
En conséquence, le programme sera vérifié et conforme aux spécifications, mais fera quelque chose de complètement différent de ce que les créateurs attendaient de lui.
Puisque dans cet article j'envisage principalement l'utilisation de la vérification formelle dans la pratique, je ne me cognerai pas la tête contre le mur pour l'instant, et choisirai un système où la complexité algorithmique et le nombre d'appels externes sont minimes.
Étant donné que les contrats intelligents répondent le mieux à ces exigences, le choix s'est porté sur les contrats RIDE de la plateforme Waves : ils ne sont pas complets de Turing et leur complexité maximale est artificiellement limitée.
Mais nous les considérerons exclusivement du côté technique.
En plus de tout, la vérification formelle sera particulièrement demandée pour tout contrat : il est généralement impossible de corriger une erreur de contrat après son lancement.
Et le coût de telles erreurs peut être très élevé, car des sommes assez importantes sont souvent stockées sur des contrats intelligents.
Ma machine virtuelle symbolique est écrite en PHP et Python et utilise Z3Prover de Microsoft Research pour résoudre les formules SMT résultantes.
À la base se trouve une puissante recherche multi-transactionnelle, qui
permet de trouver des solutions ou des vulnérabilités, même si cela nécessite de nombreuses transactions.
Même , l’un des cadres symboliques les plus puissants pour détecter les vulnérabilités d’Ethereum, n’a ajouté cette fonctionnalité qu’il y a quelques mois.
Mais il convient de noter que les contrats d’éther sont plus complexes et que Turing est complet.
PHP traduit le code source du contrat intelligent RIDE en un script python, dans lequel le programme est présenté comme un système d'états de contrat et de conditions de transition compatible Z3 SMT :
Je vais maintenant décrire plus en détail ce qui se passe à l'intérieur.
Mais d’abord, quelques mots sur le langage des contrats intelligents RIDE.
Il s’agit d’un langage de programmation fonctionnel et basé sur des expressions qui est paresseux de par sa conception.
RIDE fonctionne de manière isolée au sein de la blockchain et peut récupérer et écrire des informations à partir du stockage lié au portefeuille de l'utilisateur.
Vous pouvez joindre un contrat RIDE à chaque portefeuille, et le résultat de l'exécution sera uniquement VRAI ou FAUX.
TRUE signifie que le contrat intelligent autorise la transaction et FALSE signifie qu'il l'interdit.
Un exemple simple : un script peut interdire un transfert si le solde du portefeuille est inférieur à 100.
A titre d'exemple, je prendrai les mêmes Loup, Chèvre et Chou, mais déjà présentés sous la forme d'un contrat intelligent.
L'utilisateur ne pourra pas retirer d'argent du portefeuille sur lequel le contrat est déployé tant qu'il n'aura pas envoyé tout le monde de l'autre côté.
#Извлекаем положение всех объектов из блокчейна
let contract = tx.sender
let human= extract(getInteger(contract,"human"))
let wolf= extract(getInteger(contract,"wolf"))
let goat= extract(getInteger(contract,"goat"))
let cabbage= extract(getInteger(contract,"cabbage"))
#Это так называемая дата-транзакция, в которой пользователь присылает новые 4 переменные.
#Контракт разрешит её только в случае если все объекты останутся в сохранности.
match tx {
case t:DataTransaction =>
#Извлекаем будущее положение всех объектов из транзакции
let newHuman= extract(getInteger(t.data,"human"))
let newWolf= extract(getInteger(t.data,"wolf"))
let newGoat= extract(getInteger(t.data,"goat"))
let newCabbage= extract(getInteger(t.data,"cabbage"))
#0 обозначает, что объект на левом берегу, а 1 что на правом
let humanSide= human == 0 || human == 1
let wolfSide= wolf == 0 || wolf == 1
let goatSide= goat == 0 || goat == 1
let cabbageSide= cabbage == 0 || cabbage == 1
let side= humanSide && wolfSide && goatSide && cabbageSide
#Будут разрешены только те транзакции, где с козой никого нет в отсутствии фермера.
let safeAlone= newGoat != newWolf && newGoat != newCabbage
let safe= safeAlone || newGoat == newHuman
let humanTravel= human != newHuman
#Способы путешествия фермера туда и обратно, с кем-то либо в одиночку.
let t1= humanTravel && newWolf == wolf + 1 && newGoat == goat && newCabbage == cabbage
let t2= humanTravel && newWolf == wolf && newGoat == goat + 1 && newCabbage == cabbage
let t3= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage + 1
let t4= humanTravel && newWolf == wolf - 1 && newGoat == goat && newCabbage == cabbage
let t5= humanTravel && newWolf == wolf && newGoat == goat - 1 && newCabbage == cabbage
let t6= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage - 1
let t7= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage
let objectTravel = t1 || t2 || t3 || t4 || t5 || t6 || t7
#Последняя строка в разделе транзакции описывает разрешающее транзакцию условие.
#Переменные транзакции должны иметь значения 1 или 0, все объекты должны
#быть в безопасности, а фермер должен переплывать реку в одиночку
#или с кем-то на каждом шагу
side && safe && humanTravel && objectTravel
case s:TransferTransaction =>
#Транзакция вывода средств разрешена только в случае если все переплыли на другой берег
human == 1 && wolf == 1 && goat == 1 && cabbage == 1
#Все прочие типы транзакций запрещены
case _ => false
}
PHP extrait d'abord toutes les variables du contrat intelligent sous la forme de leurs clés et de la variable d'expression booléenne correspondante.
cabbage: extract ( getInteger ( contract , "cabbage" ) )
goat: extract ( getInteger ( contract , "goat" ) )
human: extract ( getInteger ( contract , "human" ) )
wolf: extract ( getInteger ( contract , "wolf" ) )
fState: human== 1 && wolf== 1 && goat== 1 && cabbage== 1
fState:
wolf:
goat:
cabbage:
cabbageSide: cabbage== 0 || cabbage== 1
human: extract ( getInteger ( contract , "human" ) )
newGoat: extract ( getInteger ( t.data , "goat" ) )
newHuman: extract ( getInteger ( t.data , "human" ) )
goatSide: goat== 0 || goat== 1
humanSide: human== 0 || human== 1
t7: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage
t3: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage + 1
t6: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage - 1
t2: humanTravel && newWolf== wolf && newGoat== goat + 1 && newCabbage== cabbage
t5: humanTravel && newWolf== wolf && newGoat== goat - 1 && newCabbage== cabbage
t1: humanTravel && newWolf== wolf + 1 && newGoat== goat && newCabbage== cabbage
t4: humanTravel && newWolf== wolf - 1 && newGoat== goat && newCabbage== cabbage
safeAlone: newGoat != newWolf && newGoat != newCabbage
wolfSide: wolf== 0 || wolf== 1
humanTravel: human != newHuman
side: humanSide && wolfSide && goatSide && cabbageSide
safe: safeAlone || newGoat== newHuman
objectTravel: t1 || t2 || t3 || t4 || t5 || t6 || t7
PHP les convertit ensuite en une description de système compatible Z3Prover SMT en Python.
Les données sont encapsulées dans une boucle, où les variables de stockage reçoivent l'index i, les variables de transaction l'index i + 1 et les variables avec des expressions définissent les règles de transition de l'état précédent au suivant.
C'est le cœur même de notre machine virtuelle, qui propose un moteur de recherche multi-transactionnel.
fState: And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 )
final: fState[Steps]
fState:
wolf:
goat:
cabbage:
cabbageSide: Or( cabbage[i] == 0 , cabbage[i] == 1 )
goatSide: Or( goat[i] == 0 , goat[i] == 1 )
humanSide: Or( human[i] == 0 , human[i] == 1 )
t7: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
t3: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] + 1 )
t6: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] - 1 )
t2: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage == cabbage[i] )
t5: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage == cabbage[i] )
t1: And( And( And( humanTravel[i] , wolf == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
t4: And( And( And( humanTravel[i] , wolf == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
safeAlone: And( goat[i+1] != wolf , goat[i+1] != cabbage )
wolfSide: Or( wolf[i] == 0 , wolf[i] == 1 )
humanTravel: human[i] != human[i+1]
side: And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] )
safe: Or( safeAlone[i] , goat[i+1] == human[i+1] )
objectTravel: Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] )
data: And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] )
Les conditions sont triées et insérées dans un modèle de script conçu pour décrire le système SMT en Python.
Modèle vierge
import json
from z3 import *
s = Solver()
Steps=7
Num= Steps+1
$code$
#template, only start rest
s.add(data + start)
#template
s.add(final)
ind = 0
f = open("/var/www/html/all/bin/python/log.txt", "a")
while s.check() == sat:
ind = ind +1
print ind
m = s.model()
print m
print "traversing model..."
#for d in m.decls():
#print "%s = %s" % (d.name(), m[d])
f.write(str(m))
f.write("nn")
exit()
#s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model
print "Total solution number: "
print ind
f.close()
Pour le dernier état de toute la chaîne, les règles spécifiées dans la section transaction de transfert sont appliquées.
Cela signifie que Z3Prover recherchera précisément les ensembles de conditions qui permettront finalement de retirer les fonds du contrat.
En conséquence, nous recevons automatiquement un modèle SMT entièrement fonctionnel de notre contrat.
Vous pouvez voir qu'il est très similaire au modèle de mon article précédent, que j'ai compilé manuellement.
Modèle terminé
import json
from z3 import *
s = Solver()
Steps=7
Num= Steps+1
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) ]
nothing= [ And( human[i] == human[i+1], wolf[i] == wolf[i+1], goat[i] == goat[i+1], cabbage[i] == cabbage[i+1] ) for i in range(Num-1) ]
start= [ human[0] == 1, wolf[0] == 0, goat[0] == 1, cabbage[0] == 0 ]
safeAlone= [ And( goat[i+1] != wolf[i+1] , goat[i+1] != cabbage[i+1] ) for i in range(Num-1) ]
safe= [ Or( safeAlone[i] , goat[i+1] == human[i+1] ) for i in range(Num-1) ]
humanTravel= [ human[i] != human[i+1] for i in range(Num-1) ]
cabbageSide= [ Or( cabbage[i] == 0 , cabbage[i] == 1 ) for i in range(Num-1) ]
goatSide= [ Or( goat[i] == 0 , goat[i] == 1 ) for i in range(Num-1) ]
humanSide= [ Or( human[i] == 0 , human[i] == 1 ) for i in range(Num-1) ]
t7= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t3= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] + 1 ) for i in range(Num-1) ]
t6= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] - 1 ) for i in range(Num-1) ]
t2= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t5= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t1= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t4= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
wolfSide= [ Or( wolf[i] == 0 , wolf[i] == 1 ) for i in range(Num-1) ]
side= [ And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] ) for i in range(Num-1) ]
objectTravel= [ Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] ) for i in range(Num-1) ]
data= [ Or( And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] ) , nothing[i]) for i in range(Num-1) ]
fState= And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 )
final= fState
#template, only start rest
s.add(data + start)
#template
s.add(final)
ind = 0
f = open("/var/www/html/all/bin/python/log.txt", "a")
while s.check() == sat:
ind = ind +1
print ind
m = s.model()
print m
print "traversing model..."
#for d in m.decls():
#print "%s = %s" % (d.name(), m[d])
f.write(str(m))
f.write("nn")
exit()
#s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model
print "Total solution number: "
print ind
f.close()
Après le lancement, Z3Prover résout le contrat intelligent et nous fournit une chaîne de transactions qui nous permettra de retirer des fonds :
Winning transaction chain found:
Data transaction: human= 0, wolf= 0, goat= 1, cabbage= 0
Data transaction: human= 1, wolf= 0, goat= 1, cabbage= 1
Data transaction: human= 0, wolf= 0, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 0, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Transfer transaction
En plus du contrat de ferry, vous pouvez expérimenter vos propres contrats ou essayer cet exemple simple, résolu en 2 transactions.
let contract = tx.sender
let a= extract(getInteger(contract,"a"))
let b= extract(getInteger(contract,"b"))
let c= extract(getInteger(contract,"c"))
let d= extract(getInteger(contract,"d"))
match tx {
case t:DataTransaction =>
let na= extract(getInteger(t.data,"a"))
let nb= extract(getInteger(t.data,"b"))
let nc= extract(getInteger(t.data,"c"))
let nd= extract(getInteger(t.data,"d"))
nd == 0 || a == 100 - 5
case s:TransferTransaction =>
( a + b - c ) * d == 12
case _ => true
}
Puisqu'il s'agit de la toute première version, la syntaxe est très limitée et il peut y avoir des bugs.
Dans les articles suivants, je prévois d'aborder le développement ultérieur de la VM et de montrer comment vous pouvez créer des contrats intelligents formellement vérifiés avec son aide, et pas seulement les résoudre.
La machine virtuelle des personnages est disponible sur
Après avoir mis de l'ordre dans le code source de la VM symbolique et y avoir ajouté des commentaires, je prévois de le mettre sur GitHub en accès gratuit.
Source: habr.com