🥇Mewujudkan sistem pengesahan rasmi dari awal. Bahagian 1: Mesin Maya Watak dalam PHP dan Python

Pengesahan formal ialah pengesahan satu program atau algoritma menggunakan yang lain.

Ini adalah salah satu kaedah paling berkuasa yang membolehkan anda mencari semua kelemahan dalam program atau membuktikan bahawa ia tidak wujud.

Penerangan yang lebih terperinci tentang pengesahan rasmi boleh dilihat dalam contoh penyelesaian masalah Serigala, Kambing, dan Kubis dalam artikel saya sebelum ini.

Dalam artikel ini saya beralih daripada pengesahan formal masalah kepada program dan menerangkan caranya
bagaimana ia boleh ditukar menjadi sistem peraturan formal secara automatik.

Untuk melakukan ini, saya menulis analog saya sendiri tentang mesin maya, menggunakan prinsip simbolik.

Ia menghuraikan kod program dan menterjemahkannya ke dalam sistem persamaan (SMT), yang sudah boleh diselesaikan secara pemrograman.

Memandangkan maklumat tentang pengiraan simbolik dibentangkan di Internet secara berpecah-belah,
Saya akan menerangkan secara ringkas apa itu.

Pengiraan simbolik ialah cara untuk melaksanakan program secara serentak pada julat data yang luas dan merupakan alat utama untuk pengesahan program rasmi.

Sebagai contoh, kita boleh menetapkan syarat input di mana hujah pertama boleh mengambil sebarang nilai positif, negatif kedua, sifar ketiga dan hujah keluaran, sebagai contoh, 42.

Pengiraan simbolik dalam satu larian akan memberi kita jawapan sama ada mungkin untuk kita memperoleh hasil yang diingini dan contoh set parameter input tersebut. Atau bukti bahawa tiada parameter sedemikian.

Selain itu, kita boleh menetapkan argumen input kepada semua yang mungkin, dan memilih hanya yang keluaran, sebagai contoh, kata laluan pentadbir.

Dalam kes ini, kami akan menemui semua kelemahan program atau mendapatkan bukti bahawa kata laluan pentadbir selamat.

Perlu diingatkan bahawa pelaksanaan klasik program dengan data input khusus adalah kes khas pelaksanaan simbolik.

Oleh itu, watak saya VM juga boleh berfungsi dalam mod emulasi mesin maya standard.

Dalam ulasan artikel sebelumnya, seseorang boleh mendapatkan kritikan yang adil terhadap pengesahan rasmi dengan perbincangan tentang kelemahannya.

Masalah utama ialah:

Letupan kombinatorial, kerana pengesahan rasmi akhirnya turun kepada P=NP
Memproses panggilan ke sistem fail, rangkaian dan storan luaran lain adalah lebih sukar untuk disahkan
Pepijat dalam spesifikasi, apabila pelanggan atau pengaturcara bertujuan satu perkara, tetapi tidak menerangkannya dengan cukup tepat dalam spesifikasi teknikal.

Akibatnya, program akan disahkan dan mematuhi spesifikasi, tetapi akan melakukan sesuatu yang berbeza sama sekali daripada apa yang pencipta harapkan daripadanya.

Memandangkan dalam artikel ini saya terutamanya mempertimbangkan penggunaan pengesahan rasmi dalam amalan, saya tidak akan menghantukkan kepala saya ke dinding buat masa ini, dan akan memilih sistem yang kerumitan algoritma dan bilangan panggilan luaran adalah minimum.

Memandangkan kontrak pintar paling sesuai dengan keperluan ini, pilihan jatuh pada kontrak RIDE daripada platform Waves: kontrak itu tidak lengkap Turing, dan kerumitan maksimumnya dihadkan secara buatan.

Tetapi kami akan mempertimbangkannya secara eksklusif dari segi teknikal.

Sebagai tambahan kepada segala-galanya, pengesahan rasmi akan sangat diperlukan untuk mana-mana kontrak: selalunya mustahil untuk membetulkan ralat kontrak selepas ia dilancarkan.
Dan kos kesilapan sedemikian boleh menjadi sangat tinggi, kerana jumlah dana yang agak besar sering disimpan pada kontrak pintar.

Mesin maya simbolik saya ditulis dalam PHP dan Python, dan menggunakan Z3Prover daripada Microsoft Research untuk menyelesaikan formula SMT yang terhasil.

