Formel verifikation er verifikation af et program eller en algoritme ved hjælp af et andet.
Dette er en af de mest kraftfulde metoder, der giver dig mulighed for at finde alle sårbarheder i et program eller bevise, at de ikke eksisterer.
En mere detaljeret beskrivelse af formel verifikation kan ses i eksemplet med løsning af problemet vedr i min tidligere artikel.
I denne artikel går jeg fra formel verifikation af problemer til programmer og beskriver hvordan
hvordan kan de automatisk konverteres til formelle regelsystemer.
For at gøre dette skrev jeg min egen analog af en virtuel maskine ved hjælp af symbolske principper.
Den analyserer programkoden og oversætter den til et system af ligninger (SMT), som allerede kan løses programmatisk.
Da information om symbolske beregninger præsenteres på internettet ret fragmentarisk,
Jeg vil kort beskrive, hvad det er.
Symbolsk beregning er en måde at udføre et program på en bred vifte af data samtidigt og er det vigtigste værktøj til formel programverifikation.
For eksempel kan vi indstille inputbetingelser, hvor det første argument kan tage alle positive værdier, det andet negative, det tredje nul og outputargumentet, for eksempel 42.
Symbolske beregninger i en kørsel vil give os svaret på, om det er muligt for os at opnå det ønskede resultat og et eksempel på et sæt af sådanne inputparametre. Eller bevis på, at der ikke er sådanne parametre.
Desuden kan vi indstille input-argumenterne til alle mulige og kun vælge output-argumenterne, for eksempel administratoradgangskoden.
I dette tilfælde vil vi finde alle programmets sårbarheder eller få bevis for, at administratorens adgangskode er sikker.
Det kan bemærkes, at den klassiske udførelse af et program med specifikke inputdata er et særligt tilfælde af symbolsk udførelse.
Derfor kan min karakter VM også arbejde i emuleringstilstand på en standard virtuel maskine.
I kommentarerne til den forrige artikel kan man finde rimelig kritik af formel verifikation med en diskussion af dens svagheder.
Hovedproblemerne er:
- Kombinatorisk eksplosion, da formel verifikation i sidste ende kommer ned til P=NP
- Behandling af opkald til filsystemet, netværk og anden ekstern lagring er sværere at verificere
- Fejl i specifikationen, når kunden eller programmøren havde til hensigt en ting, men ikke beskrev det præcist nok i den tekniske specifikation.
Som følge heraf vil programmet blive verificeret og overholde specifikationen, men vil gøre noget helt andet end det, skaberne forventede af det.
Da jeg i denne artikel hovedsageligt overvejer brugen af formel verifikation i praksis, vil jeg ikke banke hovedet mod væggen indtil videre, og vil vælge et system, hvor den algoritmiske kompleksitet og antallet af eksterne opkald er minimalt.
Da smarte kontrakter bedst passer til disse krav, faldt valget på RIDE-kontrakter fra Waves platformen: de er ikke Turing komplette, og deres maksimale kompleksitet er kunstigt begrænset.
Men vi vil udelukkende betragte dem fra den tekniske side.
Ud over alt vil formel verifikation især være efterspurgt for eventuelle kontrakter: det er normalt umuligt at rette en kontraktfejl efter den er blevet lanceret.
Og omkostningerne ved sådanne fejl kan være meget høje, da ret store mængder af midler ofte er gemt på smarte kontrakter.
Min symbolske virtuelle maskine er skrevet i PHP og Python, og bruger Z3Prover fra Microsoft Research til at løse de resulterende SMT-formler.
Kernen er en kraftfuld multi-transaktionel søgning, som
giver dig mulighed for at finde løsninger eller sårbarheder, selvom det kræver mange transaktioner.
Selv , en af de mest kraftfulde symbolske rammer til at finde Ethereum-sårbarheder, tilføjede kun denne funktion for et par måneder siden.
Men det er værd at bemærke, at etherkontrakter er mere komplekse og Turing komplette.
PHP oversætter kildekoden til RIDE smart kontrakten til et python-script, hvor programmet præsenteres som et Z3 SMT-kompatibelt system af kontrakttilstande og betingelser for deres overgange:
Nu vil jeg beskrive, hvad der sker indeni mere detaljeret.
Men først et par ord om RIDE smart kontraktsproget.
Det er et funktionelt og udtryksbaseret programmeringssprog, der er dovent af design.
RIDE kører isoleret inden for blockchain og kan hente og skrive information fra lager knyttet til brugerens tegnebog.
Du kan knytte en RIDE-kontrakt til hver tegnebog, og resultatet af udførelsen vil kun være SAND eller FALSK.
TRUE betyder, at den smarte kontrakt tillader transaktionen, og FALSE betyder, at den forbyder den.
Et simpelt eksempel: et script kan forbyde en overførsel, hvis tegnebogens saldo er mindre end 100.
Som et eksempel vil jeg tage den samme ulv, ged og kål, men allerede præsenteret i form af en smart kontrakt.
Brugeren vil ikke være i stand til at hæve penge fra tegnebogen, som kontrakten er indsat på, før han har sendt alle til den anden side.
#Извлекаем положение всех объектов из блокчейна
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 udtrækker først alle variablerne fra den smarte kontrakt i form af deres nøgler og den tilsvarende boolske udtryksvariabel.
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 konverterer dem derefter til en Z3Prover SMT-kompatibel systembeskrivelse i Python.
Dataene pakkes ind i en løkke, hvor lagringsvariabler modtager indeks i, transaktionsvariable indeks i + 1, og variabler med udtryk sætter reglerne for overgang fra den forrige tilstand til den næste.
Dette er selve hjertet i vores virtuelle maskine, som giver en multi-transaktionel søgemaskine.
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] )
Betingelserne er sorteret og indsat i en scriptskabelon designet til at beskrive SMT-systemet i Python.
Tom skabelon
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()
For den sidste stat i hele kæden anvendes de regler, der er specificeret i afsnittet om overførselstransaktioner.
Det betyder, at Z3Prover vil lede efter netop sådanne sæt betingelser, der i sidste ende vil tillade, at midler trækkes tilbage fra kontrakten.
Som et resultat modtager vi automatisk en fuldt funktionel SMT-model af vores kontrakt.
Du kan se, at den minder meget om modellen fra min tidligere artikel, som jeg kompilerede manuelt.
Fuldført skabelon
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()
Efter lanceringen løser Z3Prover den smarte kontrakt og giver os en kæde af transaktioner, der giver os mulighed for at hæve penge:
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
Udover færgekontrakten kan du eksperimentere med dine egne kontrakter eller prøve dette simple eksempel, som løses i 2 transaktioner.
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
}
Da dette er den allerførste version, er syntaksen meget begrænset, og der kan være fejl.
I de følgende artikler planlægger jeg at dække den videre udvikling af VM'en, og vise hvordan du kan skabe formelt verificerede smarte kontrakter med dens hjælp, og ikke bare løse dem.
Den virtuelle karaktermaskine er tilgængelig på
Efter at have sat kildekoden til den symbolske VM i rækkefølge og tilføjet kommentarer der, planlægger jeg at lægge den på GitHub for gratis adgang.
Kilde: www.habr.com