🥇Mamorona rafitra fanamarinana ofisialy hatrany am-boalohany. Fizarana 1: Machine Virtual amin'ny PHP sy Python

Ny fanamarinana ofisialy dia ny fanamarinana ny programa iray na algorithm amin'ny fampiasana hafa.

Io no iray amin'ireo fomba mahery vaika ahafahanao mahita ny vulnerability rehetra amin'ny programa iray na manaporofo fa tsy misy izy ireo.

Ny famaritana amin'ny antsipiriany bebe kokoa momba ny fanamarinana ofisialy dia azo jerena ao amin'ny ohatra amin'ny famahana ny olan'ny Amboadia sy osy ary laisoa ao amin'ny lahatsoratro teo aloha.

Ato amin'ity lahatsoratra ity aho dia miala amin'ny fanamarinana ofisialy ny olana mankany amin'ny programa ary mamaritra ny fomba
ahoana no ahafahana mamadika azy ireo ho rafitra ara-dalàna ho azy.

Mba hanaovana izany, dia nanoratra ny analogue an'ny milina virtoaly aho, mampiasa fitsipika an'ohatra.

Izy io dia mamadika ny kaody programa ary mandika azy ho rafitra fampitoviana (SMT), izay efa azo voavaha amin'ny programa.

Koa satria ny fampahalalana momba ny kajikajy an'ohatra dia aseho amin'ny Internet amin'ny ampahany kely,
Holazaiko fohifohy hoe inona izany.

Ny kajy an'ohatra dia fomba iray ahafahana manatanteraka programa iray amin'ny angon-drakitra midadasika ary izy no fitaovana lehibe ho an'ny fanamarinana programa ofisialy.

Ohatra, azontsika atao ny mametraka fepetra fampidirana izay ahafahan'ny tohan-kevitra voalohany mandray sanda tsara, ny ratsy faharoa, ny zero fahatelo, ary ny tohan-kevitra mivoaka, ohatra, 42.

Ny kajy an'ohatra amin'ny hazakazaka iray dia hanome antsika ny valiny raha azo atao ny mahazo ny vokatra tadiavina sy ny ohatra amin'ny andiana masontsivana fampidirana toy izany. Na porofo fa tsy misy paramètre toy izany.

Ankoatr'izay, azontsika atao ny mametraka ny tohan-kevitra fampidirana amin'ireo izay azo atao rehetra, ary misafidy ny vokatra vokarina ihany, ohatra, ny tenimiafina mpitantana.

Amin'ity tranga ity, ho hitantsika ny fahalemen'ny programa rehetra na hahazo porofo fa azo antoka ny tenimiafin'ny mpitantana.

Tsara homarihina fa ny famonoana klasika ny programa miaraka amin'ny angona fampidirana manokana dia tranga manokana amin'ny famonoana an'ohatra.

Noho izany, ny toetrako VM dia afaka miasa amin'ny fomba fanahafana amin'ny milina virtoaly mahazatra.

Ao amin'ny fanehoan-kevitra amin'ny lahatsoratra teo aloha dia afaka mahita tsikera ara-drariny momba ny fanamarinana ofisialy miaraka amin'ny fifanakalozan-kevitra momba ny fahalemeny.

Ny olana lehibe dia:

Fipoahana combinatorial, satria ny fanamarinana ofisialy dia tonga hatrany amin'ny P=NP
Sarotra kokoa ny manamarina ny fanodinana antso amin'ny rafi-drakitra, tambajotra ary fitahirizana ivelany hafa
Ny bibikely ao amin'ny famaritana, rehefa nikasa zavatra iray ny mpanjifa na ny programmer, saingy tsy nanoritsoritra azy tsara tamin'ny famaritana ara-teknika.

Vokatr'izany, ny programa dia hohamarinina sy hifanaraka amin'ny famaritana, fa hanao zavatra hafa tanteraka amin'ny zavatra nandrasan'ny mpamorona azy.

Koa satria ato amin'ity lahatsoratra ity aho dia mandinika indrindra ny fampiasana ny fanamarinana ara-dalàna amin'ny fampiharana, tsy hidona amin'ny rindrina ny lohako amin'izao fotoana izao, ary hifidy rafitra iray izay kely indrindra ny fahasarotana algorithmika sy ny isan'ny antso ivelany.

Satria mifanaraka tsara amin'ireo fepetra ireo ny fifanarahana marani-tsaina, dia nilatsaka tamin'ny fifanarahana RIDE avy amin'ny sehatra Waves ny safidy: tsy feno Turing izy ireo, ary voafetra amin'ny fomba artifisialy ny fahasarotana ambony indrindra.

Fa ny lafiny teknika ihany no hojerentsika.

Ho fanampin'ny zava-drehetra, ny fanamarinana ara-dalàna dia tena ilaina indrindra amin'ny fifanarahana rehetra: matetika tsy azo atao ny manitsy ny fahadisoana amin'ny fifanarahana aorian'ny nanombohana azy.
Ary ny vidin'ny fahadisoana toy izany dia mety ho avo be, satria vola be dia be no voatahiry matetika amin'ny fifanarahana marani-tsaina.

Ny milina virtoaly an'ohatra dia nosoratana tamin'ny PHP sy Python, ary mampiasa Z3Prover avy amin'ny Microsoft Research mba hamahana ireo formulas SMT vokatra.

