Verifikasi formal adalah verifikasi suatu program atau algoritma dengan menggunakan program atau algoritma lain.
Ini adalah salah satu metode paling ampuh yang memungkinkan Anda menemukan semua kerentanan dalam suatu program atau membuktikan bahwa kerentanan tersebut tidak ada.
Penjelasan lebih rinci mengenai verifikasi formal dapat dilihat pada contoh penyelesaian masalah di artikel saya sebelumnya.
Dalam artikel ini saya beralih dari verifikasi formal masalah ke program dan menjelaskan caranya
bagaimana mereka dapat diubah menjadi sistem aturan formal secara otomatis.
Untuk melakukan ini, saya menulis analogi saya sendiri tentang mesin virtual, menggunakan prinsip simbolik.
Ini mem-parsing kode program dan menerjemahkannya ke dalam sistem persamaan (SMT), yang sudah dapat diselesaikan secara terprogram.
Karena informasi tentang perhitungan simbolik disajikan di Internet secara terpisah-pisah,
Saya akan menjelaskan secara singkat apa itu.
Komputasi simbolik adalah cara untuk mengeksekusi suatu program secara bersamaan pada sejumlah besar data dan merupakan alat utama untuk verifikasi program formal.
Misalnya, kita dapat mengatur kondisi masukan di mana argumen pertama dapat mengambil nilai positif apa pun, argumen kedua negatif, nol ketiga, dan argumen keluaran, misalnya, 42.
Perhitungan simbolis dalam sekali proses akan memberi kita jawaban apakah mungkin bagi kita untuk memperoleh hasil yang diinginkan dan contoh sekumpulan parameter masukan tersebut. Atau bukti bahwa tidak ada parameter seperti itu.
Selain itu, kita dapat mengatur argumen masukan ke semua argumen yang memungkinkan, dan memilih hanya argumen keluaran, misalnya kata sandi administrator.
Dalam hal ini, kami akan menemukan semua kerentanan program atau mendapatkan bukti bahwa kata sandi administrator aman.
Dapat dicatat bahwa eksekusi klasik suatu program dengan data masukan tertentu adalah kasus khusus eksekusi simbolik.
Oleh karena itu, karakter VM saya juga dapat bekerja dalam mode emulasi mesin virtual standar.
Dalam komentar pada artikel sebelumnya kita dapat menemukan kritik yang adil terhadap verifikasi formal dengan diskusi tentang kelemahannya.
Masalah utamanya adalah:
- Ledakan kombinatorial, karena verifikasi formal pada akhirnya menghasilkan P=NP
- Memproses panggilan ke sistem file, jaringan, dan penyimpanan eksternal lainnya lebih sulit diverifikasi
- Bug dalam spesifikasi, ketika pelanggan atau pemrogram menginginkan satu hal, tetapi tidak menjelaskannya dengan cukup akurat dalam spesifikasi teknis.
Hasilnya, program tersebut akan diverifikasi dan memenuhi spesifikasi, tetapi akan melakukan sesuatu yang sama sekali berbeda dari yang diharapkan pembuatnya.
Karena dalam artikel ini saya terutama mempertimbangkan penggunaan verifikasi formal dalam praktiknya, saya tidak akan membenturkan kepala untuk saat ini, dan akan memilih sistem di mana kompleksitas algoritmik dan jumlah panggilan eksternal minimal.
Karena kontrak pintar paling sesuai dengan persyaratan ini, pilihan jatuh pada kontrak RIDE dari platform Waves: kontrak tersebut belum lengkap dari Turing, dan kompleksitas maksimumnya dibatasi secara artifisial.
Namun kami akan mempertimbangkannya secara eksklusif dari sisi teknis.
Selain itu, verifikasi formal akan sangat dibutuhkan untuk kontrak apa pun: biasanya tidak mungkin memperbaiki kesalahan kontrak setelah diluncurkan.
Dan kerugian akibat kesalahan seperti itu bisa sangat tinggi, karena sejumlah besar dana sering kali disimpan dalam kontrak pintar.
Mesin virtual simbolis saya ditulis dalam PHP dan Python, dan menggunakan Z3Prover dari Microsoft Research untuk menyelesaikan rumus SMT yang dihasilkan.
Intinya adalah pencarian multi-transaksional yang kuat, yang
memungkinkan Anda menemukan solusi atau kerentanan, meskipun memerlukan banyak transaksi.
Bahkan , salah satu kerangka simbolis paling kuat untuk menemukan kerentanan Ethereum, baru menambahkan kemampuan ini beberapa bulan yang lalu.
Namun perlu dicatat bahwa kontrak eter lebih kompleks dan Turing lengkap.
PHP menerjemahkan kode sumber kontrak pintar RIDE ke dalam skrip python, di mana program disajikan sebagai sistem status kontrak dan ketentuan transisi yang kompatibel dengan Z3 SMT:
Sekarang saya akan menjelaskan apa yang terjadi di dalam secara lebih rinci.
Namun pertama-tama, beberapa kata tentang bahasa kontrak pintar RIDE.
Ini adalah bahasa pemrograman fungsional dan berbasis ekspresi yang desainnya malas.
RIDE berjalan secara terisolasi di dalam blockchain dan dapat mengambil dan menulis informasi dari penyimpanan yang terhubung ke dompet pengguna.
Anda dapat melampirkan kontrak RIDE ke setiap dompet, dan hasil eksekusinya hanya TRUE atau FALSE.
TRUE berarti kontrak pintar mengizinkan transaksi, dan FALSE berarti melarangnya.
Contoh sederhananya: sebuah skrip dapat melarang transfer jika saldo dompet kurang dari 100.
Sebagai contoh, saya akan mengambil Serigala, Kambing, dan Kubis yang sama, tetapi sudah disajikan dalam bentuk kontrak pintar.
Pengguna tidak akan dapat menarik uang dari dompet tempat kontrak diterapkan sampai dia mengirim semua orang ke pihak lain.
#Извлекаем положение всех объектов из блокчейна
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 pertama-tama mengekstrak semua variabel dari kontrak pintar dalam bentuk kuncinya dan variabel ekspresi Boolean yang sesuai.
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 mengubahnya menjadi deskripsi sistem yang kompatibel dengan Z3Prover SMT dengan Python.
Data dibungkus dalam satu lingkaran, di mana variabel penyimpanan menerima indeks i, variabel transaksi mengindeks i + 1, dan variabel dengan ekspresi menetapkan aturan untuk transisi dari keadaan sebelumnya ke keadaan berikutnya.
Ini adalah inti dari mesin virtual kami, yang menyediakan mekanisme pencarian multi-transaksional.
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] )
Kondisi diurutkan dan dimasukkan ke dalam templat skrip yang dirancang untuk menggambarkan sistem SMT dengan 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 di seluruh rantai, aturan yang ditentukan di bagian transaksi transfer diterapkan.
Artinya, Z3Prover akan mencari serangkaian kondisi yang pada akhirnya memungkinkan penarikan dana dari kontrak.
Hasilnya, kami secara otomatis menerima model kontrak SMT yang berfungsi penuh.
Anda dapat melihat bahwa ini sangat mirip dengan model dari artikel saya sebelumnya, yang saya kompilasi secara manual.
Templat yang sudah selesai
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()
Setelah peluncuran, Z3Prover menyelesaikan kontrak pintar dan memberi kami rantai transaksi yang memungkinkan kami menarik 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 dapat bereksperimen dengan kontrak Anda sendiri atau mencoba contoh sederhana 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
}
Karena ini adalah versi pertama, sintaksnya sangat terbatas dan mungkin terdapat bug.
Dalam artikel berikut, saya berencana untuk membahas pengembangan lebih lanjut dari VM, dan menunjukkan bagaimana Anda dapat membuat kontrak pintar yang terverifikasi secara formal dengan bantuannya, dan tidak hanya menyelesaikannya.
Mesin virtual karakter tersedia di
Setelah mengurutkan kode sumber VM simbolis dan menambahkan komentar di sana, saya berencana untuk meletakkannya di GitHub untuk akses gratis.
Sumber: www.habr.com
