Il-verifika formali hija l-verifika ta' programm jew algoritmu li juża ieħor.
Dan huwa wieħed mill-aktar metodi b'saħħithom li jippermettilek issib il-vulnerabbiltajiet kollha fi programm jew tipprova li ma jeżistux.
Deskrizzjoni aktar dettaljata ta 'verifika formali tista' tidher fl-eżempju ta 'soluzzjoni tal-problema ta' fl-artiklu preċedenti tiegħi.
F'dan l-artikolu ngħaddi minn verifika formali tal-problemi għal programmi u niddeskrivi kif
kif jistgħu jiġu konvertiti f'sistemi ta' regoli formali awtomatikament.
Biex tagħmel dan, ktibt l-analogu tiegħi stess ta 'magna virtwali, bl-użu ta' prinċipji simboliċi.
Teżamina l-kodiċi tal-programm u tittraduċih f'sistema ta 'ekwazzjonijiet (SMT), li diġà tista' tiġi solvuta b'mod programmatiku.
Peress li l-informazzjoni dwar il-kalkoli simboliċi hija ppreżentata fuq l-Internet b'mod pjuttost frammentarju,
Se niddeskrivi fil-qosor x'inhu.
Il-komputazzjoni simbolika hija mod biex tesegwixxi programm simultanjament fuq firxa wiesgħa ta 'dejta u hija l-għodda ewlenija għall-verifika formali tal-programm.
Pereżempju, nistgħu nissettjaw kundizzjonijiet ta 'input fejn l-ewwel argument jista' jieħu kwalunkwe valuri pożittivi, it-tieni negattiv, it-tielet żero, u l-argument tal-output, pereżempju, 42.
Kalkoli simboliċi f'ġirja waħda jagħtuna t-tweġiba dwar jekk huwiex possibbli għalina li niksbu r-riżultat mixtieq u eżempju ta 'sett ta' tali parametri ta 'input. Jew prova li m'hemmx tali parametri.
Barra minn hekk, nistgħu nissettjaw l-argumenti tal-input għal dawk kollha possibbli, u agħżel biss dawk tal-output, pereżempju, il-password tal-amministratur.
F'dan il-każ, insibu l-vulnerabbiltajiet kollha tal-programm jew niksbu prova li l-password tal-amministratur hija sigura.
Jista 'jiġi nnotat li l-eżekuzzjoni klassika ta' programm b'dejta ta 'input speċifika hija każ speċjali ta' eżekuzzjoni simbolika.
Għalhekk, il-karattru tiegħi VM jista 'wkoll jaħdem fil-mod ta' emulazzjoni ta 'magna virtwali standard.
Fil-kummenti għall-artiklu preċedenti wieħed jista’ jsib kritika ġusta tal-verifika formali b’diskussjoni dwar id-dgħufijiet tagħha.
Il-problemi ewlenin huma:
- Splużjoni kombinatorja, peress li l-verifika formali fl-aħħar tinżel għal P=NP
- L-ipproċessar ta 'sejħiet lis-sistema tal-fajls, netwerks u ħażna esterna oħra huwa aktar diffiċli biex jiġi vverifikat
- Bugs fl-ispeċifikazzjoni, meta l-klijent jew il-programmatur maħsub ħaġa waħda, iżda ma ddeskriviehiex b'mod preċiż biżżejjed fl-ispeċifikazzjoni teknika.
Bħala riżultat, il-programm se jiġi vverifikat u jikkonforma mal-ispeċifikazzjoni, iżda se jagħmel xi ħaġa kompletament differenti minn dak li l-ħallieqa stennew minnu.
Peress li f'dan l-artikolu qed nikkunsidra prinċipalment l-użu ta 'verifika formali fil-prattika, għalissa mhux se nibang rasi mal-ħajt, u se nagħżel sistema fejn il-kumplessità algoritmika u n-numru ta' sejħiet esterni huma minimi.
Peress li l-kuntratti intelliġenti jaqdu l-aħjar għal dawn ir-rekwiżiti, l-għażla waqgħet fuq kuntratti RIDE mill-pjattaforma Waves: mhumiex Turing kompluti, u l-kumplessità massima tagħhom hija limitata artifiċjalment.
Iżda aħna se nqisuhom esklussivament mil-lat tekniku.
Minbarra kollox, il-verifika formali se tkun speċjalment fid-domanda għal kwalunkwe kuntratt: normalment huwa impossibbli li jiġi kkoreġut żball ta 'kuntratt wara li jkun tnieda.
U l-ispiża ta 'żbalji bħal dawn tista' tkun għolja ħafna, peress li ammonti pjuttost kbar ta 'fondi ħafna drabi jinħażnu fuq kuntratti intelliġenti.
Il-magna virtwali simbolika tiegħi hija miktuba f'PHP u Python, u tuża Z3Prover minn Microsoft Research biex issolvi l-formuli SMT li jirriżultaw.
Fil-qalba tagħha hemm tfittxija multi-transazzjonali qawwija, li
jippermettilek issib soluzzjonijiet jew vulnerabbiltajiet, anke jekk teħtieġ ħafna transazzjonijiet.
Anke , wieħed mill-oqfsa simboliċi l-aktar qawwija biex jinstabu vulnerabbiltajiet Ethereum, żiedet biss din il-kapaċità ftit xhur ilu.
Iżda ta 'min jinnota li l-kuntratti ether huma aktar kumplessi u Turing komplut.
PHP jittraduċi l-kodiċi tas-sors tal-kuntratt intelliġenti RIDE fi script python, li fih il-programm huwa ppreżentat bħala sistema kompatibbli ma 'Z3 SMT ta' stati kuntrattwali u kundizzjonijiet għat-tranżizzjonijiet tagħhom:
Issa ser niddeskrivi dak li qed jiġri ġewwa f'aktar dettall.
Imma l-ewwel, ftit kelmiet dwar il-lingwa tal-kuntratt intelliġenti RIDE.
Hija lingwa ta 'programmar funzjonali u bbażata fuq l-espressjoni li hija għażżien mid-disinn.
RIDE jaħdem b'mod iżolat fi ħdan il-blockchain u jista' jirkupra u jikteb informazzjoni mill-ħażna marbuta mal-kartiera tal-utent.
Tista' tehmeż kuntratt RIDE ma' kull kartiera, u r-riżultat tal-eżekuzzjoni jkun VERU jew FALZ biss.
VERU ifisser li l-kuntratt intelliġenti jippermetti t-tranżazzjoni, u FALZ ifisser li jipprojbixxiha.
Eżempju sempliċi: skript jista’ jipprojbixxi trasferiment jekk il-bilanċ tal-kartiera huwa inqas minn 100.
Bħala eżempju, se nieħu l-istess Lupu, Mogħoż, u Kaboċċi, iżda diġà ppreżentati fil-forma ta 'kuntratt intelliġenti.
L-utent mhux se jkun jista 'jiġbed il-flus mill-kartiera li fuqha huwa skjerat il-kuntratt sakemm ikun bagħat lil kulħadd fuq in-naħa l-oħra.
#Извлекаем положение всех объектов из блокчейна
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 l-ewwel estratti l-varjabbli kollha mill-kuntratt intelliġenti fil-forma taċ-ċwievet tagħhom u l-varjabbli tal-espressjoni Boolean korrispondenti.
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 mbagħad jikkonvertihom f'deskrizzjoni ta 'sistema kompatibbli ma' Z3Prover SMT f'Python.
Id-dejta hija mgeżwra f'linja, fejn il-varjabbli tal-ħażna jirċievu indiċi i, il-varjabbli tat-tranżazzjoni indiċi i + 1, u l-varjabbli b'espressjonijiet jistabbilixxu r-regoli għat-tranżizzjoni mill-istat preċedenti għall-ieħor.
Din hija l-qalba stess tal-magna virtwali tagħna, li tipprovdi mekkaniżmu ta 'tfittxija multi-transazzjonali.
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] )
Il-kundizzjonijiet huma magħżula u mdaħħla f'mudell ta 'skript iddisinjat biex jiddeskrivi s-sistema SMT f'Python.
Mudell vojt
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()
Għall-aħħar stat fil-katina kollha, ir-regoli li huma speċifikati fit-taqsima tat-tranżazzjoni tat-trasferiment huma applikati.
Dan ifisser li Z3Prover se jfittex preċiżament dawn is-settijiet ta 'kundizzjonijiet li fl-aħħar mill-aħħar jippermettu li l-fondi jiġu rtirati mill-kuntratt.
Bħala riżultat, aħna nirċievu awtomatikament mudell SMT kompletament funzjonali tal-kuntratt tagħna.
Tista 'tara li huwa simili ħafna għall-mudell mill-artiklu preċedenti tiegħi, li kkumpilajt manwalment.
Mudell komplut
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()
Wara t-tnedija, Z3Prover issolvi l-kuntratt intelliġenti u jipprovdilna katina ta 'tranżazzjonijiet li tippermettilna nirtiraw il-fondi:
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
Minbarra l-kuntratt tal-laneċ, tista 'tesperimenta bil-kuntratti tiegħek stess jew tipprova dan l-eżempju sempliċi, li huwa solvut fi tranżazzjonijiet 2.
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
}
Peress li din hija l-ewwel verżjoni, is-sintassi hija limitata ħafna u jista 'jkun hemm bugs.
Fl-artikoli li ġejjin, qed nippjana li nkopri l-iżvilupp ulterjuri tal-VM, u nuri kif tista 'toħloq kuntratti intelliġenti verifikati formalment bl-għajnuna tagħha, u mhux biss issolvihom.
Il-magna virtwali tal-karattru hija disponibbli fuq
Wara li tpoġġi l-kodiċi tas-sors tal-VM simbolika fl-ordni u żżid kummenti hemmhekk, nippjana li npoġġih fuq GitHub għal aċċess b'xejn.
Sors: www.habr.com