Formleg sannprófun er sannprófun á einu forriti eða reiknirit með því að nota annað.
Þetta er ein öflugasta aðferðin sem gerir þér kleift að finna alla veikleika í forriti eða sanna að þeir séu ekki til.
Nánari lýsingu á formlegri sannprófun má sjá í dæminu um að leysa vandamálið í fyrri grein minni.
Í þessari grein fer ég frá formlegri sannprófun á vandamálum yfir í forrit og lýsi því hvernig
hvernig er hægt að breyta þeim í formleg reglukerfi sjálfkrafa.
Til að gera þetta skrifaði ég mína eigin hliðstæðu af sýndarvél með táknrænum meginreglum.
Það greinir forritskóðann og þýðir það yfir í jöfnukerfi (SMT), sem nú þegar er hægt að leysa forritlega.
Þar sem upplýsingar um táknræna útreikninga eru settar fram á netinu frekar brotakenndar,
Ég mun lýsa stuttlega hvað það er.
Táknræn útreikningur er leið til að keyra forrit samtímis á fjölmörgum gögnum og er aðal tólið til formlegrar sannprófunar á forritum.
Til dæmis getum við stillt inntaksskilyrði þar sem fyrstu röksemdin getur tekið hvaða jákvæð gildi sem er, önnur neikvæð, sú þriðja núll og úttaksröksemdin, til dæmis 42.
Táknrænir útreikningar í einni keyrslu munu gefa okkur svar við því hvort það sé mögulegt fyrir okkur að fá þá niðurstöðu sem óskað er eftir og dæmi um safn slíkra inntaksbreyta. Eða sönnun þess að það eru engar slíkar breytur.
Þar að auki getum við stillt inntaksrökurnar á allar mögulegar og aðeins valið úttaksrökurnar, til dæmis lykilorð stjórnanda.
Í þessu tilviki munum við finna alla veikleika forritsins eða fá sönnun fyrir því að lykilorð stjórnandans sé öruggt.
Það má taka fram að klassísk framkvæmd forrits með sérstökum inntaksgögnum er sérstakt tilvik um táknræna framkvæmd.
Þess vegna getur karakterinn minn VM líka virkað í líki af venjulegri sýndarvél.
Í athugasemdum við fyrri grein má finna sanngjarna gagnrýni á formlega sannprófun með umfjöllun um veikleika hennar.
Helstu vandamálin eru:
- Samsett sprenging, þar sem formleg sannprófun kemur að lokum niður á P=NP
- Það er erfiðara að sannreyna símtöl í skráarkerfið, netkerfi og aðra ytri geymslu
- Villur í forskriftinni, þegar viðskiptavinurinn eða forritarinn ætlaði sér eitt, en lýsti því ekki nógu nákvæmlega í tækniforskriftinni.
Fyrir vikið verður forritið staðfest og uppfyllir forskriftina, en mun gera eitthvað allt annað en höfundarnir bjuggust við af því.
Þar sem ég í þessari grein er aðallega að íhuga notkun formlegrar sannprófunar í reynd mun ég ekki berja hausnum við vegg í bili, og mun velja kerfi þar sem reikniritflókið og fjöldi ytri símtala er í lágmarki.
Þar sem snjallsamningar henta best þessum kröfum, féll valið á RIDE samninga frá Waves pallinum: þeir eru ekki Turing fullkomnir og hámarksflækjustig þeirra er tilbúnar takmarkað.
En við munum íhuga þá eingöngu frá tæknilegu hliðinni.
Til viðbótar við allt verður formleg sannprófun sérstaklega eftirsótt fyrir hvaða samninga sem er: það er venjulega ómögulegt að leiðrétta samningsvillu eftir að hún hefur verið hleypt af stokkunum.
Og kostnaður við slíkar villur getur verið mjög hár, þar sem ansi stórar fjárhæðir eru oft geymdar á snjöllum samningum.
Táknræn sýndarvélin mín er skrifuð í PHP og Python og notar Z3Prover frá Microsoft Research til að leysa SMT formúlurnar sem myndast.
Í kjarna þess er öflug fjölviðskiptaleit, sem
gerir þér kleift að finna lausnir eða veikleika, jafnvel þótt það krefjist margra viðskipta.
Jafnvel , einn af öflugustu táknrænu rammanum til að finna Ethereum veikleika, bætti aðeins við þessari getu fyrir nokkrum mánuðum síðan.
En það er athyglisvert að etersamningar eru flóknari og Turing heill.
PHP þýðir frumkóðann RIDE snjallsamningsins yfir í python handrit, þar sem forritið er kynnt sem Z3 SMT-samhæft kerfi samningsríkja og skilyrði fyrir umskipti þeirra:
Nú mun ég lýsa nánar hvað er að gerast inni.
En fyrst, nokkur orð um RIDE snjallsamningamálið.
Það er hagnýtt forritunarmál sem byggir á tjáningu sem er letilegt að hönnun.
RIDE keyrir í einangrun innan blockchain og getur sótt og skrifað upplýsingar úr geymslu sem tengist veski notandans.
Þú getur hengt RIDE samning við hvert veski og niðurstaðan af framkvæmd verður aðeins SÖNN eða FALSK.
TRUE þýðir að snjallsamningurinn leyfir viðskiptin og FALSE þýðir að hann bannar þau.
Einfalt dæmi: handrit getur bannað millifærslu ef inneign veskis er minni en 100.
Sem dæmi mun ég taka sama úlf, geit og hvítkál, en þegar kynnt í formi snjölls samnings.
Notandinn mun ekki geta tekið peninga úr veskinu sem samningurinn er settur á fyrr en hann hefur sent alla á hina hliðina.
#Извлекаем положение всех объектов из блокчейна
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 dregur fyrst allar breyturnar úr snjallsamningnum í formi lykla þeirra og samsvarandi Boolean tjáningarbreytu.
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 breytir þeim síðan í Z3Prover SMT-samhæfða kerfislýsingu í Python.
Gögnunum er pakkað inn í lykkju þar sem geymslubreytur fá vísitölu i, viðskiptabreytur vísitölu i + 1 og breytur með tjáningu setja reglur um umskipti frá fyrra ástandi í það næsta.
Þetta er hjarta sýndarvélarinnar okkar, sem býður upp á leitarvél með mörgum viðskiptum.
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] )
Skilyrðin eru flokkuð og sett inn í forskriftarsniðmát sem er hannað til að lýsa SMT kerfinu í Python.
Autt sniðmát
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()
Fyrir síðasta ríkið í allri keðjunni er beitt reglum sem tilgreindar eru í kaflanum um millifærslufærslur.
Þetta þýðir að Z3Prover mun leita að nákvæmlega slíkum skilyrðum sem mun að lokum gera kleift að taka fé út úr samningnum.
Fyrir vikið fáum við sjálfkrafa fullvirkt SMT líkan af samningi okkar.
Þú getur séð að það er mjög svipað líkaninu frá fyrri grein minni, sem ég tók saman handvirkt.
Útfyllt sniðmát
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()
Eftir kynningu leysir Z3Prover snjallsamninginn og veitir okkur viðskiptakeðju sem gerir okkur kleift að taka út fjármuni:
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
Til viðbótar við ferjusamninginn geturðu gert tilraunir með þína eigin samninga eða prófað þetta einfalda dæmi sem er leyst í 2 viðskiptum.
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
}
Þar sem þetta er allra fyrsta útgáfan er setningafræði mjög takmörkuð og það geta verið villur.
Í eftirfarandi greinum ætla ég að fjalla um frekari þróun VM, og sýna hvernig þú getur búið til formlega staðfesta snjalla samninga með hjálp þess, en ekki bara leyst þá.
Karakter sýndarvélin er fáanleg á
Eftir að hafa komið frumkóða hins táknræna VM í röð og bætt við athugasemdum þar, ætla ég að setja hann á GitHub fyrir ókeypis aðgang.
Heimild: www.habr.com