Албан ёсны баталгаажуулалт гэдэг нь нэг програм эсвэл алгоритмыг нөгөөг ашиглан шалгах явдал юм.
Энэ бол програмын бүх сул талыг олох эсвэл байхгүй гэдгийг батлах хамгийн хүчирхэг аргуудын нэг юм.
Албан ёсны баталгаажуулалтын илүү нарийвчилсан тайлбарыг асуудлыг шийдвэрлэх жишээнээс харж болно миний өмнөх нийтлэлд.
Энэ нийтлэлд би асуудлын албан ёсны баталгаажуулалтаас программ руу шилжиж, хэрхэн хийхийг тайлбарлах болно
тэдгээрийг хэрхэн автоматаар албан ёсны дүрмийн систем болгон хувиргах вэ.
Үүнийг хийхийн тулд би симболын зарчмуудыг ашиглан виртуал машины аналогийг бичсэн.
Энэ нь програмын кодыг задлан шинжилж, тэгшитгэлийн систем (SMT) болгон хөрвүүлдэг бөгөөд үүнийг аль хэдийн програмын аргаар шийдэж болно.
Бэлгэдлийн тооцооллын талаархи мэдээллийг интернетэд хэсэгчилсэн байдлаар танилцуулсан тул
Энэ нь юу болохыг би товчхон тайлбарлах болно.
Симболын тооцоолол нь программыг өргөн хүрээний өгөгдөл дээр нэгэн зэрэг гүйцэтгэх арга бөгөөд программыг албан ёсоор баталгаажуулах гол хэрэгсэл юм.
Жишээлбэл, бид эхний аргумент нь эерэг утгыг, хоёр дахь нь сөрөг, гурав дахь тэг, гаралтын аргумент, жишээлбэл, 42 байж болох оролтын нөхцлийг тохируулж болно.
Нэг удаагийн гүйлтийн симболын тооцоолол нь хүссэн үр дүнд хүрэх боломжтой эсэх, ийм оролтын параметрүүдийн жишээг бидэнд өгөх болно. Эсвэл ийм параметр байхгүй гэсэн нотолгоо.
Нэмж дурдахад бид оролтын аргументуудыг бүх боломжит аргументуудад тохируулж, зөвхөн гаралтын аргументуудыг сонгох боломжтой, жишээлбэл, администраторын нууц үг.
Энэ тохиолдолд бид програмын бүх сул талыг олох эсвэл администраторын нууц үг аюулгүй гэдгийг нотлох болно.
Тодорхой оролтын өгөгдөл бүхий програмын сонгодог гүйцэтгэл нь бэлгэдлийн гүйцэтгэлийн онцгой тохиолдол гэдгийг тэмдэглэж болно.
Тиймээс миний дүрийн VM нь стандарт виртуал машины эмуляцийн горимд ажиллах боломжтой.
Өмнөх нийтлэлийн тайлбараас албан ёсны баталгаажуулалтын талаар шударга шүүмжлэл, сул талуудын талаар ярилцаж болно.
Гол бэрхшээлүүд нь:
- Албан ёсны баталгаажуулалт нь эцсийн дүндээ P=NP болж ирдэг тул хослолын тэсрэлт
- Файлын систем, сүлжээ болон бусад гадаад санах ойн дуудлагыг боловсруулах нь шалгахад илүү хэцүү байдаг
- Захиалагч эсвэл программист нэг зүйлийг зорьсон боловч техникийн тодорхойлолтод хангалттай нарийвчлалтай тайлбарлаагүй тохиолдолд техникийн тодорхойлолтод гарсан алдаа.
Үүний үр дүнд програмыг шалгаж, техникийн шаардлагад нийцүүлэх боловч бүтээгчдийн хүлээж байснаас тэс өөр зүйлийг хийх болно.
Энэ нийтлэлд би албан ёсны баталгаажуулалтыг практикт ашиглах талаар голчлон авч үзэж байгаа тул би одоохондоо толгойгоо хана руу цохихгүй бөгөөд алгоритмын нарийн төвөгтэй байдал, гадаад дуудлагын тоо хамгийн бага байх системийг сонгох болно.
Ухаалаг гэрээнүүд нь эдгээр шаардлагад хамгийн сайн нийцдэг тул сонголт нь Waves платформын RIDE гэрээн дээр унасан: тэдгээр нь Тюринг бүрэн биш бөгөөд хамгийн нарийн төвөгтэй байдал нь зохиомлоор хязгаарлагддаг.
Гэхдээ бид тэдгээрийг зөвхөн техникийн талаас нь авч үзэх болно.
Бүх зүйлээс гадна албан ёсны баталгаажуулалт нь аливаа гэрээнд эрэлт хэрэгцээтэй байх болно: гэрээний алдааг эхлүүлсний дараа засах боломжгүй байдаг.
Ухаалаг гэрээнд нэлээд их хэмжээний хөрөнгө хадгалагддаг тул ийм алдааны өртөг маш өндөр байж болно.
Миний бэлгэдлийн виртуал машин нь PHP болон Python хэл дээр бичигдсэн бөгөөд Microsoft Research-ийн Z3Prover программыг ашиглан SMT томъёог шийддэг.
Үүний гол цөм нь хүчирхэг олон гүйлгээний хайлт юм
Энэ нь олон гүйлгээ хийх шаардлагатай байсан ч шийдэл эсвэл сул талыг олох боломжийг танд олгоно.
Тэр ч байтугай , Ethereum-ийн эмзэг байдлыг олох хамгийн хүчирхэг бэлгэдлийн хүрээнүүдийн нэг нь хэдхэн сарын өмнө энэ боломжийг нэмсэн.
Гэхдээ эфирийн гэрээ нь илүү төвөгтэй бөгөөд Тюринг бүрэн гүйцэд гэдгийг тэмдэглэх нь зүйтэй.
PHP нь RIDE ухаалаг гэрээний эх кодыг python скрипт болгон хөрвүүлдэг бөгөөд уг программыг Z3 SMT-тэй нийцтэй гэрээний төлөв, тэдгээрийн шилжилтийн нөхцлүүдийн систем болгон танилцуулдаг.
Одоо би дотор нь юу болж байгааг илүү дэлгэрэнгүй тайлбарлах болно.
Гэхдээ эхлээд RIDE ухаалаг гэрээний хэлний талаар хэдэн үг хэлье.
Энэ бол функциональ, илэрхийлэлд суурилсан програмчлалын хэл бөгөөд дизайны хувьд залхуу юм.
RIDE нь блокчейн дотор тусгаарлагдмал байдлаар ажилладаг бөгөөд хэрэглэгчийн түрийвчтэй холбогдсон сангаас мэдээлэл авч, бичих боломжтой.
Та түрийвч бүрт RIDE гэрээг хавсаргаж болох бөгөөд гүйцэтгэлийн үр дүн нь зөвхөн ҮНЭН эсвэл ХУДАЛ байх болно.
ҮНЭН гэдэг нь ухаалаг гэрээ нь гүйлгээ хийхийг зөвшөөрдөг, ХУДАЛ гэдэг нь үүнийг хориглодог гэсэн үг юм.
Энгийн жишээ: хэрэв түрийвчний үлдэгдэл 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