Amin'ny fotony dia fikarohana multitransactional mahery vaika, izay
mamela anao hahita vahaolana na vulnerability, na dia mitaky fifampiraharahana maro aza izany.
Na ny Mythril, iray amin'ireo rafitra an'ohatra matanjaka indrindra amin'ny fitadiavana ny vulnerabilities Ethereum, dia nanampy io fahaiza-manao io volana vitsivitsy lasa izay.

Saingy tsara ny manamarika fa sarotra kokoa ny fifanarahana etera ary feno i Turing.

Ny PHP dia mandika ny kaody loharanon'ny fifanarahana marani-tsaina RIDE ho script python, izay anehoana ny programa ho rafitra mifanaraka amin'ny Z3 SMT amin'ny fifanarahana sy ny fepetra ho an'ny tetezamita:

Ankehitriny dia holazaiko amin'ny antsipiriany kokoa ny zava-mitranga ao anatiny.

Fa aloha, teny vitsivitsy momba ny fiteny fifanarahana marani-tsaina RIDE.

Izy io dia fiteny fandaharana miasa sy mifototra amin'ny fiteny izay kamo amin'ny famolavolana.
Ny RIDE dia mandeha mitokana ao anatin'ny blockchain ary afaka maka sy manoratra vaovao avy amin'ny fitahirizana mifandray amin'ny poketran'ny mpampiasa.

Azonao atao ny mampiditra fifanarahana RIDE amin'ny kitapom-bola tsirairay, ary ny vokatry ny famonoana dia ho MARINA na DISO ihany.

TRUE dia midika fa ny fifanarahana marani-tsaina dia mamela ny fifampiraharahana, ary ny FALSE dia midika fa mandrara izany.
Ohatra tsotra: ny script dia afaka mandrara ny famindrana raha latsaky ny 100 ny sandan'ny kitapom-bola.

Ohatra, haka ny amboadia, osy, ary laisoa mitovy aho, saingy efa naseho tamin'ny endrika fifanarahana marani-tsaina.

Ny mpampiasa dia tsy afaka maka vola amin'ny poketra izay ametrahana ny fifanarahana raha tsy efa nandefa ny rehetra ho any amin'ny ilany.

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

}

Ny PHP aloha dia mamoaka ny fari-piainana rehetra avy amin'ny fifanarahana marani-tsaina amin'ny endriky ny fanalahidin'izy ireo sy ny fari-pitenenana Boolean mifanaraka aminy.

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 dia mamadika azy ireo ho famaritana rafitra mifanaraka amin'ny Z3Prover SMT amin'ny Python.
Ny angon-drakitra dia nofonosina amin'ny tadivavarana, izay misy ny fari-piadidiana mahazo ny index i, ny transaction variables index i + 1, ary ny variables miaraka amin'ny fitenenana dia mametraka ny fitsipika momba ny fifindrana avy amin'ny fanjakana teo aloha mankany amin'ny manaraka.

Io no ivon'ny milina virtoaly misy antsika, izay manome mekanika fikarohana isan-karazany.

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

Ny fepetra dia alaina ary ampidirina ao anaty maodely script natao hamaritana ny rafitra SMT amin'ny Python.

Môdely banga


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

Ho an'ny fanjakana farany amin'ny rojo manontolo, ny fitsipika voalaza ao amin'ny fizarana fifampiraharahana dia ampiharina.

Midika izany fa ny Z3Prover dia hikaroka ireo fepetra mifanaraka amin'izany izay ahafahana manala ny vola amin'ny fifanarahana amin'ny farany.

Vokatr'izany dia mahazo modely SMT miasa tanteraka amin'ny fifanarahanay izahay.
Hitanao fa tena mitovy amin'ny modely avy amin'ny lahatsoratro teo aloha, izay nanangona tanana aho.

Môdely vita


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

Aorian'ny fandefasana, Z3Prover dia mamaha ny fifanarahana marani-tsaina ary manome antsika rojo fifampiraharahana izay ahafahantsika misintona vola:

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

Ho fanampin'ny fifanarahana ferry, azonao atao ny manandrana ny fifanarahanao manokana na manandrana ity ohatra tsotra ity, izay voavaha amin'ny fifanakalozana 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

}

Koa satria ity no dikan-teny voalohany indrindra, dia tena voafetra ny syntax ary mety hisy bibikely.
Ao amin'ny lahatsoratra manaraka, mikasa ny handrakotra ny fampandrosoana bebe kokoa ny VM aho, ary hampiseho ny fomba ahafahanao mamorona fifanarahana marani-tsaina voamarina ara-dalàna miaraka amin'ny fanampiany, fa tsy hamaha azy ireo fotsiny.

Ny milina virtoaly toetra dia hita ao amin'ny http://2.59.42.98/hyperbox/
Rehefa avy nametraka ny kaody loharanon'ny VM an'ohatra sy nampiana fanehoan-kevitra tao aho dia mikasa ny hametraka izany ao amin'ny GitHub ho an'ny fidirana maimaim-poana.

Source: www.habr.com

Mamorona rafitra fanamarinana ofisialy hatrany am-boalohany. Fizarana 1: milina virtoaly toetra amin'ny PHP sy Python

Add a comment cancel reply