Pada terasnya ialah carian berbilang transaksi yang berkuasa, yang
membolehkan anda mencari penyelesaian atau kelemahan, walaupun ia memerlukan banyak transaksi.
Malah Mythril, salah satu rangka kerja simbolik yang paling berkuasa untuk mencari kelemahan Ethereum, hanya menambah keupayaan ini beberapa bulan lalu.

Tetapi perlu diperhatikan bahawa kontrak eter lebih kompleks dan Turing lengkap.

PHP menterjemahkan kod sumber kontrak pintar RIDE ke dalam skrip python, di mana program ini dibentangkan sebagai sistem keadaan kontrak yang serasi dengan Z3 SMT dan syarat untuk peralihannya:

Sekarang saya akan menerangkan apa yang berlaku di dalam dengan lebih terperinci.

Tetapi pertama, beberapa perkataan tentang bahasa kontrak pintar RIDE.

Ia adalah bahasa pengaturcaraan yang berfungsi dan berasaskan ekspresi yang malas dengan reka bentuk.
RIDE berjalan secara berasingan dalam rantaian blok dan boleh mendapatkan dan menulis maklumat daripada storan yang dipautkan ke dompet pengguna.

Anda boleh melampirkan kontrak RIDE pada setiap dompet, dan hasil pelaksanaan hanya BENAR atau SALAH.

BENAR bermakna kontrak pintar membenarkan transaksi, dan SALAH bermakna ia melarangnya.
Contoh mudah: skrip boleh melarang pemindahan jika baki dompet kurang daripada 100.

Sebagai contoh, saya akan mengambil Serigala, Kambing, dan Kubis yang sama, tetapi telah dibentangkan dalam bentuk kontrak pintar.

Pengguna tidak akan dapat mengeluarkan wang dari dompet di mana kontrak itu digunakan sehingga dia menghantar semua orang ke seberang.

#Извлекаем положение всех объектов из блокчейна
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 mula-mula mengekstrak semua pembolehubah daripada kontrak pintar dalam bentuk kunci mereka dan pembolehubah ungkapan Boolean yang sepadan.

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 kemudian menukarnya menjadi penerangan sistem serasi Z3Prover SMT dalam Python.
Data dibalut dalam gelung, di mana pembolehubah storan menerima indeks i, pembolehubah urus niaga indeks i + 1, dan pembolehubah dengan ungkapan menetapkan peraturan untuk peralihan dari keadaan sebelumnya ke keadaan seterusnya.

Ini adalah nadi mesin maya kami, yang menyediakan enjin carian berbilang transaksi.

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] )

Syarat-syarat diisih dan dimasukkan ke dalam templat skrip yang direka untuk menerangkan sistem SMT dalam Python.

Templat kosong


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()

Untuk keadaan terakhir dalam keseluruhan rantaian, peraturan yang dinyatakan dalam bahagian transaksi pemindahan digunakan.

Ini bermakna Z3Prover akan mencari dengan tepat set syarat sedemikian yang akhirnya akan membolehkan dana ditarik balik daripada kontrak.

Akibatnya, kami secara automatik menerima model SMT berfungsi sepenuhnya kontrak kami.
Anda boleh melihat bahawa ia sangat serupa dengan model dari artikel saya sebelum ini, yang saya susun secara manual.

Templat lengkap


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()

Selepas pelancaran, Z3Prover menyelesaikan kontrak pintar dan memberikan kami rangkaian transaksi yang membolehkan kami mengeluarkan dana:

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

Selain kontrak feri, anda boleh bereksperimen dengan kontrak anda sendiri atau mencuba contoh mudah ini, yang diselesaikan dalam 2 transaksi.

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

}

Memandangkan ini adalah versi pertama, sintaksnya sangat terhad dan mungkin terdapat pepijat.
Dalam artikel berikut, saya bercadang untuk membincangkan perkembangan lanjut VM, dan menunjukkan cara anda boleh membuat kontrak pintar yang disahkan secara rasmi dengan bantuannya, dan bukan hanya menyelesaikannya.

Mesin maya watak boleh didapati di http://2.59.42.98/hyperbox/
Selepas meletakkan kod sumber VM simbolik dalam susunan dan menambah komen di sana, saya bercadang untuk meletakkannya di GitHub untuk akses percuma.

Sumber: www.habr.com

Mencipta sistem pengesahan rasmi dari awal. Bahagian 1: Mesin Maya Watak dalam PHP dan Python

Tambah komen Batal reply