🥇Kuunda mfumo rasmi wa uthibitishaji kutoka mwanzo. Sehemu ya 1: Mashine ya Tabia ya Tabia katika PHP na Python

Uthibitishaji rasmi ni uthibitishaji wa programu moja au algoriti kwa kutumia nyingine.

Hii ni mojawapo ya njia zenye nguvu zaidi zinazokuwezesha kupata udhaifu wote katika programu au kuthibitisha kuwa haipo.

Maelezo ya kina zaidi ya uthibitishaji rasmi yanaweza kuonekana katika mfano wa kutatua tatizo la Mbwa mwitu, Mbuzi na Kabeji katika makala yangu iliyopita.

Katika nakala hii ninahama kutoka kwa uthibitishaji rasmi wa shida hadi programu na kuelezea jinsi
zinawezaje kubadilishwa kuwa mifumo rasmi ya sheria moja kwa moja.

Ili kufanya hivyo, niliandika analog yangu mwenyewe ya mashine ya kawaida, kwa kutumia kanuni za mfano.

Huchanganua msimbo wa programu na kuitafsiri katika mfumo wa milinganyo (SMT), ambao unaweza tayari kutatuliwa kiprogramu.

Kwa kuwa habari juu ya mahesabu ya mfano huwasilishwa kwenye mtandao kwa sehemu,
Nitaelezea kwa ufupi ni nini.

Kukokotoa kwa ishara ni njia ya kutekeleza kwa wakati mmoja programu kwenye anuwai ya data na ndio zana kuu ya uthibitishaji rasmi wa programu.

Kwa mfano, tunaweza kuweka masharti ya ingizo ambapo hoja ya kwanza inaweza kuchukua maadili yoyote chanya, ya pili hasi, ya tatu sifuri, na hoja ya matokeo, kwa mfano, 42.

Mahesabu ya ishara katika kukimbia moja yatatupa jibu la ikiwa inawezekana kwetu kupata matokeo yaliyohitajika na mfano wa seti ya vigezo vya pembejeo vile. Au ushahidi kwamba hakuna vigezo vile.

Zaidi ya hayo, tunaweza kuweka hoja za pembejeo kwa zote zinazowezekana, na kuchagua tu zile za pato, kwa mfano, nenosiri la msimamizi.

Katika kesi hii, tutapata udhaifu wote wa programu au kupata uthibitisho kwamba nenosiri la msimamizi ni salama.

Inaweza kuzingatiwa kuwa utekelezaji wa classical wa programu na data maalum ya pembejeo ni kesi maalum ya utekelezaji wa ishara.

Kwa hivyo, mhusika wangu VM pia anaweza kufanya kazi katika hali ya kuiga ya mashine ya kawaida ya kawaida.

Katika maoni kwa kifungu kilichopita mtu anaweza kupata ukosoaji wa haki wa uthibitishaji rasmi na mjadala wa udhaifu wake.

Shida kuu ni:

Mlipuko wa pamoja, kwa kuwa uthibitishaji rasmi hatimaye huja hadi P=NP
Kuchakata simu kwa mfumo wa faili, mitandao na hifadhi nyingine ya nje ni vigumu zaidi kuthibitisha
Hitilafu katika vipimo, wakati mteja au programu alikusudia jambo moja, lakini hakulielezea kwa usahihi wa kutosha katika vipimo vya kiufundi.

Matokeo yake, programu itathibitishwa na kuzingatia vipimo, lakini itafanya kitu tofauti kabisa na kile ambacho waundaji walitarajia kutoka kwake.

Kwa kuwa katika makala hii ninazingatia hasa matumizi ya uthibitishaji rasmi katika mazoezi, sitapiga kichwa changu dhidi ya ukuta kwa sasa, na nitachagua mfumo ambapo utata wa algorithmic na idadi ya simu za nje ni ndogo.

Kwa kuwa mikataba mahiri inakidhi mahitaji haya, chaguo lilitokana na kandarasi za RIDE kutoka kwa jukwaa la Waves: hazijakamilika, na ugumu wao wa juu ni mdogo kwa njia ya bandia.

Lakini tutazingatia pekee kutoka upande wa kiufundi.

Mbali na kila kitu, uthibitishaji rasmi utakuwa hasa katika mahitaji ya mikataba yoyote: kwa kawaida haiwezekani kurekebisha kosa la mkataba baada ya kuzinduliwa.
Na gharama ya makosa kama hayo inaweza kuwa ya juu sana, kwani kiasi kikubwa cha fedha mara nyingi huhifadhiwa kwenye mikataba ya smart.

Mashine yangu pepe ya mfano imeandikwa katika PHP na Python, na hutumia Z3Prover kutoka kwa Utafiti wa Microsoft kutatua fomula zinazotokana za SMT.

