Formele verifikasie is die verifikasie van een program of algoritme met behulp van 'n ander.
Dit is een van die kragtigste metodes waarmee u al die kwesbaarhede in die program kan vind of bewys dat dit nie bestaan nie.
'n Meer gedetailleerde beskrywing van formele verifikasie kan gesien word in die voorbeeld van die oplossing van die probleem van in my vorige artikel.
In hierdie artikel beweeg ek van formele probleemverifikasie na programme en beskryf ek hoe
hoe jy dit outomaties in stelsels van formele reëls kan omskep.
Om dit te doen, het ek my analoog van 'n virtuele masjien geskryf, op simboliese beginsels.
Dit ontleed die programkode en vertaal dit in 'n stelsel van vergelykings (SBS), wat reeds programmaties opgelos kan word.
Aangesien inligting oor simboliese berekeninge redelik fragmentaries op die internet aangebied word,
Ek sal kortliks beskryf wat dit is.
Simboliese berekeninge is 'n manier om 'n program gelyktydig op 'n wye reeks data uit te voer en is die hoofinstrument vir formele programverifikasie.
Ons kan byvoorbeeld insetvoorwaardes stel waar die eerste argument enige positiewe waarde kan aanneem, die tweede negatief kan wees, die derde nul kan wees, en die uitvoerargument is byvoorbeeld 42.
Simboliese berekeninge in een lopie sal vir ons 'n antwoord gee of dit vir ons moontlik is om die gewenste resultaat te verkry en 'n voorbeeld van 'n stel sulke invoerparameters. Of bewys dat daar nie sulke parameters is nie.
Boonop kan ons die invoerargumente in die algemeen as alles moontlik stel, en slegs die uitvoer kies, byvoorbeeld die administrateurwagwoord.
In hierdie geval sal ons al die kwesbaarhede van die program vind, of ons sal bewys kry dat die administrateurwagwoord veilig is.
Dit kan gesien word dat die klassieke uitvoering van 'n program met spesifieke invoerdata 'n spesiale geval van 'n simboliese een is.
Daarom kan my karakter VM ook in die emulasiemodus van 'n standaard virtuele masjien werk.
In die kommentaar op die vorige artikel kan 'n mens ook regverdige kritiek op formele verifikasie vind met 'n bespreking van die swakhede daarvan.
Die hoofprobleme is:
- Kombinatoriese ontploffing, aangesien formele verifikasie uiteindelik op P=NP berus
- Die hantering van oproepe na die lêerstelsel, netwerke en ander eksterne berging is moeiliker om te verifieer
- Foute in die spesifikasie, wanneer die kliënt of programmeerder een ding bedink het, maar dit nie akkuraat in die TOR beskryf het nie.
As gevolg hiervan sal die program geverifieer word en aan die spesifikasie voldoen, maar sal iets heeltemal anders doen as wat die skeppers daarvan verwag het.
Aangesien ek in hierdie artikel hoofsaaklik die toepassing van formele verifikasie in die praktyk oorweeg, sal ek vir eers nie my voorkop teen die muur klop nie, en ek sal 'n stelsel kies waar die algoritmiese kompleksiteit en die aantal eksterne oproepe minimaal is.
Aangesien slim kontrakte op die beste manier aan hierdie vereistes voldoen, het die keuse op RIDE-kontrakte van die Waves-platform geval: hulle is nie Turing-volledig nie, en hul maksimum kompleksiteit is kunsmatig beperk.
Maar ons sal hulle uitsluitlik van die tegniese kant af oorweeg.
Benewens alles, vir enige kontrakte, sal formele verifikasie veral in aanvraag wees: in die reël is dit onmoontlik om 'n kontrakfout reg te stel nadat dit van stapel gestuur is.
En die prys van sulke foute kan baie hoog wees, aangesien redelik groot bedrae fondse dikwels op slim kontrakte gestoor word.
My karakter VM is in PHP en Python geskryf, en gebruik Microsoft Research se Z3Prover om die gevolglike SBS-formules op te los.
Die kern daarvan is 'n kragtige multi-transaksie soektog, wat
laat jou toe om oplossings of kwesbaarhede te vind, selfs al verg dit baie transaksies.
Selfs , een van die kragtigste karakterraamwerke om Ethereum-kwesbaarhede te vind, het hierdie vermoë eers 'n paar maande gelede bygevoeg.
Maar dit is opmerklik dat eterkontrakte meer kompleks is en Turing-voltooidheid het.
PHP vertaal die bronkode van die RIDE-slimkontrak in 'n luislangskrif, waarin die program aangebied word as 'n Z3 SMT-versoenbare stelsel van kontraktoestande en hul oorgangstoestande:
Nou sal ek in meer besonderhede beskryf wat binne gebeur.
Maar eers 'n paar woorde oor die RIDE-slimkontraktaal.
Dit is 'n funksionele en uitdrukking-gebaseerde programmeertaal wat lui van ontwerp is.
RIDE loop in isolasie binne die blokketting, en kan inligting onttrek en skryf uit die berging wat met die gebruiker se beursie geassosieer word.
'n RIDE-kontrak kan aan elke beursie geheg word, en die resultaat van uitvoering sal slegs WAAR of ONWAAR wees.
WAAR beteken dat die slim kontrak die transaksie toelaat, en ONWAAR dat dit dit verbied.
'n Eenvoudige voorbeeld: die skrif kan die oordrag verbied as die beursie-saldo minder as 100 is.
As voorbeeld sal ek dieselfde Wolf, Bok en Kool neem, maar reeds in die vorm van 'n slim kontrak aangebied.
Die gebruiker sal nie geld kan onttrek uit die beursie waarop die kontrak ontplooi is totdat hy almal anderkant toe stuur nie.
#Извлекаем положение всех объектов из блокчейна
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 onttrek eers alle veranderlikes uit die slim kontrak in die vorm van hul sleutels en die ooreenstemmende Boolese uitdrukking.
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 omskep dit dan in 'n Z3Prover SMT-versoenbare luislangstelselbeskrywing.
Die data word in 'n lus toegedraai, waar die stoorveranderlikes indeks i ontvang, die transaksieveranderlikes indeks i + 1, en die veranderlikes met uitdrukkings die reëls stel vir oorgang van die vorige toestand na die volgende.
Dit is die hart van ons virtuele masjien, wat 'n multi-transaksie soekenjin bied.
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] )
Die voorwaardes word gesorteer en in 'n skripsjabloon ingevoeg wat ontwerp is om die SBS-stelsel in luislang te beskryf.
Leë 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()
Vir die laaste toestand van die hele ketting word die reëls wat in die oordragtransaksie-afdeling gestel word, toegepas.
Dit beteken dat Z3Prover presies sulke stelle state sal soek wat jou uiteindelik sal toelaat om fondse uit die kontrak te onttrek.
Gevolglik kry ons outomaties 'n ten volle funksionele SBS-model van ons kontrak.
Jy kan sien dat dit baie soortgelyk is aan die model van my vorige artikel, wat ek met die hand saamgestel het.
Voltooide 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 bekendstelling los Z3Prover die slim kontrak op en vertoon 'n ketting transaksies vir ons, wat ons in staat sal stel om fondse te onttrek:
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
Benewens die kruiskontrak, kan u met u eie kontrakte eksperimenteer of hierdie eenvoudige voorbeeld probeer, wat in 2 transaksies opgelos word.
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
}
Aangesien dit die heel eerste weergawe is, is die sintaksis baie beperk en kan daar foute wees.
In die volgende artikels beplan ek om die verdere ontwikkeling van die VM te dek, en te wys hoe jy formeel geverifieerde slim kontrakte daarmee kan skep, en nie net dit kan oplos nie.
Die karakter virtuele masjien is beskikbaar by
Nadat ek die bronkode van die karakter VM in orde gebring het en opmerkings daar gevoeg het, beplan ek om dit op github in gratis toegang te plaas.
Bron: will.com