Formal yoxlama bir proqramın və ya alqoritmin digərinin köməyi ilə yoxlanılmasıdır.
Bu, proqramdakı bütün zəiflikləri tapmağa və ya onların olmadığını sübut etməyə imkan verən ən güclü üsullardan biridir.
Formal yoxlamanın daha ətraflı təsvirini problemin həlli nümunəsində görmək olar əvvəlki məqaləmdə.
Bu yazıda mən problemin formal yoxlanışından proqramlara keçirəm və necə olduğunu təsvir edirəm
onları avtomatik olaraq formal qaydalar sisteminə necə çevirə bilərsiniz.
Bunun üçün mən virtual maşının analoqunu simvolik prinsiplər əsasında yazdım.
O, proqram kodunu təhlil edir və onu artıq proqramlı şəkildə həll edilə bilən tənliklər sisteminə (SMT) çevirir.
Simvolik hesablamalar haqqında məlumat İnternetdə kifayət qədər fraqmentli şəkildə təqdim olunduğundan,
Bunun nə olduğunu qısaca təsvir edəcəyəm.
Simvolik hesablamalar geniş məlumat diapazonunda eyni vaxtda proqramı icra etmək üsuludur və proqramın rəsmi yoxlanılması üçün əsas vasitədir.
Məsələn, birinci arqumentin hər hansı müsbət qiymət ala biləcəyi, ikincinin mənfi, üçüncüsü sıfır ola biləcəyi və çıxış arqumentinin, məsələn, 42 ola biləcəyi giriş şərtlərini təyin edə bilərik.
Bir qaçışda simvolik hesablamalar bizə istənilən nəticəni əldə etməyin mümkün olub-olmadığını və bu cür giriş parametrləri toplusunun nümunəsini verəcəkdir. Və ya belə parametrlərin olmadığı sübutu.
Üstəlik, giriş arqumentlərini ümumiyyətlə mümkün qədər təyin edə bilərik və yalnız çıxışı, məsələn, administrator parolunu seçə bilərik.
Bu halda biz proqramın bütün zəifliklərini tapacağıq və ya admin parolunun təhlükəsiz olduğuna dair sübut əldə edəcəyik.
Görünür ki, proqramın xüsusi giriş verilənləri ilə klassik icrası simvolik olanın xüsusi halıdır.
Buna görə də, mənim xarakterim VM standart virtual maşının emulyasiya rejimində də işləyə bilər.
Əvvəlki məqaləyə şərhlərdə, zəif tərəflərinin müzakirəsi ilə rəsmi yoxlamanın ədalətli tənqidinə də rast gəlmək olar.
Əsas problemlər bunlardır:
- Kombinator partlayışı, çünki formal yoxlama sonda P=NP üzərində dayanır
- Fayl sisteminə, şəbəkələrə və digər xarici yaddaşa edilən zəngləri yoxlamaq daha çətindir
- Müştəri və ya proqramçı bir şeyi düşünərkən, lakin onu TOR-da dəqiq təsvir etmədikdə spesifikasiyadakı səhvlər.
Nəticədə, proqram yoxlanılacaq və spesifikasiyaya uyğun olacaq, lakin yaradıcıların ondan gözlədiklərindən tamamilə fərqli bir şey edəcək.
Bu yazıda mən əsasən praktikada formal yoxlamanın tətbiqini nəzərdən keçirdiyim üçün hələlik alnımı divara vurmayacağam və alqoritmik mürəkkəbliyin və xarici zənglərin sayının minimal olduğu bir sistem seçəcəyəm.
Ağıllı müqavilələr bu tələblərə ən yaxşı şəkildə uyğun gəldiyi üçün seçim Waves platformasından olan RIDE müqavilələrinə düşdü: onlar Turing-tamamilə deyil və onların maksimum mürəkkəbliyi süni şəkildə məhdudlaşdırılıb.
Ancaq biz onları yalnız texniki tərəfdən nəzərdən keçirəcəyik.
Hər şeyə əlavə olaraq, hər hansı bir müqavilə üçün rəsmi yoxlama xüsusilə tələb olunacaq: bir qayda olaraq, işə salındıqdan sonra müqavilə səhvini düzəltmək mümkün deyil.
Və bu cür səhvlərin qiyməti çox yüksək ola bilər, çünki çox vaxt ağıllı müqavilələrdə kifayət qədər böyük miqdarda vəsait saxlanılır.
Mənim xarakterim VM PHP və Python dillərində yazılmışdır və əldə edilən SMT düsturlarını həll etmək üçün Microsoft Research-in Z3Prover proqramından istifadə edir.
Onun əsasını güclü çox əməliyyatlı axtarış təşkil edir
bir çox əməliyyat tələb etsə belə, həllər və ya zəiflikləri tapmağa imkan verir.
Hətta , Ethereum zəifliklərini tapmaq üçün ən güclü xarakter çərçivələrindən biri, bu qabiliyyəti yalnız bir neçə ay əvvəl əlavə etdi.
Ancaq qeyd etmək lazımdır ki, efir müqavilələri daha mürəkkəbdir və Turing-tamlığına malikdir.
PHP, RIDE smart müqaviləsinin mənbə kodunu python skriptinə tərcümə edir, burada proqram Z3 SMT-uyğun müqavilə dövlətləri və onların keçid şərtləri sistemi kimi təqdim olunur:
İndi içəridə baş verənləri daha ətraflı təsvir edəcəyəm.
Ancaq əvvəlcə RIDE ağıllı müqavilə dili haqqında bir neçə söz.
Dizayn baxımından tənbəl olan funksional və ifadəyə əsaslanan proqramlaşdırma dilidir.
RIDE blokçeyn daxilində təcrid olunmuş şəkildə işləyir və istifadəçinin pul kisəsi ilə əlaqəli yaddaşdan məlumat çıxara və yaza bilər.
Hər bir pul kisəsinə RIDE müqaviləsi əlavə edilə bilər və icranın nəticəsi yalnız DOĞRU və ya YANLIŞ olacaqdır.
DOĞRU o deməkdir ki, ağıllı müqavilə əməliyyata icazə verir və YANLIŞ onu qadağan edir.
Sadə bir nümunə: cüzdan balansı 100-dən az olarsa, skript köçürməni qadağan edə bilər.
Nümunə olaraq, eyni Qurd, Keçi və Kələm götürəcəyəm, lakin artıq ağıllı bir müqavilə şəklində təqdim olunur.
İstifadəçi hər kəsi qarşı tərəfə göndərənə qədər müqavilənin yerləşdiyi cüzdandan pul çıxara bilməyəcək.
#Извлекаем положение всех объектов из блокчейна
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 əvvəlcə ağıllı müqavilədən bütün dəyişənləri açarları və müvafiq boolean ifadəsi şəklində çıxarır.
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 daha sonra onları Z3Prover SMT uyğun python sisteminin təsvirinə çevirir.
Məlumatlar dövrəyə bükülür, burada saxlama dəyişənləri indeksi i alır, əməliyyat dəyişənləri indeksi i + 1 və ifadələri olan dəyişənlər əvvəlki vəziyyətdən növbəti vəziyyətə keçid qaydalarını təyin edir.
Bu, çox əməliyyatlı axtarış mexanizmini təmin edən virtual maşınımızın ürəyidir.
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] )
Şərtlər çeşidlənir və python-da SMT sistemini təsvir etmək üçün hazırlanmış skript şablonuna daxil edilir.
Boş şablon
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()
Bütün zəncirin son vəziyyəti üçün köçürmə əməliyyatı bölməsində müəyyən edilmiş qaydalar tətbiq edilir.
Bu o deməkdir ki, Z3Prover son nəticədə müqavilədən pul çıxarmağa imkan verəcək vəziyyətlərin məhz belə dəstlərini axtaracaq.
Nəticədə, biz avtomatik olaraq müqaviləmizin tam funksional SMT modelini əldə edirik.
Əllə tərtib etdiyim əvvəlki məqaləmdəki modelə çox bənzədiyini görə bilərsiniz.
Tamamlanmış Şablon
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()
Başladıqdan sonra Z3Prover ağıllı müqaviləni həll edir və bizim üçün pul çıxarmağa imkan verən əməliyyatlar zəncirini göstərir:
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
Keçid müqaviləsinə əlavə olaraq, öz müqavilələrinizlə sınaqdan keçirə və ya 2 əməliyyatda həll olunan bu sadə nümunəni sınaya bilərsiniz.
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, ilk versiya olduğundan, sintaksis çox məhduddur və səhvlər ola bilər.
Növbəti məqalələrdə VM-nin gələcək inkişafını əhatə etməyi planlaşdırıram və onunla rəsmi olaraq təsdiqlənmiş ağıllı müqavilələri necə yarada biləcəyinizi və sadəcə onları həll etməyinizi planlaşdırıram.
Simvol virtual maşını burada mövcuddur
VM personajının mənbə kodunu qaydasına salıb oraya şərhlər əlavə etdikdən sonra onu pulsuz girişdə github-a yerləşdirməyi planlaşdırıram.
Mənbə: www.habr.com