Katika msingi wake ni utafutaji wenye nguvu wa shughuli nyingi, ambayo
hukuruhusu kupata suluhu au udhaifu, hata kama inahitaji miamala mingi.
Hata Mythril, mojawapo ya mifumo ya ishara yenye nguvu zaidi ya kutafuta udhaifu wa Ethereum, iliongeza tu uwezo huu miezi michache iliyopita.

Lakini inafaa kuzingatia kuwa mikataba ya etha ni ngumu zaidi na Turing imekamilika.

PHP hutafsiri msimbo wa chanzo wa mkataba mahiri wa RIDE kuwa hati ya chatu, ambapo programu inawasilishwa kama mfumo unaolingana na Z3 SMT wa hali za mkataba na masharti ya mabadiliko yao:

Sasa nitaelezea kile kinachotokea ndani kwa undani zaidi.

Lakini kwanza, maneno machache kuhusu lugha ya mkataba mahiri ya RIDE.

Ni lugha ya programu inayofanya kazi na inayojieleza ambayo ni mvivu kwa muundo.
RIDE huendeshwa kwa kutengwa ndani ya blockchain na inaweza kurejesha na kuandika maelezo kutoka kwa hifadhi iliyounganishwa na pochi ya mtumiaji.

Unaweza kuambatisha mkataba wa RIDE kwa kila pochi, na matokeo ya utekelezaji yatakuwa TRUE au FALSE tu.

TRUE inamaanisha kuwa mkataba mahiri unaruhusu muamala, na FALSE inamaanisha kuwa unaupiga marufuku.
Mfano rahisi: hati inaweza kuzuia uhamisho ikiwa salio la pochi ni chini ya 100.

Kama mfano, nitachukua mbwa mwitu sawa, Mbuzi na Kabeji, lakini tayari imewasilishwa kwa njia ya mkataba mzuri.

Mtumiaji hataweza kutoa pesa kutoka kwa mkoba ambao mkataba umewekwa hadi atume kila mtu upande mwingine.

#Извлекаем положение всех объектов из блокчейна
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 kwanza hutoa viambajengo vyote kutoka kwa mkataba mahiri katika mfumo wa funguo zao na kigezo sambamba cha usemi wa Boolean.

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 kisha inazibadilisha kuwa maelezo ya mfumo unaolingana na Z3Prover SMT katika Python.
Data imefungwa kwa kitanzi, ambapo vigeu vya uhifadhi hupokea fahirisi i, vigeu vya muamala index i + 1, na vigeuzo vyenye misemo huweka sheria za mpito kutoka hali ya awali hadi inayofuata.

Huu ndio moyo wa mashine yetu pepe, ambayo hutoa utaratibu wa utafutaji wa shughuli nyingi.

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

Masharti hupangwa na kuingizwa kwenye kiolezo cha hati iliyoundwa kuelezea mfumo wa SMT katika Python.

Kiolezo tupu


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

Kwa hali ya mwisho katika mlolongo mzima, sheria ambazo zimeelezwa katika sehemu ya shughuli ya uhamisho hutumiwa.

Hii inamaanisha kuwa Z3Prover itatafuta kwa usahihi seti kama hizo za masharti ambazo hatimaye zitaruhusu pesa kuondolewa kwenye mkataba.

Kwa hivyo, tunapokea kiotomatiki muundo wa SMT unaofanya kazi kikamilifu wa mkataba wetu.
Unaweza kuona kwamba ni sawa na mfano kutoka kwa makala yangu ya awali, ambayo nilikusanya kwa mikono.

Kiolezo kilichokamilika


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

Baada ya kuzinduliwa, Z3Prover hutatua mkataba mahiri na hutupatia msururu wa miamala ambayo itaturuhusu kutoa pesa:

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

Mbali na mkataba wa kivuko, unaweza kujaribu na mikataba yako mwenyewe au jaribu mfano huu rahisi, ambao unatatuliwa katika shughuli 2.

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

}

Kwa kuwa hili ni toleo la kwanza kabisa, syntax ni mdogo sana na kunaweza kuwa na mende.
Katika makala zifuatazo, nina mpango wa kufunika maendeleo zaidi ya VM, na kuonyesha jinsi unaweza kuunda mikataba ya smart iliyothibitishwa rasmi kwa msaada wake, na si kutatua tu.

Mashine pepe ya herufi inapatikana kwa http://2.59.42.98/hyperbox/
Baada ya kuweka nambari ya chanzo ya VM ya mfano na kuongeza maoni hapo, ninapanga kuiweka kwenye GitHub kwa ufikiaji wa bure.

Chanzo: mapenzi.com

Kuunda mfumo rasmi wa uthibitishaji kutoka mwanzo. Sehemu ya 1: Mashine ya Tabia ya Tabia katika PHP na Python

Kuongeza maoni Kufuta kujibu