La verificació formal és la verificació d'un programa o algorisme mitjançant un altre.
Aquest és un dels mètodes més potents que permet trobar totes les vulnerabilitats d'un programa o demostrar que no existeixen.
Una descripció més detallada de la verificació formal es pot veure a l'exemple de resolució del problema de al meu article anterior.
En aquest article passo de la verificació formal dels problemes als programes i descric com
com es poden convertir automàticament en sistemes de regles formals.
Per fer-ho, vaig escriure el meu propi anàleg d'una màquina virtual, utilitzant principis simbòlics.
Analitza el codi del programa i el tradueix a un sistema d'equacions (SMT), que ja es pot resoldre mitjançant programació.
Atès que la informació sobre càlculs simbòlics es presenta a Internet de manera força fragmentària,
Descriuré breument què és.
El càlcul simbòlic és una manera d'executar simultàniament un programa sobre una àmplia gamma de dades i és l'eina principal per a la verificació formal del programa.
Per exemple, podem establir condicions d'entrada on el primer argument pugui prendre qualsevol valor positiu, el segon negatiu, el tercer zero i l'argument de sortida, per exemple, 42.
Els càlculs simbòlics en una tirada ens donaran la resposta a si és possible obtenir el resultat desitjat i un exemple d'un conjunt d'aquests paràmetres d'entrada. O prova que no existeixen aquests paràmetres.
A més, podem establir els arguments d'entrada a tots els possibles i seleccionar només els de sortida, per exemple, la contrasenya de l'administrador.
En aquest cas, trobarem totes les vulnerabilitats del programa o obtindrem una prova que la contrasenya de l'administrador és segura.
Es pot observar que l'execució clàssica d'un programa amb dades d'entrada específiques és un cas especial d'execució simbòlica.
Per tant, el meu personatge VM també pot funcionar en mode d'emulació d'una màquina virtual estàndard.
En els comentaris de l'article anterior es pot trobar una crítica justa a la verificació formal amb una discussió sobre les seves debilitats.
Els principals problemes són:
- Explosió combinatòria, ja que la verificació formal es redueix finalment a P=NP
- El processament de trucades al sistema de fitxers, xarxes i altres emmagatzematge extern és més difícil de verificar
- Errors a l'especificació, quan el client o programador pretenia una cosa, però no ho descriu amb prou precisió a l'especificació tècnica.
Com a resultat, el programa es verificarà i complirà l'especificació, però farà una cosa completament diferent del que els creadors esperaven d'ell.
Com que en aquest article estic considerant principalment l'ús de la verificació formal a la pràctica, de moment no em colpejaré el cap contra la paret i triaré un sistema on la complexitat algorítmica i el nombre de trucades externes siguin mínims.
Com que els contractes intel·ligents s'adapten millor a aquests requisits, l'elecció va recaure en els contractes RIDE de la plataforma Waves: no són Turing complets i la seva màxima complexitat està limitada artificialment.
Però els considerarem exclusivament des del vessant tècnic.
A més de tot, la verificació formal serà especialment demandada per a qualsevol contracte: normalment és impossible corregir un error de contracte després que s'hagi posat en marxa.
I el cost d'aquests errors pot ser molt elevat, ja que sovint s'emmagatzemen quantitats bastant grans de fons en contractes intel·ligents.
La meva màquina virtual simbòlica està escrita en PHP i Python i utilitza Z3Prover de Microsoft Research per resoldre les fórmules SMT resultants.
En el seu nucli hi ha una potent cerca multi-transaccional, que
permet trobar solucions o vulnerabilitats, encara que requereixi moltes transaccions.
Fins i tot , un dels marcs simbòlics més potents per trobar vulnerabilitats d'Ethereum, només va afegir aquesta capacitat fa uns mesos.
Però val la pena assenyalar que els contractes d'èter són més complexos i Turing complet.
PHP tradueix el codi font del contracte intel·ligent RIDE a un script Python, en el qual el programa es presenta com un sistema d'estats de contracte i condicions per a les seves transicions compatible amb Z3 SMT:
Ara descriuré amb més detall què passa a dins.
Però primer, algunes paraules sobre el llenguatge del contracte intel·ligent RIDE.
És un llenguatge de programació funcional i basat en expressions que és mandrós per disseny.
RIDE s'executa de manera aïllada dins de la cadena de blocs i pot recuperar i escriure informació de l'emmagatzematge vinculat a la cartera de l'usuari.
Podeu adjuntar un contracte RIDE a cada cartera i el resultat de l'execució només serà VERDADER o FALS.
TRUE vol dir que el contracte intel·ligent permet la transacció i FALSE significa que la prohibeix.
Un exemple senzill: un script pot prohibir una transferència si el saldo de la cartera és inferior a 100.
Com a exemple, prendré el mateix llop, cabra i col, però ja presentats en forma de contracte intel·ligent.
L'usuari no podrà retirar diners de la cartera en què es desplega el contracte fins que no hagi enviat tothom a l'altra banda.
#Извлекаем положение всех объектов из блокчейна
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 extreu primer totes les variables del contracte intel·ligent en forma de les seves claus i la corresponent variable d'expressió booleana.
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
A continuació, PHP els converteix en una descripció del sistema compatible amb Z3Prover SMT a Python.
Les dades s'emboliquen en un bucle, on les variables d'emmagatzematge reben l'índex i, les variables de transacció índex i + 1 i les variables amb expressions estableixen les regles per a la transició de l'estat anterior al següent.
Aquest és el cor mateix de la nostra màquina virtual, que proporciona un motor de cerca multitransaccional.
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 condicions s'ordenen i s'insereixen en una plantilla d'script dissenyada per descriure el sistema SMT a Python.
Plantilla en blanc
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()
Per a l'últim estat de tota la cadena, s'apliquen les regles que s'especifiquen a la secció de transacció de transferència.
Això vol dir que Z3Prover buscarà precisament aquests conjunts de condicions que permetin, finalment, retirar fons del contracte.
Com a resultat, rebem automàticament un model SMT totalment funcional del nostre contracte.
Podeu veure que és molt semblant al model del meu article anterior, que vaig compilar manualment.
Plantilla completada
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()
Després del llançament, Z3Prover resol el contracte intel·ligent i ens proporciona una cadena de transaccions que ens permetran retirar fons:
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
A més del contracte de ferri, podeu experimentar amb els vostres propis contractes o provar aquest exemple senzill, que es resol en 2 transaccions.
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
}
Com que aquesta és la primera versió, la sintaxi és molt limitada i pot haver-hi errors.
En els articles següents, penso cobrir el desenvolupament posterior de la VM i mostrar com podeu crear contractes intel·ligents verificats formalment amb la seva ajuda, i no només resoldre'ls.
La màquina virtual de personatges està disponible a
Després d'ordenar el codi font de la VM simbòlica i afegir-hi comentaris, penso posar-lo a GitHub per accedir-hi gratuïtament.
Font: www.habr.com