Geekly articles weekly

Pembuatan sistem verifikasi formal dari awal. Bagian 1: mesin virtual karakter dalam PHP dan Python

Verifikasi formal adalah verifikasi dari satu program atau algoritma menggunakan yang lain.

Ini adalah salah satu metode paling ampuh yang memungkinkan Anda menemukan semua kerentanan dalam program atau untuk membuktikan bahwa mereka tidak ada.

Deskripsi yang lebih rinci tentang verifikasi formal dapat dilihat pada contoh penyelesaian masalah Wolf, Goat, dan kubis di artikel saya sebelumnya.

Dalam artikel ini, saya akan beralih dari verifikasi formal tugas ke program, dan saya akan jelaskan
cara mengubahnya menjadi sistem aturan formal secara otomatis.

Untuk ini, saya menulis analog saya tentang mesin virtual, dengan prinsip simbolik.

Dia mem-parsing kode program dan menerjemahkannya ke dalam sistem persamaan (SMT), yang sudah dapat dipecahkan secara terprogram.

Karena informasi tentang perhitungan simbolik disajikan di Internet agak terpisah-pisah,
Saya akan menjelaskan secara singkat apa itu.

Perhitungan karakter adalah cara untuk secara bersamaan menjalankan program pada berbagai data dan merupakan alat utama untuk verifikasi formal program.

Sebagai contoh, kita dapat mengatur kondisi input di mana argumen pertama dapat mengambil nilai positif, negatif kedua, ketiga - nol, dan argumen output, misalnya, 42.

Perhitungan simbolik dalam sekali jalan akan memberi kita jawaban, apakah mungkin bagi kita untuk mendapatkan hasil yang diinginkan dan contoh dari serangkaian parameter input tersebut. Atau bukti bahwa tidak ada parameter seperti itu.

Selain itu, kami dapat mengatur argumen input secara umum sebanyak mungkin, dan hanya memilih output, misalnya, kata sandi administrator.

Dalam hal ini, kami akan menemukan semua kerentanan program atau kami akan mendapatkan bukti bahwa kata sandi admin aman.

Anda mungkin memperhatikan bahwa eksekusi klasik suatu program dengan data input spesifik adalah kasus khusus yang simbolis.

Oleh karena itu, VM karakter saya juga dapat bekerja dalam mode emulasi mesin virtual standar.

Dalam komentar di artikel sebelumnya, Anda dapat menemukan kritik yang adil terhadap verifikasi formal dengan diskusi tentang kelemahannya.

Masalah utama adalah sebagai berikut:

  1. Ledakan kombinasi, karena verifikasi formal akhirnya bersandar pada P = NP
  2. Menangani panggilan ke sistem file, jaringan, dan penyimpanan eksternal lainnya lebih sulit untuk diverifikasi
  3. Bug dalam spesifikasi, ketika pelanggan atau programmer menyusun satu hal, tetapi tidak secara akurat menggambarkannya dalam pernyataan kerja.

Akibatnya, program akan diverifikasi dan memenuhi spesifikasi, tetapi tidak akan melakukan apa yang diharapkan pembuatnya.

Karena dalam artikel ini saya terutama mempertimbangkan penerapan verifikasi formal dalam praktiknya, saya belum akan mengalahkan dahi saya, dan saya akan memilih sistem di mana kompleksitas algoritmik dan jumlah panggilan eksternal minimal.

Karena kontrak pintar sesuai dengan persyaratan ini dengan cara terbaik, pilihan jatuh pada kontrak RIDE dari platform Waves: mereka tidak lengkap Turing, dan kompleksitas maksimumnya terbatas secara buatan.

Tapi kami akan mempertimbangkannya hanya dari sisi teknis.

Selain semua, untuk kontrak apa pun, verifikasi formal akan sangat diminati: sebagai aturan, tidak mungkin untuk memperbaiki kesalahan kontrak setelah peluncurannya.
Dan harga kesalahan semacam itu bisa sangat tinggi, karena jumlah dana yang agak besar sering disimpan dalam kontrak yang cerdas.

