Formālā pārbaude ir vienas programmas vai algoritma pārbaude, izmantojot citu.
Šī ir viena no jaudīgākajām metodēm, kas ļauj atrast visas programmas ievainojamības vai pierādīt, ka tās neeksistē.
Detalizētāks formālās pārbaudes apraksts ir redzams problēmas risināšanas piemērā manā iepriekšējā rakstā.
Šajā rakstā es pāreju no formālas problēmu pārbaudes uz programmām un aprakstu, kā to izdarīt
kā tos var automātiski pārvērst formālās noteikumu sistēmās.
Lai to izdarītu, es uzrakstīju savu virtuālās mašīnas analogu, izmantojot simboliskus principus.
Tas parsē programmas kodu un pārvērš to vienādojumu sistēmā (SMT), ko jau var atrisināt programmatiski.
Tā kā informācija par simboliskiem aprēķiniem internetā tiek sniegta diezgan fragmentāri,
Es īsi aprakstīšu, kas tas ir.
Simboliskā aprēķins ir veids, kā vienlaicīgi izpildīt programmu ar plašu datu klāstu, un tas ir galvenais rīks oficiālai programmas pārbaudei.
Piemēram, mēs varam iestatīt ievades nosacījumus, kuros pirmais arguments var iegūt jebkādas pozitīvas vērtības, otrais negatīvs, trešais nulle un izvades arguments, piemēram, 42.
Simboliski aprēķini vienā piegājienā sniegs mums atbildi, vai mums ir iespējams iegūt vēlamo rezultātu, un šādu ievades parametru kopas piemēru. Vai arī pierādījums tam, ka tādu parametru nav.
Turklāt mēs varam iestatīt ievades argumentus uz visiem iespējamiem un atlasīt tikai izvades argumentus, piemēram, administratora paroli.
Šajā gadījumā mēs atradīsim visas programmas ievainojamības vai iegūsim pierādījumu, ka administratora parole ir droša.
Var atzīmēt, ka klasiskā programmas izpilde ar konkrētiem ievades datiem ir īpašs simboliskās izpildes gadījums.
Tāpēc mana personāža VM var darboties arī standarta virtuālās mašīnas emulācijas režīmā.
Iepriekšējā raksta komentāros var atrast godīgu formālās pārbaudes kritiku ar tās vājo vietu iztirzājumu.
Galvenās problēmas ir šādas:
- Kombinatorisks sprādziens, jo formālā pārbaude galu galā ir P = NP
- Failu sistēmas, tīklu un citas ārējās atmiņas zvanu apstrādi ir grūtāk pārbaudīt
- Kļūdas specifikācijā, kad pasūtītājs vai programmētājs bija iecerējis vienu lietu, bet nav pietiekami precīzi aprakstījis tehniskajā specifikācijā.
Rezultātā programma tiks pārbaudīta un atbildīs specifikācijai, taču darīs kaut ko pavisam citu, nekā no tās gaidīja veidotāji.
Tā kā šajā rakstā galvenokārt apsveru formālās verifikācijas izmantošanu praksē, tad pagaidām galvu sienā nedauzīšu un izvēlēšos sistēmu, kurā algoritmiskā sarežģītība un ārējo zvanu skaits ir minimāls.
Tā kā viedie līgumi vislabāk atbilst šīm prasībām, izvēle krita uz Waves platformas RIDE līgumiem: tie nav pabeigti Turing, un to maksimālā sarežģītība ir mākslīgi ierobežota.
Bet mēs tos izskatīsim tikai no tehniskās puses.
Papildus visam jebkādiem līgumiem īpaši pieprasīta būs formāla pārbaude: parasti nav iespējams labot līguma kļūdu pēc tās palaišanas.
Un šādu kļūdu izmaksas var būt ļoti augstas, jo viedajos līgumos bieži tiek glabāti diezgan lieli naudas līdzekļi.
Mana simboliskā virtuālā mašīna ir rakstīta PHP un Python valodā, un, lai atrisinātu iegūtās SMT formulas, tiek izmantots Z3Prover no Microsoft Research.
Tās pamatā ir jaudīga vairāku darījumu meklēšana, kas
ļauj atrast risinājumus vai ievainojamības, pat ja tas prasa daudz darījumu.
Pat , kas ir viens no spēcīgākajiem simboliskiem ietvariem Ethereum ievainojamību atrašanai, šo iespēju pievienoja tikai pirms dažiem mēnešiem.
Bet ir vērts atzīmēt, ka ētera līgumi ir sarežģītāki un Tjūringa pilnīgāki.
PHP pārvērš RIDE viedā līguma avota kodu python skriptā, kurā programma tiek parādīta kā ar Z3 SMT saderīga līguma stāvokļu un to pāreju nosacījumu sistēma:
Tagad es sīkāk aprakstīšu, kas notiek iekšā.
Bet vispirms daži vārdi par RIDE viedo līgumu valodu.
Tā ir funkcionāla un uz izteiksmēm balstīta programmēšanas valoda, kuras dizains ir slinks.
RIDE darbojas izolēti blokķēdē un var izgūt un ierakstīt informāciju no krātuves, kas saistīta ar lietotāja maku.
Katram maciņam varat pievienot BRAUKŠANAS līgumu, un izpildes rezultāts būs tikai TRUE vai FALSE.
TRUE nozīmē, ka viedais līgums atļauj veikt darījumu, un FALSE nozīmē, ka tas to aizliedz.
Vienkāršs piemērs: skripts var aizliegt pārskaitījumu, ja maka atlikums ir mazāks par 100.
Kā piemēru ņemšu to pašu Vilku, Kazu un Kāpostu, bet jau uzrādītu viedā līguma veidā.
Lietotājs nevarēs izņemt naudu no maka, uz kura ir izvietots līgums, kamēr nebūs visus nosūtījis uz otru pusi.
#Извлекаем положение всех объектов из блокчейна
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 vispirms izvelk visus mainīgos no viedā līguma to atslēgu un atbilstošā Būla izteiksmes mainīgā veidā.
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
Pēc tam PHP tos pārvērš ar Z3Prover SMT saderīgā sistēmas aprakstā Python.
Dati tiek ietīti cilpā, kur krātuves mainīgie saņem indeksu i, darījumu mainīgie indeksu i + 1, bet mainīgie ar izteiksmēm nosaka noteikumus pārejai no iepriekšējā stāvokļa uz nākamo.
Šī ir mūsu virtuālās mašīnas sirds, kas nodrošina vairāku darījumu meklēšanas mehānismu.
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] )
Nosacījumi tiek sakārtoti un ievietoti skripta veidnē, kas izstrādāta, lai aprakstītu SMT sistēmu Python.
Tukša veidne
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()
Pēdējam stāvoklim visā ķēdē tiek piemēroti noteikumi, kas norādīti pārsūtīšanas darījumu sadaļā.
Tas nozīmē, ka Z3Prover meklēs tieši tādus nosacījumu kopumus, kas galu galā ļaus izņemt līdzekļus no līguma.
Rezultātā mēs automātiski saņemam pilnībā funkcionējošu mūsu līguma SMT modeli.
Var redzēt, ka tas ir ļoti līdzīgs modelim no mana iepriekšējā raksta, kuru es sastādīju manuāli.
Pabeigta veidne
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()
Pēc palaišanas Z3Prover atrisina viedo līgumu un nodrošina mums darījumu ķēdi, kas ļaus mums izņemt līdzekļus:
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
Papildus prāmja līgumam varat eksperimentēt ar saviem līgumiem vai izmēģināt šo vienkāršo piemēru, kas tiek atrisināts 2 darījumos.
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
}
Tā kā šī ir pati pirmā versija, sintakse ir ļoti ierobežota un var būt kļūdas.
Turpmākajos rakstos plānoju aplūkot VM tālāko attīstību un parādīt, kā ar tās palīdzību var izveidot formāli pārbaudītus viedos līgumus, nevis tikai tos atrisināt.
Rakstzīmju virtuālā mašīna ir pieejama vietnē
Pēc simboliskās VM pirmkoda sakārtošanas un komentāru pievienošanas plānoju to ievietot GitHub bezmaksas piekļuvei.
Avots: www.habr.com