🥇Paglikha ng isang pormal na sistema ng pag-verify mula sa simula. Bahagi 1: Character Virtual Machine sa PHP at Python

Ang pormal na pag-verify ay ang pag-verify ng isang programa o algorithm gamit ang isa pa.

Isa ito sa pinakamakapangyarihang pamamaraan na nagbibigay-daan sa iyong mahanap ang lahat ng mga kahinaan sa isang programa o patunayan na wala ang mga ito.

Ang isang mas detalyadong paglalarawan ng pormal na pagpapatunay ay makikita sa halimbawa ng paglutas ng problema ng Lobo, Kambing, at Repolyo sa aking nakaraang artikulo.

Sa artikulong ito lumipat ako mula sa pormal na pag-verify ng mga problema patungo sa mga programa at inilalarawan kung paano
paano sila awtomatikong mako-convert sa mga pormal na sistema ng panuntunan.

Upang gawin ito, isinulat ko ang aking sariling analogue ng isang virtual machine, gamit ang mga simbolikong prinsipyo.

Pina-parse nito ang program code at isinasalin ito sa isang system of equation (SMT), na maaari nang lutasin sa programmatically.

Dahil ang impormasyon tungkol sa mga simbolikong kalkulasyon ay ipinakita sa Internet sa halip fragmentarily,
Ilalarawan ko nang maikli kung ano ito.

Ang simbolikong pag-compute ay isang paraan upang sabay-sabay na magsagawa ng isang programa sa isang malawak na hanay ng data at ito ang pangunahing tool para sa pormal na pag-verify ng programa.

Halimbawa, maaari tayong magtakda ng mga kundisyon sa pag-input kung saan ang unang argumento ay maaaring kumuha ng anumang positibong halaga, ang pangalawang negatibo, ang ikatlong zero, at ang output na argumento, halimbawa, 42.

Ang mga simbolikong kalkulasyon sa isang pagtakbo ay magbibigay sa amin ng sagot kung posible para sa amin na makuha ang nais na resulta at isang halimbawa ng isang set ng naturang mga parameter ng input. O patunay na walang ganoong mga parameter.

Bukod dito, maaari naming itakda ang input argument sa lahat ng posibleng mga, at piliin lamang ang mga output, halimbawa, ang administrator password.

Sa kasong ito, mahahanap namin ang lahat ng mga kahinaan ng program o makakakuha kami ng patunay na ligtas ang password ng administrator.

Mapapansin na ang klasikal na pagpapatupad ng isang programa na may partikular na data ng pag-input ay isang espesyal na kaso ng simbolikong pagpapatupad.

Samakatuwid, ang aking karakter na VM ay maaari ding gumana sa emulation mode ng isang karaniwang virtual machine.

Sa mga komento sa nakaraang artikulo ay makakahanap ng patas na pagpuna sa pormal na pagpapatunay na may pagtalakay sa mga kahinaan nito.

Ang mga pangunahing problema ay:

Kombinatoryal na pagsabog, dahil ang pormal na pag-verify sa huli ay bumaba sa P=NP
Ang pagproseso ng mga tawag sa file system, mga network at iba pang panlabas na storage ay mas mahirap i-verify
Mga bug sa detalye, kapag ang customer o programmer ay naglaan ng isang bagay, ngunit hindi ito inilarawan nang tumpak sa teknikal na detalye.

Bilang resulta, ang programa ay mabe-verify at susunod sa detalye, ngunit gagawa ng isang bagay na ganap na naiiba sa inaasahan ng mga tagalikha mula dito.

Dahil sa artikulong ito, higit sa lahat ay isinasaalang-alang ko ang paggamit ng pormal na pag-verify sa pagsasanay, hindi ko iuuntog ang aking ulo sa dingding sa ngayon, at pipili ako ng isang sistema kung saan ang pagiging kumplikado ng algorithm at ang bilang ng mga panlabas na tawag ay minimal.

Dahil ang mga matalinong kontrata ay pinakaangkop sa mga kinakailangang ito, ang pagpipilian ay nahulog sa mga kontrata ng RIDE mula sa Waves platform: ang mga ito ay hindi kumpleto sa Turing, at ang kanilang pinakamataas na kumplikado ay artipisyal na limitado.

Ngunit isasaalang-alang namin ang mga ito ng eksklusibo mula sa teknikal na bahagi.

Bilang karagdagan sa lahat, ang pormal na pag-verify ay higit na hihilingin para sa anumang mga kontrata: kadalasan ay imposibleng itama ang isang error sa kontrata pagkatapos itong mailunsad.
At ang halaga ng naturang mga pagkakamali ay maaaring napakataas, dahil ang medyo malaking halaga ng mga pondo ay madalas na nakaimbak sa mga matalinong kontrata.

Ang aking simbolikong virtual machine ay nakasulat sa PHP at Python, at gumagamit ng Z3Prover mula sa Microsoft Research upang malutas ang mga resultang SMT formula.

