A verificação formal é a verificação de um programa ou algoritmo usando outro.
Este é um dos métodos mais poderosos que permite encontrar todas as vulnerabilidades de um programa ou provar que elas não existem.
Uma descrição mais detalhada da verificação formal pode ser vista no exemplo de resolução do problema de no meu artigo anterior.
Neste artigo passo da verificação formal de problemas para programas e descrevo como
como eles podem ser convertidos automaticamente em sistemas de regras formais.
Para fazer isso, escrevi meu próprio análogo de máquina virtual, usando princípios simbólicos.
Ele analisa o código do programa e o traduz em um sistema de equações (SMT), que já pode ser resolvido programaticamente.
Como as informações sobre cálculos simbólicos são apresentadas na Internet de forma bastante fragmentada,
Descreverei brevemente o que é.
A computação simbólica é uma forma de executar simultaneamente um programa em uma ampla gama de dados e é a principal ferramenta para verificação formal do programa.
Por exemplo, podemos definir condições de entrada onde o primeiro argumento pode assumir quaisquer valores positivos, o segundo negativo, o terceiro zero e o argumento de saída, por exemplo, 42.
Cálculos simbólicos em uma única execução nos darão a resposta se é possível obter o resultado desejado e um exemplo de um conjunto de tais parâmetros de entrada. Ou prova de que não existem tais parâmetros.
Além disso, podemos definir os argumentos de entrada para todos os possíveis e selecionar apenas os de saída, por exemplo, a senha do administrador.
Neste caso, encontraremos todas as vulnerabilidades do programa ou obteremos provas de que a senha do administrador é segura.
Pode-se notar que a execução clássica de um programa com dados de entrada específicos é um caso especial de execução simbólica.
Portanto, minha VM de personagem também pode funcionar no modo de emulação de uma máquina virtual padrão.
Nos comentários ao artigo anterior podemos encontrar críticas justas à verificação formal com uma discussão das suas fraquezas.
Os principais problemas são:
- Explosão combinatória, já que a verificação formal se resume a P = NP
- O processamento de chamadas para o sistema de arquivos, redes e outros armazenamentos externos é mais difícil de verificar
- Bugs na especificação, quando o cliente ou programador pretendia algo, mas não o descreveu com precisão suficiente na especificação técnica.
Com isso, o programa será verificado e estará em conformidade com as especificações, mas fará algo completamente diferente do que os criadores esperavam dele.
Como neste artigo estou considerando principalmente o uso da verificação formal na prática, não vou bater a cabeça na parede por enquanto e escolherei um sistema onde a complexidade algorítmica e o número de chamadas externas sejam mínimos.
Como os contratos inteligentes atendem melhor a esses requisitos, a escolha recaiu sobre os contratos RIDE da plataforma Waves: eles não são Turing completos e sua complexidade máxima é artificialmente limitada.
Mas iremos considerá-los exclusivamente do lado técnico.
Além de tudo, a verificação formal será especialmente exigida para qualquer contrato: normalmente é impossível corrigir um erro de contrato depois de lançado.
E o custo de tais erros pode ser muito alto, uma vez que grandes quantidades de fundos são frequentemente armazenadas em contratos inteligentes.
Minha máquina virtual simbólica é escrita em PHP e Python e usa Z3Prover da Microsoft Research para resolver as fórmulas SMT resultantes.
Em sua essência está uma poderosa pesquisa multitransacional, que
permite encontrar soluções ou vulnerabilidades, mesmo que isso exija muitas transações.
Mesmo , uma das estruturas simbólicas mais poderosas para encontrar vulnerabilidades do Ethereum, adicionou esse recurso apenas há alguns meses.
Mas é importante notar que os contratos Ether são mais complexos e Turing completos.
PHP traduz o código-fonte do contrato inteligente RIDE em um script python, no qual o programa é apresentado como um sistema de estados de contrato e condições de contrato compatível com Z3 SMT para suas transições:
Agora vou descrever o que está acontecendo lá dentro com mais detalhes.
Mas primeiro, algumas palavras sobre a linguagem do contrato inteligente RIDE.
É uma linguagem de programação funcional e baseada em expressões que é preguiçosa por design.
O RIDE é executado isoladamente no blockchain e pode recuperar e gravar informações do armazenamento vinculado à carteira do usuário.
Você pode anexar um contrato RIDE a cada carteira e o resultado da execução será apenas VERDADEIRO ou FALSO.
VERDADEIRO significa que o contrato inteligente permite a transação e FALSO significa que a proíbe.
Um exemplo simples: um script pode proibir uma transferência se o saldo da carteira for inferior a 100.
Como exemplo, pegarei o mesmo Lobo, Cabra e Repolho, mas já apresentado na forma de contrato inteligente.
O usuário não poderá sacar dinheiro da carteira na qual o contrato está implantado até que tenha enviado todos para o 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
}
O PHP primeiro extrai todas as variáveis do contrato inteligente na forma de suas chaves e a variável de expressão booleana correspondente.
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
O PHP então os converte em uma descrição de sistema compatível com Z3Prover SMT em Python.
Os dados são agrupados em um loop, onde as variáveis de armazenamento recebem o índice i, as variáveis de transação o índice i + 1 e as variáveis com expressões definem as regras de transição do estado anterior para o próximo.
Este é o coração da nossa máquina virtual, que fornece um mecanismo de pesquisa multitransacional.
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 condições são classificadas e inseridas em um modelo de script projetado para descrever o sistema SMT em Python.
Modelo em 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 cadeia, são aplicadas as regras especificadas na seção de transação de transferência.
Isso significa que o Z3Prover procurará precisamente os conjuntos de condições que, em última instância, permitirão a retirada de fundos do contrato.
Como resultado, recebemos automaticamente um modelo SMT totalmente funcional do nosso contrato.
Você pode ver que é muito semelhante ao modelo do meu artigo anterior, que compilei manualmente.
Modelo concluído
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()
Após o lançamento, o Z3Prover resolve o contrato inteligente e nos fornece uma cadeia de transações que nos permitirá sacar fundos:
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
Além do contrato de ferry, você pode experimentar seus próprios contratos ou tentar este exemplo simples, que se resolve em 2 transações.
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
}
Como esta é a primeira versão, a sintaxe é muito limitada e pode haver bugs.
Nos artigos a seguir, pretendo abordar o desenvolvimento da VM e mostrar como você pode criar contratos inteligentes formalmente verificados com sua ajuda, e não apenas resolvê-los.
A máquina virtual do personagem está disponível em
Depois de colocar o código-fonte da VM simbólica em ordem e adicionar comentários lá, pretendo colocá-lo no GitHub para acesso gratuito.
Fonte: habr.com