Formele verificatie is de verificatie van het ene programma of algoritme met behulp van een ander programma.
Dit is een van de krachtigste methoden waarmee je alle kwetsbaarheden in een programma kunt vinden of kunt bewijzen dat ze niet bestaan.
Een meer gedetailleerde beschrijving van formele verificatie is te zien in het voorbeeld van het oplossen van het probleem in mijn vorige artikel.
In dit artikel ga ik van formele verificatie van problemen over naar programma's en beschrijf ik hoe
hoe kunnen ze automatisch worden omgezet in formele regelsystemen?
Om dit te doen, schreef ik mijn eigen analoog van een virtuele machine, waarbij ik symbolische principes gebruikte.
Het ontleedt de programmacode en vertaalt deze in een systeem van vergelijkingen (SMT), dat al programmatisch kan worden opgelost.
Omdat informatie over symbolische berekeningen nogal fragmentarisch op internet wordt gepresenteerd,
Ik zal kort omschrijven wat het is.
Symbolische berekeningen zijn een manier om gelijktijdig een programma uit te voeren op een breed scala aan gegevens en zijn het belangrijkste hulpmiddel voor formele programmaverificatie.
We kunnen bijvoorbeeld invoervoorwaarden instellen waarbij het eerste argument elke positieve waarde kan aannemen, het tweede negatief, de derde nul en het uitvoerargument bijvoorbeeld 42.
Symbolische berekeningen in één run zullen ons het antwoord geven op de vraag of het voor ons mogelijk is om het gewenste resultaat te verkrijgen en een voorbeeld van een reeks van dergelijke invoerparameters. Of een bewijs dat dergelijke parameters niet bestaan.
Bovendien kunnen we de invoerargumenten instellen op alle mogelijke argumenten en alleen de uitvoerargumenten selecteren, bijvoorbeeld het beheerderswachtwoord.
In dit geval zullen we alle kwetsbaarheden van het programma vinden of een bewijs krijgen dat het beheerderswachtwoord veilig is.
Opgemerkt kan worden dat de klassieke uitvoering van een programma met specifieke invoergegevens een speciaal geval van symbolische uitvoering is.
Daarom kan mijn karakter-VM ook werken in de emulatiemodus van een standaard virtuele machine.
In de commentaren op het vorige artikel vindt u terechte kritiek op de formele verificatie, met een bespreking van de zwakke punten ervan.
De belangrijkste problemen zijn:
- Combinatorische explosie, aangezien formele verificatie uiteindelijk neerkomt op P=NP
- Het verwerken van oproepen naar het bestandssysteem, netwerken en andere externe opslag is moeilijker te verifiëren
- Bugs in de specificatie, wanneer de klant of programmeur iets bedoelde, maar dit niet nauwkeurig genoeg omschreef in de technische specificatie.
Het resultaat is dat het programma wordt geverifieerd en voldoet aan de specificatie, maar iets heel anders doet dan wat de makers ervan verwachtten.
Omdat ik in dit artikel vooral de toepassing van formele verificatie in de praktijk beschouw, zal ik voorlopig niet met mijn hoofd tegen de muur stoten, maar kiezen voor een systeem waarbij de algoritmische complexiteit en het aantal externe oproepen minimaal zijn.
Omdat slimme contracten het beste bij deze eisen passen, viel de keuze op RIDE-contracten van het Waves-platform: ze zijn niet Turing-compleet en hun maximale complexiteit is kunstmatig beperkt.
Maar we zullen ze uitsluitend vanuit de technische kant bekijken.
Bovendien zal formele verificatie vooral nodig zijn voor alle contracten: het is meestal onmogelijk om een contractfout te corrigeren nadat deze is gelanceerd.
En de kosten van dergelijke fouten kunnen erg hoog zijn, omdat er vaak vrij grote hoeveelheden geld in slimme contracten worden opgeslagen.
Mijn symbolische virtuele machine is geschreven in PHP en Python en gebruikt Z3Prover van Microsoft Research om de resulterende SMT-formules op te lossen.
De kern is een krachtige multi-transactionele zoekopdracht, die
stelt u in staat oplossingen of kwetsbaarheden te vinden, zelfs als daarvoor veel transacties nodig zijn.
Zelfs , een van de krachtigste symbolische raamwerken voor het vinden van Ethereum-kwetsbaarheden, heeft deze mogelijkheid pas een paar maanden geleden toegevoegd.
Maar het is de moeite waard om op te merken dat ethercontracten complexer zijn en dat Turing compleet is.
PHP vertaalt de broncode van het RIDE smart contract in een Python-script, waarin het programma wordt gepresenteerd als een Z3 SMT-compatibel systeem van contractstaten en voorwaarden voor hun overgangen:
Nu zal ik in meer detail beschrijven wat er binnen gebeurt.
Maar eerst een paar woorden over de RIDE slimme contracttaal.
Het is een functionele en op expressies gebaseerde programmeertaal die lui van opzet is.
RIDE draait geïsoleerd binnen de blockchain en kan informatie ophalen en schrijven uit opslag die is gekoppeld aan de portemonnee van de gebruiker.
U kunt aan elke portemonnee een RIDE-contract koppelen en het resultaat van de uitvoering zal alleen WAAR of ONWAAR zijn.
TRUE betekent dat het slimme contract de transactie toestaat, en FALSE betekent dat het deze verbiedt.
Een eenvoudig voorbeeld: een script kan een overdracht verbieden als het portemonneesaldo minder dan 100 is.
Als voorbeeld neem ik dezelfde Wolf, Geit en Kool, maar dan al gepresenteerd in de vorm van een slim contract.
De gebruiker kan pas geld opnemen uit de portemonnee waarop het contract is ingezet als hij iedereen naar de andere kant heeft gestuurd.
#Извлекаем положение всех объектов из блокчейна
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 extraheert eerst alle variabelen uit het slimme contract in de vorm van hun sleutels en de bijbehorende Booleaanse expressievariabele.
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 converteert ze vervolgens naar een Z3Prover SMT-compatibele systeembeschrijving in Python.
De gegevens worden in een lus gewikkeld, waarbij opslagvariabelen index i ontvangen, transactievariabelen index i + 1, en variabelen met uitdrukkingen de regels bepalen voor de overgang van de vorige staat naar de volgende.
Dit is het hart van onze virtuele machine, die een multi-transactionele zoekmachine biedt.
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] )
De voorwaarden worden gesorteerd en ingevoegd in een scriptsjabloon dat is ontworpen om het SMT-systeem in Python te beschrijven.
Lege sjabloon
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()
Voor de laatste status in de gehele keten gelden de regels die zijn vastgelegd in het onderdeel overboekingstransactie.
Dit betekent dat Z3Prover op zoek zal gaan naar precies zulke voorwaarden die het uiteindelijk mogelijk zullen maken om geld uit het contract te halen.
Als gevolg hiervan ontvangen wij automatisch een volledig functioneel SMT-model van ons contract.
Je kunt zien dat het erg lijkt op het model uit mijn vorige artikel, dat ik handmatig heb samengesteld.
Voltooid sjabloon
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()
Na de lancering lost Z3Prover het slimme contract op en biedt het ons een reeks transacties waarmee we geld kunnen opnemen:
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
Naast het veerbootcontract kunt u experimenteren met uw eigen contracten of dit eenvoudige voorbeeld proberen, dat in 2 transacties is opgelost.
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
}
Omdat dit de allereerste versie is, is de syntaxis zeer beperkt en kunnen er bugs voorkomen.
In de volgende artikelen ben ik van plan de verdere ontwikkeling van de VM te bespreken en te laten zien hoe je met behulp hiervan formeel geverifieerde slimme contracten kunt creëren, en deze niet alleen kunt oplossen.
De virtuele karaktermachine is beschikbaar op
Nadat ik de broncode van de symbolische VM op orde heb gebracht en daar commentaar heb toegevoegd, ben ik van plan deze op GitHub te plaatsen voor gratis toegang.
Bron: www.habr.com