La verificación formal es la verificación de un programa o algoritmo utilizando otro.
Este es uno de los métodos más poderosos que le permite encontrar todas las vulnerabilidades en un programa o demostrar que no existen.
Se puede ver una descripción más detallada de la verificación formal en el ejemplo de resolución del problema de en mi artículo anterior.
En este artículo paso de la verificación formal de problemas a los programas y describo cómo
¿Cómo pueden convertirse automáticamente en sistemas de reglas formales?
Para ello, escribí mi propio análogo de una máquina virtual, utilizando principios simbólicos.
Analiza el código del programa y lo traduce a un sistema de ecuaciones (SMT), que ya se puede resolver mediante programación.
Dado que la información sobre cálculos simbólicos en Internet se presenta de forma bastante fragmentaria,
Describiré brevemente de qué se trata.
La computación simbólica es una forma de ejecutar simultáneamente un programa en una amplia gama de datos y es la herramienta principal para la verificación formal del programa.
Por ejemplo, podemos establecer condiciones de entrada donde el primer argumento puede tomar cualquier valor positivo, el segundo negativo, el tercero cero y el argumento de salida, por ejemplo, 42.
Los cálculos simbólicos de una sola vez nos darán la respuesta sobre si es posible obtener el resultado deseado y un ejemplo de un conjunto de dichos parámetros de entrada. O prueba de que no existen tales parámetros.
Además, podemos establecer los argumentos de entrada en todos los posibles y seleccionar solo los de salida, por ejemplo, la contraseña de administrador.
En este caso encontraremos todas las vulnerabilidades del programa o obtendremos pruebas de que la contraseña del administrador es segura.
Cabe señalar que la ejecución clásica de un programa con datos de entrada específicos es un caso especial de ejecución simbólica.
Por lo tanto, mi personaje VM también puede funcionar en modo de emulación de una máquina virtual estándar.
En los comentarios al artículo anterior se pueden encontrar críticas justas a la verificación formal con una discusión de sus debilidades.
Los principales problemas son:
- Explosión combinatoria, ya que la verificación formal finalmente se reduce a P=NP
- El procesamiento de llamadas al sistema de archivos, redes y otros almacenamientos externos es más difícil de verificar
- Errores en la especificación, cuando el cliente o programador pretendía una cosa, pero no la describió con suficiente precisión en la especificación técnica.
Como resultado, el programa será verificado y cumplirá con las especificaciones, pero hará algo completamente diferente de lo que los creadores esperaban de él.
Dado que en este artículo estoy considerando principalmente el uso de la verificación formal en la práctica, por ahora no me golpearé la cabeza contra la pared y elegiré un sistema donde la complejidad algorítmica y el número de llamadas externas sean mínimos.
Dado que los contratos inteligentes se adaptan mejor a estos requisitos, la elección recayó en los contratos RIDE de la plataforma Waves: no son Turing completos y su complejidad máxima está limitada artificialmente.
Pero los consideraremos exclusivamente desde el punto de vista técnico.
Además de todo, la verificación formal será especialmente solicitada para cualquier contrato: normalmente es imposible corregir un error en el contrato una vez lanzado.
Y el coste de tales errores puede ser muy alto, ya que a menudo se almacenan cantidades bastante grandes de fondos en contratos inteligentes.
Mi máquina virtual simbólica está escrita en PHP y Python y utiliza Z3Prover de Microsoft Research para resolver las fórmulas SMT resultantes.
En esencia, se encuentra una potente búsqueda multitransaccional, que
le permite encontrar soluciones o vulnerabilidades, incluso si requiere muchas transacciones.
Incluso , uno de los marcos simbólicos más poderosos para encontrar vulnerabilidades de Ethereum, agregó esta capacidad hace solo unos meses.
Pero vale la pena señalar que los contratos de ether son más complejos y Turing está completo.
PHP traduce el código fuente del contrato inteligente RIDE a un script de Python, en el que el programa se presenta como un sistema de estados de contrato y condiciones para sus transiciones compatible con Z3 SMT:
Ahora describiré con más detalle lo que sucede dentro.
Pero primero, unas palabras sobre el lenguaje de contrato inteligente de RIDE.
Es un lenguaje de programación funcional y basado en expresiones que es vago por diseño.
RIDE se ejecuta de forma aislada dentro de la cadena de bloques y puede recuperar y escribir información desde el almacenamiento vinculado a la billetera del usuario.
Puede adjuntar un contrato RIDE a cada billetera y el resultado de la ejecución será solo VERDADERO o FALSO.
VERDADERO significa que el contrato inteligente permite la transacción y FALSO significa que la prohíbe.
Un ejemplo simple: un script puede prohibir una transferencia si el saldo de la billetera es inferior a 100.
Como ejemplo, tomaré el mismo Lobo, Cabra y Repollo, pero ya presentados en forma de contrato inteligente.
El usuario no podrá retirar dinero de la billetera en la que está implementado el contrato hasta que haya enviado todos al otro 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 primero extrae todas las variables del contrato inteligente en forma de sus claves y la variable de expresión booleana correspondiente.
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
Luego, PHP los convierte en una descripción del sistema compatible con Z3Prover SMT en Python.
Los datos se envuelven en un bucle, donde las variables de almacenamiento reciben el índice i, las variables de transacción el índice i + 1 y las variables con expresiones establecen las reglas para la transición del estado anterior al siguiente.
Este es el corazón mismo de nuestra máquina virtual, que proporciona un mecanismo de búsqueda 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] )
Las condiciones se clasifican e insertan en una plantilla de script diseñada para describir el sistema SMT en Python.
Plantilla en blanco
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 el último estado de toda la cadena se aplican las reglas que se especifican en la sección de transacciones de transferencia.
Esto significa que Z3Prover buscará precisamente aquellos conjuntos de condiciones que finalmente permitan retirar fondos del contrato.
Como resultado, recibimos automáticamente un modelo SMT completamente funcional de nuestro contrato.
Puedes ver que es muy similar al modelo de mi artículo anterior, que compilé manualmente.
Plantilla completa
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()
Tras el lanzamiento, Z3Prover resuelve el contrato inteligente y nos proporciona una cadena de transacciones 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
Además del contrato de ferry, puedes experimentar con tus propios contratos o probar este sencillo ejemplo, que se resuelve en 2 transacciones.
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 es la primera versión, la sintaxis es muy limitada y puede haber errores.
En los siguientes artículos, planeo cubrir el desarrollo posterior de la VM y mostrar cómo se pueden crear contratos inteligentes formalmente verificados con su ayuda, y no solo resolverlos.
La máquina virtual de personajes está disponible en
Después de ordenar el código fuente de la VM simbólica y agregar comentarios allí, planeo ponerlo en GitHub para acceso gratuito.
Fuente: habr.com
