Формальды верификация – бір бағдарламаны немесе алгоритмді екіншісін қолдану арқылы тексеру.
Бұл бағдарламадағы барлық осалдықтарды табуға немесе олардың жоқтығын дәлелдеуге мүмкіндік беретін ең қуатты әдістердің бірі.
Ресми тексерудің толығырақ сипаттамасын мәселені шешу мысалында көруге болады алдыңғы мақаламда.
Бұл мақалада мен проблемаларды формальды тексеруден бағдарламаларға көшемін және оны қалай сипаттаймын
оларды қалай автоматты түрде ресми ережелер жүйесіне айналдыруға болады.
Ол үшін символдық принциптерді қолдана отырып, виртуалды машинаның өз аналогын жаздым.
Ол бағдарлама кодын талдайды және оны программалық түрде шешуге болатын теңдеулер жүйесіне (SMT) аударады.
Символдық есептеулер туралы ақпарат Интернетте бөлшектеп берілгендіктен,
Мен оның не екенін қысқаша сипаттаймын.
Символдық есептеу – кең ауқымды деректерде бағдарламаны бір уақытта орындау тәсілі және бағдарламаны формальды тексерудің негізгі құралы болып табылады.
Мысалы, бірінші аргумент кез келген оң мәндерді, екінші теріс, үшінші нөлді және шығыс аргументін қабылдай алатын енгізу шарттарын орната аламыз, мысалы, 42.
Бір жүгірістегі символдық есептеулер бізге қажетті нәтижені алу мүмкін бе деген сұраққа жауап береді және осындай енгізу параметрлері жиынтығының мысалын береді. Немесе мұндай параметрлердің жоқтығының дәлелі.
Сонымен қатар, біз кіріс аргументтерін барлық мүмкін болатындарға орнатып, тек шығыстарды таңдай аламыз, мысалы, әкімші құпия сөзі.
Бұл жағдайда біз бағдарламаның барлық осалдықтарын табамыз немесе әкімші құпия сөзі қауіпсіз екенін дәлелдейтін боламыз.
Белгілі бір кіріс деректері бар программаның классикалық орындалуы символдық орындаудың ерекше жағдайы болып табылатынын атап өтуге болады.
Сондықтан менің кейіпкерім VM стандартты виртуалды машинаның эмуляция режимінде де жұмыс істей алады.
Алдыңғы мақалаға түсініктемелерде оның әлсіз жақтарын талқылай отырып, ресми тексеруді әділ сынға алуға болады.
Негізгі проблемалар:
- Комбинаторлық жарылыс, өйткені формальды тексеру ақыр соңында P = NP дейін түседі
- Файлдық жүйеге, желілерге және басқа сыртқы жадқа қоңырауларды өңдеуді тексеру қиынырақ
- Тұтынушы немесе бағдарламашы бір нәрсені көздеген, бірақ оны техникалық сипаттамада жеткілікті түрде дәл сипаттамаған кездегі спецификациядағы қателер.
Нәтижесінде бағдарлама тексеріледі және спецификацияға сәйкес келеді, бірақ жасаушылар одан күткеннен мүлдем басқа нәрсе жасайды.
Бұл мақалада мен негізінен ресми тексеруді тәжірибеде қолдануды қарастырып жатқандықтан, мен әзірге басымды қабырғаға соқпаймын және алгоритмдік күрделілік пен сыртқы қоңыраулар саны аз болатын жүйені таңдаймын.
Ақылды келісім-шарттар осы талаптарға ең жақсы сәйкес келетіндіктен, таңдау Waves платформасындағы RIDE келісім-шарттарына түсті: олар Turing толық емес және олардың максималды күрделілігі жасанды түрде шектелген.
Бірақ біз оларды тек техникалық жағынан қарастырамыз.
Барлығына қоса, ресми тексеру әсіресе кез келген келісім-шарттар үшін сұранысқа ие болады: әдетте келісімшарт қатесін іске қосқаннан кейін түзету мүмкін емес.
Мұндай қателердің құны өте жоғары болуы мүмкін, өйткені өте үлкен көлемдегі қаражат көбінесе смарт келісімшарттарда сақталады.
Менің символдық виртуалды машинам PHP және Python тілдерінде жазылған және алынған SMT формулаларын шешу үшін Microsoft Research компаниясының Z3Prover бағдарламасын пайдаланады.
Оның негізінде қуатты көп транзакциялық іздеу жатыр, ол
көптеген транзакцияларды қажет етсе де, шешімдерді немесе осалдықтарды табуға мүмкіндік береді.
Тіпті , Ethereum осалдықтарын табуға арналған ең қуатты символдық құрылымдардың бірі бұл мүмкіндікті бірнеше ай бұрын ғана қосты.
Бірақ айта кету керек, эфирлік келісімшарттар күрделірек және Тьюринг толық.
PHP RIDE смарт келісім-шартының бастапқы кодын питон сценарийіне аударады, онда бағдарлама келісім-шарт күйлерінің және олардың ауысу шарттарының Z3 SMT-үйлесімді жүйесі ретінде ұсынылған:
Енді мен іште не болып жатқанын толығырақ сипаттаймын.
Бірақ алдымен RIDE смарт келісімшарт тілі туралы бірнеше сөз.
Бұл дизайн бойынша жалқау функционалды және өрнекке негізделген бағдарламалау тілі.
RIDE блокчейн ішінде оқшау жұмыс істейді және пайдаланушының әмиянына байланысты қоймадан ақпаратты шығарып, жаза алады.
Әрбір әмиянға RIDE келісімшартын тіркей аласыз және орындалу нәтижесі тек ШЫН немесе ЖАЛҒАН болады.
TRUE смарт келісім-шарттың транзакцияға рұқсат беретінін, ал ЖАЛҒАН оған тыйым салатынын білдіреді.
Қарапайым мысал: әмияндағы теңгерім 100-ден аз болса, сценарий аударуға тыйым сала алады.
Мысал ретінде мен бірдей Қасқырды, Ешкі мен Қырыққабатты аламын, бірақ қазірдің өзінде ақылды келісімшарт түрінде ұсынылған.
Пайдаланушы барлығын басқа тарапқа жібермейінше, келісімшарт орналастырылған әмияннан ақшаны ала алмайды.
#Извлекаем положение всех объектов из блокчейна
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 алдымен смарт келісім-шарттан барлық айнымалы мәндерді олардың кілттері және сәйкес логикалық өрнек айнымалысы түрінде шығарады.
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 оларды Python тіліндегі Z3Prover SMT-үйлесімді жүйе сипаттамасына түрлендіреді.
Деректер циклге оралады, мұнда сақтау айнымалылары i индексін алады, транзакцияның айнымалылары индексі i + 1 және өрнектері бар айнымалылар алдыңғы күйден келесіге өту ережелерін орнатады.
Бұл көп транзакциялық іздеу жүйесін қамтамасыз ететін виртуалды машинамыздың жүрегі.
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] )
Шарттар сұрыпталған және Python тіліндегі SMT жүйесін сипаттауға арналған сценарий үлгісіне енгізілген.
Бос үлгі
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()
Бүкіл тізбектегі соңғы күй үшін аударым транзакциясы бөлімінде көрсетілген ережелер қолданылады.
Бұл Z3Prover келісім-шарттан ақшаны алып тастауға мүмкіндік беретін нақты шарттар жиынтығын іздейтінін білдіреді.
Нәтижесінде біз автоматты түрде келісім-шартымыздың толық функционалды SMT үлгісін аламыз.
Қолмен құрастырған алдыңғы мақаламдағы үлгіге өте ұқсас екенін көруге болады.
Аяқталған үлгі
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()
Іске қосылғаннан кейін Z3Prover ақылды келісім-шартты шешеді және бізге қаражатты алуға мүмкіндік беретін транзакциялар тізбегін ұсынады:
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
Паромдық келісімшартқа қосымша, сіз өзіңіздің келісімшарттарыңызбен тәжірибе жасай аласыз немесе 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
}
Бұл ең бірінші нұсқа болғандықтан, синтаксис өте шектеулі және қателер болуы мүмкін.
Келесі мақалаларда мен VM-нің одан әрі дамуын қарастыруды жоспарлап отырмын және оның көмегімен ресми түрде тексерілген смарт-келісімшарттарды қалай жасауға болатындығын көрсетуді және оларды жай ғана шешпейді.
Таңбаның виртуалды машинасы мына жерден қол жетімді
Символдық VM бастапқы кодын ретке келтіріп, сол жерге түсініктемелерді қосқаннан кейін мен оны GitHub сайтында тегін қол жеткізу үшін жариялауды жоспарлап отырмын.
Ақпарат көзі: www.habr.com