Mesin virtual karakter saya ditulis dalam PHP dan Python, dan menggunakan Z3Prover dari Microsoft Research untuk menyelesaikan formula SMT yang dihasilkan.

Pada intinya terletak pencarian multi-transaksional yang kuat
memungkinkan Anda untuk menemukan solusi atau kerentanan, bahkan jika itu membutuhkan banyak transaksi.
Bahkan Mythril , salah satu kerangka simbolis yang paling kuat untuk mencari kerentanan Ethereum, menambahkan fitur ini hanya beberapa bulan yang lalu.

Tetapi perlu dicatat bahwa kontrak eter lebih kompleks dan memiliki kelengkapan Turing.

PHP menerjemahkan kode sumber kontrak pintar RIDE menjadi skrip python di mana program disajikan dalam bentuk sistem status kontrak dan ketentuan untuk transisinya yang kompatibel dengan Z3 SMT:



Sekarang saya akan menjelaskan apa yang terjadi di dalam, lebih terinci.

Tapi pertama-tama, beberapa kata tentang bahasa kontrak pintar RIDE.

Ini adalah bahasa pemrograman fungsional dan berbasis ekspresi yang malas sebagaimana dimaksud.
RIDE dilakukan dalam isolasi di dalam blockchain, dan dapat mengekstraksi dan merekam informasi dari penyimpanan yang terkait dengan dompet pengguna.

Anda dapat melampirkan kontrak RIDE ke setiap dompet, dan hasil eksekusi hanya akan BENAR atau SALAH.

BENAR berarti bahwa kontrak pintar memungkinkan transaksi, dan SALAH yang melarangnya.
Contoh sederhana: skrip dapat melarang transfer jika saldo dompet kurang dari 100.

Sebagai contoh, saya akan mengambil semua Serigala, Kambing, dan Kubis yang sama, tetapi sudah disajikan dalam bentuk kontrak pintar.

Pengguna tidak akan dapat menarik uang dari dompet di mana kontrak digunakan sampai ia meneruskan semua orang ke sisi 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 dari kontrak pintar semua variabel dalam bentuk kunci mereka dan variabel yang sesuai dari ekspresi logis.

 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 Python yang kompatibel untuk Z3Prover SMT.
Data dibungkus dalam siklus di mana variabel penyimpanan mendapatkan indeks i, variabel transaksi indeks i +1, dan variabel dengan ekspresi menetapkan aturan untuk transisi dari keadaan sebelumnya ke yang berikutnya.

Ini adalah jantung dari mesin virtual kami, yang menyediakan mesin pencari 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 dalam python.

Template 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("\n\n") 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 dari seluruh rantai, aturan yang ditentukan dalam bagian transaksi transfer berlaku.

Jadi, Z3Prover akan mencari serangkaian kondisi yang pada akhirnya akan memungkinkan Anda untuk menarik dana dari kontrak.

Akibatnya, kami secara otomatis mendapatkan model SMT yang berfungsi penuh dari kontrak kami.
Anda dapat melihat bahwa ini sangat mirip dengan model dari artikel saya sebelumnya, yang saya tulis secara manual.

Template 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("\n\n") 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 diluncurkan, Z3Prover memecahkan kontrak yang cerdas dan menampilkan rantai transaksi kepada kami, yang memungkinkan kami untuk 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 bug dapat terjadi.
Dalam artikel berikut ini saya berencana untuk membahas pengembangan VM lebih lanjut, dan menunjukkan bagaimana mungkin untuk membuat kontrak pintar yang diverifikasi secara formal dengan bantuannya, dan tidak hanya menyelesaikannya.

Mesin virtual simbolis tersedia di http://2.59.42.98/hyperbox/
Sumber tersedia di github: http://github.com/scp1001/hyperbox
Semua logika VM terkandung dalam 2 file, hyperbox.php dan hyperbox2.php

Source: https://habr.com/ru/post/id450016/

More articles:


All Articles