Ang pormal nga pag-verify mao ang pag-verify sa usa ka programa o algorithm sa tabang sa lain.
Kini usa sa labing kusgan nga mga pamaagi nga nagtugot kanimo nga makit-an ang tanan nga mga kahuyangan sa programa o pamatud-an nga wala kini.
Ang usa ka mas detalyado nga paghulagway sa pormal nga verification makita sa panig-ingnan sa pagsulbad sa problema sa sa akong miaging artikulo.
Niini nga artikulo, mibalhin ko gikan sa pormal nga pag-verify sa problema ngadto sa mga programa ug ihulagway kung giunsa
kung giunsa nimo kini mahimo nga mga sistema sa pormal nga mga lagda awtomatiko.
Aron mahimo kini, gisulat nako ang akong analogue sa usa ka virtual nga makina, sa simbolikong mga prinsipyo.
Gi-parse niini ang program code ug gihubad kini ngadto sa usa ka system of equation (SMT), nga masulbad na pinaagi sa programa.
Tungod kay ang impormasyon bahin sa simbolikong mga kalkulasyon gipresentar sa Internet nga medyo tipik,
Ako sa mubo nga paghulagway kon unsa kini.
Ang simbolikong mga kalkulasyon usa ka paagi sa dungan nga pagpatuman sa usa ka programa sa usa ka halapad nga mga datos ug mao ang nag-unang himan alang sa pormal nga pag-verify sa programa.
Pananglitan, mahimo natong itakda ang mga kondisyon sa pag-input diin ang una nga argumento mahimong makakuha og bisan unsang positibo nga bili, ang ikaduha mahimong negatibo, ang ikatulo mahimong zero, ug ang output argumento, pananglitan, 42.
Ang simbolikong mga kalkulasyon sa usa ka run maghatag kanato ug tubag kon posible ba nga makuha nato ang gitinguhang resulta ug usa ka pananglitan sa usa ka set sa maong input parameters. O pamatuod nga walay ingon nga mga parameter.
Dugang pa, mahimo natong itakda ang input nga mga argumento sa kinatibuk-an kutob sa mahimo, ug pilion lamang ang output, pananglitan, ang password sa tagdumala.
Sa kini nga kaso, makit-an namon ang tanan nga mga kahuyangan sa programa, o makakuha kami pamatuod nga luwas ang password sa admin.
Makita nga ang klasikal nga pagpatuman sa usa ka programa nga adunay piho nga data sa pag-input usa ka espesyal nga kaso sa usa ka simbolo.
Busa, ang akong kinaiya nga VM mahimo usab nga magtrabaho sa emulation mode sa usa ka standard virtual machine.
Sa mga komento sa miaging artikulo, makit-an usab sa usa ang patas nga pagsaway sa pormal nga pag-verify nga adunay paghisgot sa mga kahuyang niini.
Ang mga nag-unang problema mao ang:
- Kombinatoryal nga pagbuto, tungod kay ang pormal nga pag-verify sa katapusan naa sa P = NP
- Ang pagdumala sa mga tawag sa file system, network, ug uban pang external storage mas lisud nga mapamatud-an
- Ang mga bug sa detalye, kung ang kostumer o programmer nakahunahuna usa ka butang, apan wala kini tukma nga gihulagway sa TOR.
Ingon usa ka sangputanan, ang programa mapamatud-an ug magsunod sa detalye, apan maghimo usa ka butang nga hingpit nga lahi sa gipaabut sa mga tiglalang gikan niini.
Tungod kay sa niini nga artikulo ako nag-una nga gikonsiderar ang paggamit sa pormal nga pag-verify sa praktis, dili ko mabunalan ang akong agtang batok sa bungbong sa pagkakaron, ug ako mopili sa usa ka sistema diin ang algorithmic complexity ug ang gidaghanon sa mga eksternal nga tawag gamay ra.
Tungod kay ang mga smart nga kontrata mohaum niini nga mga kinahanglanon sa pinakamaayo nga paagi, ang pagpili nahulog sa mga kontrata sa RIDE gikan sa Waves platform: dili sila Turing-kompleto, ug ang ilang pinakataas nga komplikado kay artipisyal nga limitado.
Apan atong tagdon sila nga eksklusibo gikan sa teknikal nga bahin.
Gawas pa sa tanan, alang sa bisan unsang mga kontrata, ang pormal nga pag-verify labi na nga gipangayo: ingon usa ka lagda, imposible nga matul-id ang usa ka sayup sa kontrata pagkahuman nga kini gilusad.
Ug ang presyo sa ingon nga mga sayup mahimo’g taas kaayo, tungod kay daghang mga pondo ang kanunay nga gitipigan sa mga smart nga kontrata.
Ang akong karakter nga VM gisulat sa PHP ug Python, ug naggamit sa Z3Prover sa Microsoft Research aron masulbad ang resulta nga mga pormula sa SMT.
Sa kinauyokan niini mao ang usa ka gamhanan nga multi-transaksyonal nga pagpangita, nga
nagtugot kanimo sa pagpangita sa mga solusyon o mga kahuyangan, bisan kung kini nanginahanglan daghang mga transaksyon.
Bisan ang , usa sa labing gamhanan nga mga gambalay sa karakter alang sa pagpangita sa mga kahuyangan sa Ethereum, gidugang lamang kini nga kapabilidad pipila ka bulan ang milabay.
Apan angay nga matikdan nga ang mga kontrata sa ether mas komplikado ug adunay Turing-completeness.
Gihubad sa PHP ang source code sa RIDE smart contract ngadto sa python script, diin ang programa gipresentar isip Z3 SMT-compatible nga sistema sa mga estado sa kontrata ug ang ilang mga kondisyon sa pagbalhin:
Karon akong ihulagway kung unsa ang nahitabo sa sulod, sa mas detalyado.
Apan una, pipila ka mga pulong mahitungod sa RIDE smart contract nga pinulongan.
Kini usa ka functional ug expression-based programming language nga tapolan sa disenyo.
Ang RIDE nagdagan nga nag-inusara sa sulod sa blockchain, ug mahimo’g makuha ug isulat ang kasayuran gikan sa pagtipig nga adunay kalabotan sa pitaka sa tiggamit.
Ang usa ka kontrata sa RIDE mahimong ilakip sa matag pitaka, ug ang resulta sa pagpatuman mahimong TINUOD o PAKIK.
TINUOD nagpasabot nga ang smart nga kontrata nagtugot sa transaksyon, ug FALSE nga kini nagdili niini.
Usa ka yano nga pananglitan: ang script mahimong magdili sa pagbalhin kung ang balanse sa pitaka dili moubos sa 100.
Ingon nga usa ka pananglitan, akong kuhaon ang parehas nga Lobo, Kanding, ug Cabbage, apan gipresentar na sa porma sa usa ka smart nga kontrata.
Ang tiggamit dili makahimo sa pag-withdraw sa salapi gikan sa pitaka diin ang kontrata gi-deploy hangtud nga iyang ipadala ang tanan ngadto sa pikas nga bahin.
#Извлекаем положение всех объектов из блокчейна
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
}
Una nga gikuha sa PHP ang tanan nga mga variable gikan sa smart contract sa porma sa ilang mga yawe ug ang katugbang nga boolean nga ekspresyon.
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
Gi-convert kini sa PHP ngadto sa Z3Prover SMT compatible python system description.
Ang datos giputos sa usa ka loop, diin ang mga variable sa pagtipig makadawat sa indeks i, ang mga variable sa transaksyon index i + 1, ug ang mga variable nga adunay mga ekspresyon nagtakda sa mga lagda alang sa pagbalhin gikan sa miaging estado ngadto sa sunod.
Mao kini ang kasingkasing sa atong virtual machine, nga naghatag og multi-transactional nga search engine.
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] )
Ang mga kondisyon gisunod ug gisulod sa usa ka script template nga gidisenyo aron ihulagway ang SMT system sa python.
Walay sulod nga template
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()
Alang sa katapusang estado sa tibuok kadena, ang mga lagda nga gitakda sa seksyon sa transaksyon sa pagbalhin gipadapat.
Kini nagpasabut nga ang Z3Prover mangita alang sa eksakto nga mga set sa estado nga sa katapusan magtugot kanimo sa pag-withdraw sa mga pondo gikan sa kontrata.
Ingon usa ka sangputanan, awtomatiko kaming makakuha usa ka hingpit nga magamit nga modelo sa SMT sa among kontrata.
Imong makita nga kini susama kaayo sa modelo gikan sa akong miaging artikulo, nga akong gihugpong pinaagi sa kamot.
Nakompleto nga Template
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()
Pagkahuman sa paglansad, gisulbad sa Z3Prover ang intelihente nga kontrata ug gipakita ang usa ka kutay sa mga transaksyon alang kanamo, nga magtugot kanamo sa pag-withdraw sa mga pondo:
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
Dugang pa sa kontrata sa pagtabok, mahimo ka mag-eksperimento sa imong kaugalingon nga mga kontrata o sulayan kining yano nga pananglitan, nga masulbad sa 2 nga mga transaksyon.
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
}
Tungod kay kini ang labing una nga bersyon, ang syntax limitado kaayo ug mahimong adunay mga bug.
Sa sunod nga mga artikulo, nagplano ako nga tabonan ang dugang nga pag-uswag sa VM, ug ipakita kung giunsa nimo paghimo ang pormal nga gipamatud-an nga mga smart nga mga kontrata uban niini, ug dili lamang pagsulbad niini.
Ang karakter nga virtual machine anaa sa
Human madala ang source code sa karakter nga VM sa han-ay ug pagdugang og mga komento didto, plano nako nga ibutang kini sa github sa libre nga pag-access.
Source: www.habr.com