Sa kaibuturan nito ay isang malakas na multi-transactional na paghahanap, na
nagbibigay-daan sa iyo na makahanap ng mga solusyon o kahinaan, kahit na nangangailangan ito ng maraming transaksyon.
Kahit na Mythril, isa sa pinakamakapangyarihang simbolikong balangkas para sa paghahanap ng mga kahinaan ng Ethereum, idinagdag lamang ang kakayahang ito ilang buwan na ang nakalipas.

Ngunit ito ay nagkakahalaga ng noting na eter kontrata ay mas kumplikado at Turing kumpleto.

Isinasalin ng PHP ang source code ng RIDE smart contract sa isang python script, kung saan ipinakita ang programa bilang isang Z3 SMT-compatible na sistema ng mga estado ng kontrata at kundisyon para sa kanilang mga transition:

Ngayon ay ilalarawan ko kung ano ang nangyayari sa loob nang mas detalyado.

Ngunit una, ilang salita tungkol sa RIDE smart contract language.

Ito ay isang functional at expression-based na programming language na tamad sa disenyo.
Ang RIDE ay tumatakbo nang nakahiwalay sa loob ng blockchain at maaaring kunin at magsulat ng impormasyon mula sa storage na naka-link sa wallet ng user.

Maaari kang mag-attach ng kontrata ng RIDE sa bawat wallet, at ang resulta ng pagpapatupad ay magiging TAMA o MALI.

Ang ibig sabihin ng TRUE ay pinapayagan ng smart contract ang transaksyon, at ang FALSE ay nangangahulugan na ipinagbabawal ito.
Isang simpleng halimbawa: maaaring ipagbawal ng isang script ang paglipat kung ang balanse ng wallet ay mas mababa sa 100.

Bilang halimbawa, kukuha ako ng parehong Lobo, Kambing, at Repolyo, ngunit ipinakita na sa anyo ng isang matalinong kontrata.

Ang user ay hindi makakapag-withdraw ng pera mula sa wallet kung saan naka-deploy ang kontrata hanggang sa maipadala niya ang lahat sa kabilang panig.

#Извлекаем положение всех объектов из блокчейна
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

}

Kinukuha muna ng PHP ang lahat ng variable mula sa smart contract sa anyo ng kanilang mga key at ang kaukulang Boolean expression variable.

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

Pagkatapos ay iko-convert ng PHP ang mga ito sa isang paglalarawan ng system na katugma sa Z3Prover SMT sa Python.
Ang data ay nakabalot sa isang loop, kung saan ang mga variable ng storage ay tumatanggap ng index i, ang mga variable ng transaksyon index i + 1, at ang mga variable na may mga expression ay nagtatakda ng mga panuntunan para sa paglipat mula sa nakaraang estado patungo sa susunod.

Ito ang pinakapuso ng aming virtual machine, na nagbibigay ng multi-transactional na search engine.

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

Ang mga kundisyon ay pinagsunod-sunod at ipinasok sa isang script template na idinisenyo upang ilarawan ang SMT system sa Python.

Blangkong template


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

Para sa huling estado sa buong chain, inilalapat ang mga panuntunang tinukoy sa seksyon ng transaksyon sa paglilipat.

Nangangahulugan ito na hahanapin ng Z3Prover ang mga tiyak na hanay ng mga kundisyon na sa huli ay magbibigay-daan sa pag-withdraw ng mga pondo mula sa kontrata.

Bilang resulta, awtomatiko kaming nakakatanggap ng fully functional na modelo ng SMT ng aming kontrata.
Maaari mong makita na ito ay halos kapareho sa modelo mula sa aking nakaraang artikulo, na manu-mano kong pinagsama-sama.

Nakumpleto ang template


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

Pagkatapos ng paglunsad, nilulutas ng Z3Prover ang matalinong kontrata at nagbibigay sa amin ng isang hanay ng mga transaksyon na magbibigay-daan sa aming mag-withdraw ng mga pondo:

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

Bilang karagdagan sa kontrata ng ferry, maaari kang mag-eksperimento sa iyong sariling mga kontrata o subukan ang simpleng halimbawang ito, na nalutas sa 2 mga transaksyon.

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

}

Dahil ito ang pinakaunang bersyon, ang syntax ay napakalimitado at maaaring may mga bug.
Sa mga sumusunod na artikulo, plano kong saklawin ang karagdagang pag-unlad ng VM, at ipakita kung paano ka makakagawa ng pormal na na-verify na mga smart na kontrata sa tulong nito, at hindi lamang lutasin ang mga ito.

Ang character na virtual machine ay magagamit sa http://2.59.42.98/hyperbox/
Matapos ilagay ang source code ng simbolikong VM sa pagkakasunud-sunod at magdagdag ng mga komento doon, plano kong ilagay ito sa GitHub para sa libreng pag-access.

Pinagmulan: www.habr.com

Paglikha ng isang pormal na sistema ng pag-verify mula sa simula. Bahagi 1: Character Virtual Machine sa PHP at Python

Magdagdag ng komento Kanselahin ang sumagot