A verificación formal é a verificación dun programa ou algoritmo mediante outro.
Este é un dos métodos máis poderosos que permite atopar todas as vulnerabilidades nun programa ou demostrar que non existen.
Unha descrición máis detallada da verificación formal pódese ver no exemplo de resolución do problema de no meu artigo anterior.
Neste artigo paso da verificación formal de problemas aos programas e describo como
como se poden converter en sistemas de regras formais automaticamente.
Para iso, escribín o meu propio análogo dunha máquina virtual, utilizando principios simbólicos.
Analiza o código do programa e tradúceo nun sistema de ecuacións (SMT), que xa se pode resolver mediante programación.
Dado que a información sobre cálculos simbólicos se presenta en Internet de forma bastante fragmentaria,
Vou describir brevemente o que é.
A computación simbólica é unha forma de executar simultaneamente un programa nunha ampla gama de datos e é a principal ferramenta para a verificación formal do programa.
Por exemplo, podemos establecer condicións de entrada onde o primeiro argumento pode tomar calquera valor positivo, o segundo negativo, o terceiro cero e o argumento de saída, por exemplo, 42.
Os cálculos simbólicos nunha soa carreira daranos a resposta sobre se é posible obter o resultado desexado e un exemplo dun conxunto de tales parámetros de entrada. Ou proba de que non existen tales parámetros.
Ademais, podemos establecer os argumentos de entrada para todos os posibles e seleccionar só os de saída, por exemplo, o contrasinal do administrador.
Neste caso, atoparemos todas as vulnerabilidades do programa ou obteremos probas de que o contrasinal do administrador está seguro.
Pódese sinalar que a execución clásica dun programa con datos de entrada específicos é un caso especial de execución simbólica.
Polo tanto, o meu personaxe VM tamén pode funcionar en modo de emulación dunha máquina virtual estándar.
Nos comentarios do artigo anterior pódese atopar unha crítica xusta á verificación formal cunha discusión das súas debilidades.
Os principais problemas son:
- Explosión combinatoria, xa que a verificación formal se reduce finalmente a P=NP
- Procesar chamadas ao sistema de ficheiros, redes e outro almacenamento externo é máis difícil de verificar
- Erros na especificación, cando o cliente ou programador pretendía unha cousa, pero non a describiu con suficiente precisión na especificación técnica.
Como resultado, o programa verificarase e cumprirá coa especificación, pero fará algo completamente diferente do que os creadores esperaban del.
Dado que neste artigo estou considerando principalmente o uso da verificación formal na práctica, por agora non vou bater a cabeza contra a parede e escollerei un sistema onde a complexidade algorítmica e o número de chamadas externas sexan mínimos.
Dado que os contratos intelixentes se adaptan mellor a estes requisitos, a elección recaeu nos contratos RIDE da plataforma Waves: non están Turing completos e a súa máxima complexidade está limitada artificialmente.
Pero considerarémolos exclusivamente desde o lado técnico.
Ademais de todo, a verificación formal será especialmente demandada para calquera contrato: adoita ser imposible corrixir un erro de contrato despois de que se lanzou.
E o custo destes erros pode ser moi alto, xa que moitas veces se almacenan cantidades bastante grandes de fondos en contratos intelixentes.
A miña máquina virtual simbólica está escrita en PHP e Python e usa Z3Prover de Microsoft Research para resolver as fórmulas SMT resultantes.
No seu núcleo está unha potente busca multi-transacción, que
permítelle atopar solucións ou vulnerabilidades, aínda que requira moitas transaccións.
Mesmo , un dos marcos simbólicos máis poderosos para atopar vulnerabilidades de Ethereum, só engadiu esta capacidade hai uns meses.
Pero vale a pena sinalar que os contratos de éter son máis complexos e Turing completo.
PHP traduce o código fonte do contrato intelixente RIDE nun script Python, no que o programa se presenta como un sistema compatible con Z3 SMT de estados de contrato e condicións para as súas transicións:
Agora describirei con máis detalle o que está a suceder dentro.
Pero primeiro, algunhas palabras sobre a linguaxe do contrato intelixente RIDE.
É unha linguaxe de programación funcional e baseada en expresións que é preguiceiro polo deseño.
RIDE execútase illado dentro da cadea de bloques e pode recuperar e escribir información do almacenamento ligado á carteira do usuario.
Podes anexar un contrato RIDE a cada carteira e o resultado da execución só será VERDADEIRO ou FALSO.
VERDADEIRO significa que o contrato intelixente permite a transacción e FALSO significa que a prohibe.
Un exemplo sinxelo: un script pode prohibir unha transferencia se o saldo da carteira é inferior a 100.
Como exemplo, tomarei os mesmos Lobo, Cabra e Repolo, pero xa presentados en forma de contrato intelixente.
O usuario non poderá retirar cartos da carteira na que se desprega o contrato ata que os envíe ao outro lado.
#Извлекаем положение всех объектов из блокчейна
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 extrae primeiro todas as variables do contrato intelixente en forma das súas claves e da correspondente variable de expresión 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
Despois PHP convérteos nunha descrición do sistema compatible con Z3Prover SMT en Python.
Os datos están envoltos nun bucle, onde as variables de almacenamento reciben o índice i, as variables de transacción índice i + 1 e as variables con expresións establecen as regras para a transición do estado anterior ao seguinte.
Este é o corazón da nosa máquina virtual, que ofrece un motor de busca multitransacción.
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] )
As condicións ordénanse e insírense nun modelo de script deseñado para describir o sistema SMT en Python.
Modelo en branco
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()
Para o último estado de toda a cadea, aplícanse as regras que se especifican na sección de transaccións de transferencia.
Isto significa que Z3Prover buscará precisamente estes conxuntos de condicións que permitan finalmente retirar fondos do contrato.
Como resultado, recibimos automaticamente un modelo SMT totalmente funcional do noso contrato.
Podes ver que é moi semellante ao modelo do meu artigo anterior, que compilei manualmente.
Modelo completado
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()
Despois do lanzamento, Z3Prover resolve o contrato intelixente e proporciónanos unha cadea de transaccións que nos permitirán retirar fondos:
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
Ademais do contrato de ferry, podes probar cos teus propios contratos ou probar este sinxelo exemplo, que se resolve en 2 transaccións.
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
}
Dado que esta é a primeira versión, a sintaxe é moi limitada e pode haber erros.
Nos seguintes artigos, penso cubrir o desenvolvemento da máquina virtual e mostrar como podes crear contratos intelixentes verificados formalmente coa súa axuda, e non só resolvelos.
A máquina virtual de personaxes está dispoñible en
Despois de poñer en orde o código fonte da máquina virtual simbólica e engadir comentarios alí, penso poñelo en GitHub para o acceso gratuíto.
Fonte: www.habr.com