Rasmiy tekshirish - bu bir dastur yoki algoritmni boshqasidan foydalangan holda tekshirish.
Bu dasturdagi barcha zaifliklarni topish yoki ularning mavjud emasligini isbotlash imkonini beruvchi eng kuchli usullardan biridir.
Rasmiy tekshirishning batafsil tavsifini muammoni hal qilish misolida ko'rish mumkin oldingi maqolamda.
Ushbu maqolada men muammolarni rasmiy tekshirishdan dasturlarga o'taman va qanday qilishni tasvirlayman
qanday qilib ular avtomatik ravishda rasmiy qoidalar tizimiga aylantirilishi mumkin.
Buning uchun men ramziy printsiplardan foydalangan holda virtual mashinaning o'z analogini yozdim.
U dastur kodini tahlil qiladi va uni allaqachon dasturiy tarzda echilishi mumkin bo'lgan tenglamalar tizimiga (SMT) aylantiradi.
Ramziy hisob-kitoblar haqidagi ma'lumotlar Internetda qisman taqdim etilganligi sababli,
Men nima ekanligini qisqacha tasvirlab beraman.
Simvolik hisoblash dasturni bir vaqtning o'zida keng doiradagi ma'lumotlarda bajarish usuli bo'lib, dasturni rasmiy tekshirishning asosiy vositasi hisoblanadi.
Masalan, birinchi argument har qanday ijobiy qiymatlarni, ikkinchi salbiy, uchinchi nolni va chiqish argumentini, masalan, 42 ni olishi mumkin bo'lgan kirish shartlarini o'rnatishimiz mumkin.
Bitta yugurishdagi ramziy hisob-kitoblar bizga kerakli natijani olish mumkinmi yoki yo'qmi degan savolga javob beradi va bunday kirish parametrlari to'plamiga misol bo'ladi. Yoki bunday parametrlar yo'qligini isbotlash.
Bundan tashqari, biz kirish argumentlarini barcha mumkin bo'lganlarga o'rnatishimiz va faqat chiqish argumentlarini tanlashimiz mumkin, masalan, administrator paroli.
Bunday holda, biz dasturning barcha zaif tomonlarini topamiz yoki administrator paroli xavfsiz ekanligiga dalil olamiz.
Shuni ta'kidlash mumkinki, dasturning ma'lum bir kirish ma'lumotlari bilan klassik bajarilishi ramziy bajarishning alohida holatidir.
Shuning uchun, mening xarakterim VM standart virtual mashinaning emulyatsiya rejimida ham ishlashi mumkin.
Oldingi maqolaga berilgan sharhlarda rasmiy tekshirishning zaif tomonlarini muhokama qilish bilan adolatli tanqidni topish mumkin.
Asosiy muammolar quyidagilardan iborat:
- Kombinatoriy portlash, chunki rasmiy tekshirish oxir-oqibat P = NP ga tushadi
- Fayl tizimiga, tarmoqlarga va boshqa tashqi xotiraga qo'ng'iroqlarni qayta ishlashni tekshirish qiyinroq
- Spetsifikatsiyadagi xatolar, mijoz yoki dasturchi bitta narsani nazarda tutgan bo'lsa-da, lekin uni texnik spetsifikatsiyada etarlicha aniq tasvirlamagan.
Natijada, dastur tekshiriladi va spetsifikatsiyaga mos keladi, lekin yaratuvchilar undan kutganidan butunlay boshqacha ishni bajaradi.
Ushbu maqolada men asosan rasmiy tekshirishdan amalda foydalanishni ko'rib chiqayotganim sababli, men hozircha boshimni devorga urmayman va algoritmik murakkablik va tashqi qo'ng'iroqlar soni minimal bo'lgan tizimni tanlayman.
Aqlli kontraktlar ushbu talablarga eng mos kelganligi sababli, tanlov Waves platformasidagi RIDE shartnomalariga to'g'ri keldi: ular Turing to'liq emas va ularning maksimal murakkabligi sun'iy ravishda cheklangan.
Ammo biz ularni faqat texnik tomondan ko'rib chiqamiz.
Har bir narsaga qo'shimcha ravishda, rasmiy tekshirish har qanday shartnomalar uchun ayniqsa talabga ega bo'ladi: shartnoma xatosini ishga tushirilgandan keyin tuzatish odatda mumkin emas.
Va bunday xatolarning narxi juda yuqori bo'lishi mumkin, chunki juda katta miqdordagi mablag'lar ko'pincha aqlli shartnomalarda saqlanadi.
Mening ramziy virtual mashinasim PHP va Python tillarida yozilgan va olingan SMT formulalarini hal qilish uchun Microsoft Research kompaniyasining Z3Prover dasturidan foydalanadi.
Uning asosida kuchli ko'p tranzaksiyali qidiruv mavjud
ko'p tranzaktsiyalarni talab qilsa ham, echimlar yoki zaifliklarni topishga imkon beradi.
Hatto , Ethereum zaifliklarini topish uchun eng kuchli ramziy ramkalardan biri, bu imkoniyatni faqat bir necha oy oldin qo'shgan.
Ammo shuni ta'kidlash kerakki, efir shartnomalari yanada murakkab va Turing to'liq.
PHP RIDE aqlli kontraktining manba kodini python skriptiga tarjima qiladi, unda dastur Z3 SMT-mos keladigan shartnoma holatlari va ularning o'tish shartlari tizimi sifatida taqdim etiladi:
Endi men ichkarida nima sodir bo'layotganini batafsilroq tasvirlab beraman.
Lekin birinchi navbatda, RIDE aqlli kontrakt tili haqida bir necha so'z.
Bu funktsional va ifodaga asoslangan dasturlash tili bo'lib, dizayn jihatidan dangasa.
RIDE blokcheyn ichida alohida ishlaydi va foydalanuvchi hamyoniga bog‘langan xotiradan ma’lumotlarni olishi va yozishi mumkin.
Siz har bir hamyonga RIDE shartnomasini biriktirishingiz mumkin va bajarilish natijasi faqat TRUE yoki FALSE bo'ladi.
TRUE, aqlli shartnoma tranzaktsiyaga ruxsat berishini anglatadi va FALSE buni taqiqlaydi.
Oddiy misol: agar hamyon balansi 100 dan kam bo'lsa, skript pul o'tkazishni taqiqlashi mumkin.
Misol tariqasida, men bir xil bo'ri, echki va karamni olaman, lekin allaqachon aqlli shartnoma shaklida taqdim etilgan.
Foydalanuvchi hammani boshqa tomonga yubormaguncha, shartnoma o'rnatilgan hamyondan pul yechib ololmaydi.
#Извлекаем положение всех объектов из блокчейна
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 birinchi navbatda aqlli shartnomadan barcha o'zgaruvchilarni kalitlari va tegishli mantiqiy ifoda o'zgaruvchisi ko'rinishida chiqaradi.
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
Keyin PHP ularni Pythonda Z3Prover SMT-mos keladigan tizim tavsifiga aylantiradi.
Ma'lumotlar halqa ichiga o'ralgan bo'lib, unda saqlash o'zgaruvchilari indeks i, tranzaksiya o'zgaruvchilari indeksi i + 1 va ifodali o'zgaruvchilar oldingi holatdan keyingi holatga o'tish qoidalarini o'rnatadi.
Bu ko'p tranzaksiyali qidiruv tizimini ta'minlaydigan virtual mashinamizning qalbidir.
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] )
Shartlar tartiblangan va Python'da SMT tizimini tavsiflash uchun mo'ljallangan skript shabloniga kiritilgan.
Bo'sh shablon
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()
Butun zanjirdagi oxirgi holat uchun transfer operatsiyasi bo'limida ko'rsatilgan qoidalar qo'llaniladi.
Bu shuni anglatadiki, Z3Prover shartnomadan pul mablag'larini olib qo'yishga imkon beradigan aniq shartlar to'plamini qidiradi.
Natijada, biz avtomatik ravishda shartnomamizning to'liq ishlaydigan SMT modelini olamiz.
Bu mening oldingi maqolamdagi modelga juda o'xshashligini ko'rishingiz mumkin, uni men qo'lda tuzganman.
Tugallangan shablon
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()
Ishga tushgandan so'ng, Z3Prover aqlli shartnomani hal qiladi va bizga pul mablag'larini olib qo'yish imkonini beradigan tranzaktsiyalar zanjirini taqdim etadi:
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
Parom shartnomasiga qo'shimcha ravishda siz o'zingizning shartnomalaringiz bilan tajriba qilishingiz yoki 2 ta tranzaktsiyada hal qilinadigan ushbu oddiy misolni sinab ko'rishingiz mumkin.
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
}
Bu birinchi versiya bo'lgani uchun sintaksis juda cheklangan va xatolar bo'lishi mumkin.
Keyingi maqolalarda men VM ning keyingi rivojlanishini yoritishni va uning yordami bilan qanday qilib rasmiy tasdiqlangan aqlli kontraktlarni yaratishingiz mumkinligini va ularni nafaqat hal qilishni ko'rsatmoqchiman.
Belgilar virtual mashinasi mavjud
Ramziy VM ning manba kodini tartibga solib, u erda sharhlar qo'shgandan so'ng, men uni GitHub-ga bepul kirish uchun joylashtirishni rejalashtirmoqdaman.
Manba: www.habr.com