Resmi doğrulama, bir programın veya algoritmanın diğerini kullanarak doğrulanmasıdır.
Bu, bir programdaki tüm güvenlik açıklarını bulmanızı veya bunların var olmadığını kanıtlamanızı sağlayan en güçlü yöntemlerden biridir.
Resmi doğrulamanın daha ayrıntılı bir açıklaması, problemin çözümü örneğinde görülebilir. önceki yazımda.
Bu makalede sorunların resmi olarak doğrulanmasından programlara geçiyorum ve bunun nasıl yapıldığını anlatacağım.
otomatik olarak resmi kural sistemlerine nasıl dönüştürülebilirler?
Bunu yapmak için sembolik ilkeleri kullanarak kendi sanal makine analogumu yazdım.
Program kodunu ayrıştırır ve onu zaten programlı olarak çözülebilen bir denklem sistemine (SMT) dönüştürür.
Sembolik hesaplamalarla ilgili bilgiler internette oldukça parçalı olarak sunulduğundan,
Ne olduğunu kısaca anlatacağım.
Sembolik hesaplama, bir programı geniş bir veri yelpazesi üzerinde aynı anda yürütmenin bir yoludur ve resmi program doğrulamanın ana aracıdır.
Örneğin, ilk argümanın herhangi bir pozitif değeri, ikinci negatifin, üçüncü sıfırın ve çıkış argümanının örneğin 42'yi alabileceği giriş koşullarını ayarlayabiliriz.
Tek bir çalıştırmadaki sembolik hesaplamalar bize istenen sonucu elde etmemizin mümkün olup olmadığı sorusunun cevabını ve bu tür giriş parametreleri kümesinin bir örneğini verecektir. Veya böyle parametrelerin olmadığının kanıtı.
Ayrıca, giriş argümanlarını mümkün olan tüm argümanlara ayarlayabilir ve yalnızca çıktı argümanlarını, örneğin yönetici şifresini seçebiliriz.
Bu durumda programın tüm güvenlik açıklarını bulacağız veya yönetici şifresinin güvenli olduğuna dair kanıt alacağız.
Bir programın belirli girdi verileriyle klasik yürütülmesinin, sembolik yürütmenin özel bir durumu olduğu belirtilebilir.
Bu nedenle karakterim VM, standart bir sanal makinenin emülasyon modunda da çalışabilir.
Önceki makaleye yapılan yorumlarda, resmi doğrulamanın zayıf yönlerinin tartışılmasıyla ilgili adil eleştiri bulunabilir.
Başlıca sorunlar şunlardır:
- Kombinatoryal patlama, resmi doğrulamanın sonuçta P=NP'ye inmesi nedeniyle
- Dosya sistemine, ağlara ve diğer harici depolamaya yapılan çağrıların işlenmesinin doğrulanması daha zordur
- Müşterinin veya programcının bir şeyi amaçladığı ancak bunu teknik spesifikasyonda yeterince doğru şekilde tanımlamadığı spesifikasyondaki hatalar.
Sonuç olarak program doğrulanacak ve spesifikasyona uyacak, ancak yaratıcıların ondan beklediğinden tamamen farklı bir şey yapacak.
Bu yazıda esas olarak resmi doğrulamanın pratikte kullanımını ele aldığım için şimdilik kafamı duvara çarpmayacağım, algoritmik karmaşıklığın ve harici çağrı sayısının minimum olduğu bir sistem seçeceğim.
Akıllı sözleşmeler bu gereksinimlere en iyi şekilde uyduğundan, seçim Waves platformundaki RIDE sözleşmelerine düştü: Turing tam değiller ve maksimum karmaşıklıkları yapay olarak sınırlı.
Ancak bunları yalnızca teknik açıdan ele alacağız.
Her şeye ek olarak, herhangi bir sözleşme için resmi doğrulama özellikle talep edilecektir: Bir sözleşme hatasını başlatıldıktan sonra düzeltmek genellikle imkansızdır.
Ve bu tür hataların maliyeti çok yüksek olabilir, çünkü oldukça büyük miktarlarda fon genellikle akıllı sözleşmelerde depolanır.
Sembolik sanal makinem PHP ve Python ile yazılmış ve ortaya çıkan SMT formüllerini çözmek için Microsoft Research'ün Z3Prover'ını kullanıyor.
Özünde güçlü, çok işlemli bir arama bulunur.
çok sayıda işlem gerektirse bile çözüm veya açık bulmanızı sağlar.
Hatta Ethereum'daki güvenlik açıklarını bulmaya yönelik en güçlü sembolik çerçevelerden biri olan bu özellik, yalnızca birkaç ay önce eklendi.
Ancak eter sözleşmelerinin daha karmaşık ve Turing'in eksiksiz olduğunu belirtmekte fayda var.
PHP, RIDE akıllı sözleşmesinin kaynak kodunu bir python betiğine çevirir; burada program, Z3 SMT uyumlu sözleşme durumları ve geçiş koşulları sistemi olarak sunulur:
Şimdi içeride neler olduğunu daha detaylı anlatacağım.
Ama önce RIDE akıllı sözleşme dili hakkında birkaç söz edelim.
Tasarım gereği tembel, işlevsel ve ifade tabanlı bir programlama dilidir.
RIDE, blok zinciri içerisinde izole bir şekilde çalışır ve kullanıcının cüzdanına bağlı depolama alanından bilgi alıp yazabilir.
Her cüzdana bir RIDE sözleşmesi ekleyebilirsiniz ve yürütmenin sonucu yalnızca DOĞRU veya YANLIŞ olacaktır.
DOĞRU, akıllı sözleşmenin işleme izin verdiği, YANLIŞ ise işlemi yasakladığı anlamına gelir.
Basit bir örnek: Bir komut dosyası, cüzdan bakiyesi 100'den azsa aktarımı yasaklayabilir.
Örnek olarak aynı Kurt, Keçi ve Lahanayı alacağım, ancak zaten akıllı bir sözleşme şeklinde sunuldu.
Kullanıcı, herkesi diğer tarafa gönderene kadar sözleşmenin uygulandığı cüzdandan para çekemeyecektir.
#Извлекаем положение всех объектов из блокчейна
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 ilk önce akıllı sözleşmedeki tüm değişkenleri anahtarları ve karşılık gelen Boolean ifade değişkeni biçiminde çıkarı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 bunları Python'da Z3Prover SMT uyumlu sistem açıklamasına dönüştürür.
Veriler, depolama değişkenlerinin indeks i'yi, işlem değişkenleri indeks i + 1'i aldığı ve ifadelere sahip değişkenlerin önceki durumdan diğerine geçiş kurallarını belirlediği bir döngüye sarılır.
Bu, çok işlemli bir arama motoru sağlayan sanal makinemizin tam kalbidir.
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] )
Koşullar sıralanır ve Python'daki SMT sistemini tanımlamak için tasarlanmış bir komut dosyası şablonuna eklenir.
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()
Tüm zincirin son durumu için transfer işlemi bölümünde belirtilen kurallar uygulanır.
Bu, Z3Prover'ın, fonların sözleşmeden çekilmesine eninde sonunda izin verecek tam olarak bu tür koşulları arayacağı anlamına gelir.
Sonuç olarak, sözleşmemizin tamamen işlevsel bir SMT modelini otomatik olarak alıyoruz.
Bir önceki yazımda manuel olarak derlediğim modele oldukça benzediğini görebilirsiniz.
Tamamlanan ş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()
Lansmandan sonra Z3Prover akıllı sözleşmeyi çözer ve bize para çekmemize olanak sağlayacak bir işlemler zinciri sağlar:
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
Feribot sözleşmesine ek olarak kendi sözleşmelerinizi deneyebilir veya 2 işlemde çözülen bu basit örneği deneyebilirsiniz.
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 sürüm olduğu için sözdizimi çok sınırlıdır ve hatalar olabilir.
Aşağıdaki makalelerde, VM'nin daha da geliştirilmesini ele almayı ve onun yardımıyla resmi olarak doğrulanmış akıllı sözleşmeleri nasıl oluşturabileceğinizi ve yalnızca bunları çözmekle kalmayıp nasıl oluşturabileceğinizi göstermeyi planlıyorum.
Karakter sanal makinesi şu adreste mevcuttur:
Sembolik VM'nin kaynak kodunu düzenleyip buraya yorumları ekledikten sonra GitHub'da ücretsiz erişim için yayınlamayı planlıyorum.
Kaynak: habr.com