Formalna verifikacija je verifikacija jednog programa ili algoritma uz pomoć drugog.
Ovo je jedna od najmoćnijih metoda koja vam omogućava da pronađete sve ranjivosti u programu ili dokažete da one ne postoje.
Detaljniji opis formalne verifikacije može se vidjeti na primjeru rješavanja problema u mom prethodnom članku.
U ovom članku prelazim sa formalne verifikacije problema na programe i opisujem kako
kako ih možete automatski pretvoriti u sisteme formalnih pravila.
Da bih to uradio, napisao sam svoj analog virtuelne mašine, na simboličkim principima.
On analizira programski kod i prevodi ga u sistem jednačina (SMT), koji se već može riješiti programski.
Budući da su informacije o simboličkim proračunima predstavljene na internetu prilično fragmentarno,
Ukratko ću opisati šta je to.
Simbolička izračunavanja su način da se istovremeno izvrši program na širokom spektru podataka i glavni su alat za formalnu verifikaciju programa.
Na primjer, možemo postaviti ulazne uvjete gdje prvi argument može imati bilo koju pozitivnu vrijednost, drugi može biti negativan, treći može biti nula, a izlazni argument je, na primjer, 42.
Simbolička izračunavanja u jednoj vožnji će nam dati odgovor da li je moguće da dobijemo željeni rezultat i primjer skupa takvih ulaznih parametara. Ili dokaz da takvih parametara nema.
Štaviše, možemo postaviti ulazne argumente općenito što je više moguće i odabrati samo izlaz, na primjer, administratorsku lozinku.
U tom slučaju ćemo pronaći sve ranjivosti programa ili ćemo dobiti dokaz da je administratorska lozinka sigurna.
Može se vidjeti da je klasično izvršavanje programa sa specifičnim ulaznim podacima poseban slučaj simboličkog.
Dakle, VM mog karaktera takođe može da radi u režimu emulacije standardne virtuelne mašine.
U komentarima na prethodni članak može se naći i poštena kritika formalne verifikacije sa raspravom o njenim slabostima.
Glavni problemi su:
- Kombinatorna eksplozija, pošto formalna verifikacija na kraju počiva na P=NP
- Rukovanje pozivima sistemu datoteka, mrežama i drugim eksternim pohranama je teže provjeriti
- Greške u specifikaciji, kada je kupac ili programer zamislio jednu stvar, ali je nije precizno opisao u TOR-u.
Kao rezultat toga, program će biti verifikovan i usklađen sa specifikacijom, ali će raditi nešto potpuno drugačije od onoga što su kreatori očekivali od njega.
Pošto u ovom članku uglavnom razmatram primenu formalne verifikacije u praksi, za sada neću lupiti čelo o zid, već ću izabrati sistem gde su algoritamska složenost i broj eksternih poziva minimalni.
Budući da pametni ugovori na najbolji način odgovaraju ovim zahtjevima, izbor je pao na RIDE ugovore sa platforme Waves: oni nisu potpuni po Turingu, a njihova maksimalna složenost je umjetno ograničena.
Ali mi ćemo ih razmotriti isključivo sa tehničke strane.
Uz sve, za bilo koje ugovore posebno će biti tražena formalna verifikacija: po pravilu je nemoguće ispraviti grešku u ugovoru nakon njenog pokretanja.
A cijena takvih grešaka može biti vrlo visoka, budući da su prilično velike količine sredstava često pohranjene na pametnim ugovorima.
Moj karakter VM je napisan u PHP-u i Pythonu i koristi Microsoft Research Z3Prover za rješavanje rezultirajućih SMT formula.
U njegovoj osnovi je moćna multitransakciona pretraga, koja
omogućava vam da pronađete rješenja ili ranjivosti, čak i ako zahtijeva mnogo transakcija.
Čak i , jedan od najmoćnijih okvira karaktera za pronalaženje Ethereum ranjivosti, dodao je ovu mogućnost tek prije nekoliko mjeseci.
Ali vrijedi napomenuti da su eter ugovori složeniji i imaju Turingovu kompletnost.
PHP prevodi izvorni kod RIDE pametnog ugovora u python skriptu, u kojoj je program predstavljen kao Z3 SMT kompatibilan sistem stanja ugovora i njihovih prelaznih uslova:
Sada ću detaljnije opisati šta se dešava unutra.
Ali prvo, nekoliko riječi o RIDE jeziku pametnih ugovora.
To je funkcionalan programski jezik zasnovan na ekspresiji koji je po dizajnu lijen.
RIDE radi u izolaciji unutar blockchaina i može izvući i pisati informacije iz skladišta povezane s korisničkim novčanikom.
RIDE ugovor može biti priložen svakom novčaniku, a rezultat izvršenja će biti samo TAČNO ili LAŽNO.
TRUE znači da pametni ugovor dozvoljava transakciju, a FALSE da je zabranjuje.
Jednostavan primjer: skripta može zabraniti prijenos ako je stanje novčanika manje od 100.
Kao primjer uzet ću iste vuka, koze i kupusa, ali već predstavljene u obliku pametnog ugovora.
Korisnik neće moći podići novac iz novčanika na kojem je ugovor raspoređen sve dok sve ne pošalje na drugu stranu.
#Извлекаем положение всех объектов из блокчейна
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 prvo izdvaja sve varijable iz pametnog ugovora u obliku njihovih ključeva i odgovarajućeg logičkog izraza.
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 ih zatim pretvara u Z3Prover SMT kompatibilan Python sistemski opis.
Podaci su umotani u petlju, gdje varijable za skladištenje primaju indeks i, transakcijske varijable indeks i + 1, a varijable sa izrazima postavljaju pravila za prijelaz iz prethodnog stanja u sljedeće.
Ovo je samo srce naše virtuelne mašine, koja pruža višetransakcioni mehanizam pretraživanja.
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] )
Uslovi se sortiraju i ubacuju u šablon skripte dizajniran da opiše SMT sistem u pythonu.
Prazan šablon
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()
Za posljednje stanje cijelog lanca primjenjuju se pravila koja su postavljena u odjeljku transakcije prijenosa.
To znači da će Z3Prover tražiti upravo takve skupove stanja koji će vam na kraju omogućiti da povučete sredstva iz ugovora.
Kao rezultat, automatski dobijamo potpuno funkcionalan SMT model našeg ugovora.
Vidite da je vrlo sličan modelu iz mog prethodnog članka, koji sam sastavio ručno.
Završen predložak
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()
Nakon lansiranja, Z3Prover rješava pametni ugovor i prikazuje lanac transakcija za nas, što će nam omogućiti da povučemo sredstva:
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
Osim ugovora o ukrštanju, možete eksperimentirati sa vlastitim ugovorima ili isprobati ovaj jednostavan primjer koji se rješava u 2 transakcije.
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
}
Pošto je ovo prva verzija, sintaksa je vrlo ograničena i može postojati greške.
U narednim člancima planiram da pokrijem dalji razvoj VM-a, i pokažem kako sa njim možete kreirati formalno verifikovane pametne ugovore, a ne samo da ih rešavate.
Virtualna mašina karaktera dostupna je na adresi
Nakon što dovedem izvorni kod karakternog VM-a u red i tamo dodam komentare, planiram ga staviti na github u slobodnom pristupu.
izvor: www.habr.com