La verifica formale è la verifica di un programma o algoritmo utilizzandone un altro.
Questo è uno dei metodi più potenti che ti consente di trovare tutte le vulnerabilità in un programma o dimostrare che non esistono.
Una descrizione più dettagliata della verifica formale può essere vista nell'esempio della risoluzione del problema di nel mio articolo precedente.
In questo articolo passo dalla verifica formale dei problemi ai programmi e descrivo come
come possono essere convertiti automaticamente in sistemi di regole formali.
Per fare ciò, ho scritto il mio analogo di una macchina virtuale, utilizzando principi simbolici.
Analizza il codice del programma e lo traduce in un sistema di equazioni (SMT), che può già essere risolto a livello di codice.
Poiché le informazioni sui calcoli simbolici sono presentate su Internet in modo piuttosto frammentario,
Descriverò brevemente di cosa si tratta.
Il calcolo simbolico è un modo per eseguire simultaneamente un programma su un'ampia gamma di dati ed è lo strumento principale per la verifica formale del programma.
Ad esempio, possiamo impostare condizioni di input in cui il primo argomento può assumere qualsiasi valore positivo, il secondo negativo, il terzo zero e l'argomento di output, ad esempio, 42.
I calcoli simbolici in un'unica esecuzione ci daranno la risposta se è possibile ottenere il risultato desiderato e un esempio di un insieme di tali parametri di input. O la prova che tali parametri non esistono.
Inoltre, possiamo impostare tutti gli argomenti di input possibili e selezionare solo quelli di output, ad esempio la password dell'amministratore.
In questo caso troveremo tutte le vulnerabilità del programma o otterremo la prova che la password dell’amministratore è sicura.
Si può notare che l'esecuzione classica di un programma con dati di input specifici è un caso speciale di esecuzione simbolica.
Pertanto, la VM del mio personaggio può funzionare anche in modalità emulazione di una macchina virtuale standard.
Nei commenti all'articolo precedente si può trovare una giusta critica alla verifica formale con una discussione sui suoi punti deboli.
I problemi principali sono:
- Esplosione combinatoria, poiché la verifica formale alla fine si riduce a P=NP
- L'elaborazione delle chiamate al file system, alle reti e ad altri dispositivi di archiviazione esterni è più difficile da verificare
- Bug nelle specifiche, quando il cliente o il programmatore intendeva una cosa, ma non la descriveva in modo sufficientemente accurato nelle specifiche tecniche.
Di conseguenza, il programma verrà verificato e rispetterà le specifiche, ma farà qualcosa di completamente diverso da ciò che i creatori si aspettavano da esso.
Poiché in questo articolo considererò principalmente l'uso pratico della verifica formale, per ora non sbatterò la testa contro il muro e sceglierò un sistema in cui la complessità algoritmica e il numero di chiamate esterne sono minimi.
Poiché i contratti intelligenti si adattano meglio a questi requisiti, la scelta è caduta sui contratti RIDE della piattaforma Waves: non sono Turing Complete e la loro massima complessità è limitata artificialmente.
Ma li considereremo esclusivamente dal lato tecnico.
Oltre a tutto, la verifica formale sarà particolarmente richiesta per eventuali contratti: di solito è impossibile correggere un errore contrattuale dopo che è stato avviato.
E il costo di tali errori può essere molto elevato, poiché quantità piuttosto elevate di fondi vengono spesso archiviate nei contratti intelligenti.
La mia macchina virtuale simbolica è scritta in PHP e Python e utilizza Z3Prover di Microsoft Research per risolvere le formule SMT risultanti.
Al centro c'è una potente ricerca multitransazionale, che
ti consente di trovare soluzioni o vulnerabilità, anche se richiede molte transazioni.
Anche , uno dei framework simbolici più potenti per individuare le vulnerabilità di Ethereum, ha aggiunto questa funzionalità solo pochi mesi fa.
Ma vale la pena notare che i contratti eterei sono più complessi e Turing è completo.
PHP traduce il codice sorgente del contratto intelligente RIDE in uno script Python, in cui il programma viene presentato come un sistema compatibile con Z3 SMT di stati contrattuali e condizioni per le loro transizioni:
Ora descriverò cosa sta succedendo all'interno in modo più dettagliato.
Ma prima, qualche parola sul linguaggio del contratto intelligente RIDE.
È un linguaggio di programmazione funzionale e basato sulle espressioni che è pigro per progettazione.
RIDE funziona in modo isolato all'interno della blockchain e può recuperare e scrivere informazioni dallo spazio di archiviazione collegato al portafoglio dell'utente.
Puoi allegare un contratto RIDE a ciascun portafoglio e il risultato dell'esecuzione sarà solo VERO o FALSO.
VERO significa che il contratto intelligente consente la transazione e FALSO significa che la vieta.
Un semplice esempio: uno script può vietare un trasferimento se il saldo del portafoglio è inferiore a 100.
Ad esempio, prenderò gli stessi Lupo, Capra e Cavolo, ma già presentati sotto forma di contratto intelligente.
L'utente non potrà prelevare denaro dal portafoglio su cui è distribuito il contratto finché non avrà mandato tutti dall'altra parte.
#Извлекаем положение всех объектов из блокчейна
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 estrae prima tutte le variabili dallo smart contract sotto forma di chiavi e la corrispondente variabile di espressione 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
PHP li converte quindi in una descrizione del sistema compatibile con Z3Prover SMT in Python.
I dati sono racchiusi in un ciclo, in cui le variabili di archiviazione ricevono l'indice i, le variabili di transazione l'indice i + 1 e le variabili con espressioni impostano le regole per la transizione dallo stato precedente a quello successivo.
Questo è il cuore della nostra macchina virtuale, che fornisce un motore di ricerca multi-transazionale.
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] )
Le condizioni vengono ordinate e inserite in un modello di script progettato per descrivere il sistema SMT in Python.
Modello vuoto
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 l'ultimo stato dell'intera catena vengono applicate le regole specificate nella sezione transazione di trasferimento.
Ciò significa che Z3Prover cercherà esattamente le condizioni che alla fine consentiranno il ritiro dei fondi dal contratto.
Di conseguenza, riceviamo automaticamente un modello SMT completamente funzionante del nostro contratto.
Puoi vedere che è molto simile al modello del mio articolo precedente, che ho compilato manualmente.
Modello completato
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()
Dopo il lancio, Z3Prover risolve il contratto intelligente e ci fornisce una catena di transazioni che ci permetterà di prelevare fondi:
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
Oltre al contratto del traghetto, puoi sperimentare i tuoi contratti o provare questo semplice esempio, che si risolve in 2 transazioni.
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
}
Poiché questa è la primissima versione, la sintassi è molto limitata e potrebbero esserci dei bug.
Nei seguenti articoli, intendo coprire l'ulteriore sviluppo della VM e mostrare come è possibile creare contratti intelligenti formalmente verificati con il suo aiuto e non solo risolverli.
La macchina virtuale del personaggio è disponibile su
Dopo aver messo in ordine il codice sorgente della VM simbolica e aver aggiunto i commenti lì, ho intenzione di metterlo su GitHub per l'accesso gratuito.
Fonte: habr.com