Formalna verifikacija je verifikacija jednog programa ili algoritma korištenjem drugog.
Ovo je jedna od najmoćnijih metoda koja vam omogućuje da pronađete sve ranjivosti u programu ili dokažete da ne postoje.
Detaljniji opis formalne provjere može se vidjeti na primjeru rješavanja problema u mom prethodnom članku.
U ovom članku prelazim s formalne provjere problema na programe i opisujem kako
kako se mogu automatski pretvoriti u formalne sustave pravila.
Da bih to učinio, napisao sam svoj vlastiti analog virtualnog stroja, koristeći simbolička načela.
On analizira programski kod i prevodi ga u sustav jednadžbi (SMT), koji se već može riješiti programski.
Budući da su informacije o simboličkim izračunima na internetu predstavljene prilično fragmentarno,
Ukratko ću opisati što je to.
Simboličko izračunavanje način je istovremenog izvršavanja programa na širokom rasponu podataka i glavni je alat za formalnu provjeru programa.
Na primjer, možemo postaviti ulazne uvjete gdje prvi argument može imati bilo koju pozitivnu vrijednost, drugi negativnu, treći nulu, a izlazni argument, na primjer, 42.
Simbolični izračuni u jednom izvođenju dat će nam odgovor je li moguće dobiti željeni rezultat i primjer skupa takvih ulaznih parametara. Ili dokaz da tih parametara nema.
Štoviše, ulazne argumente možemo postaviti na sve moguće, a odabrati samo izlazne, na primjer administratorsku lozinku.
U tom slučaju pronaći ćemo sve ranjivosti programa ili dobiti dokaz da je lozinka administratora sigurna.
Može se primijetiti da je klasično izvođenje programa s određenim ulaznim podacima poseban slučaj simboličkog izvođenja.
Stoga moj lik VM također može raditi u načinu emulacije standardnog virtualnog stroja.
U komentarima na prethodni članak može se pronaći poštena kritika formalne verifikacije uz raspravu o njezinim slabostima.
Glavni problemi su:
- Kombinatorna eksplozija, budući da se formalna verifikacija u konačnici svodi na P=NP
- Obradu poziva prema datotečnom sustavu, mrežama i drugoj vanjskoj pohrani teže je provjeriti
- Greške u specifikaciji, kada je kupac ili programer namjeravao jedno, ali to nije dovoljno točno opisao u tehničkoj specifikaciji.
Kao rezultat toga, program će biti verificiran i u skladu sa specifikacijom, ali će raditi nešto potpuno drugačije od onoga što su kreatori od njega očekivali.
Budući da u ovom članku uglavnom razmatram korištenje formalne verifikacije u praksi, za sada neću lupati glavom o zid, već ću izabrati sustav u kojem je algoritamska složenost i broj vanjskih poziva minimalan.
Budući da pametni ugovori najbolje odgovaraju ovim zahtjevima, izbor je pao na RIDE ugovore s Waves platforme: oni nisu Turing potpuni, a njihova maksimalna složenost je umjetno ograničena.
Ali mi ćemo ih razmotriti isključivo s tehničke strane.
Uz sve, formalna provjera bit će posebno tražena za sve ugovore: obično je nemoguće ispraviti grešku u ugovoru nakon što je pokrenut.
A cijena takvih pogrešaka može biti vrlo visoka, budući da se prilično velike količine sredstava često pohranjuju na pametnim ugovorima.
Moj simbolički virtualni stroj napisan je u PHP-u i Pythonu i koristi Z3Prover iz Microsoft Research za rješavanje rezultirajućih SMT formula.
U svojoj jezgri moćno je višetransakcijsko pretraživanje koje
omogućuje vam pronalaženje rješenja ili ranjivosti, čak i ako zahtijeva mnogo transakcija.
još , jedan od najmoćnijih simboličkih okvira za pronalaženje ranjivosti Ethereuma, dodao je ovu mogućnost tek prije nekoliko mjeseci.
Ali vrijedi napomenuti da su ether ugovori složeniji i Turing potpuniji.
PHP prevodi izvorni kod RIDE pametnog ugovora u python skriptu, u kojoj je program predstavljen kao Z3 SMT-kompatibilan sustav stanja ugovora i uvjeta za njihove prijelaze:
Sada ću detaljnije opisati što se unutra događa.
Ali prvo, nekoliko riječi o jeziku pametnih ugovora RIDE.
To je funkcionalan programski jezik temeljen na izrazima koji je po dizajnu lijen.
RIDE radi izolirano unutar blockchaina i može dohvaćati i pisati informacije iz pohrane povezane s korisničkim novčanikom.
Uz svaki novčanik možete priložiti RIDE ugovor, a rezultat izvršenja bit će samo TRUE ili FALSE.
TRUE znači da pametni ugovor dopušta transakciju, a FALSE znači da je zabranjuje.
Jednostavan primjer: skripta može zabraniti prijenos ako je saldo novčanika manji od 100.
Kao primjer uzet ću istog Vuka, Kozu i Kupus, ali već predstavljene u obliku pametnog ugovora.
Korisnik neće moći povući novac iz novčanika na kojem je ugovor raspoređen 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će varijable Boolean 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 opis sustava u Pythonu.
Podaci su omotani u petlju, gdje varijable za pohranu dobivaju indeks i, varijable transakcije indeks i + 1, a varijable s izrazima postavljaju pravila za prijelaz iz prethodnog stanja u sljedeće.
Ovo je samo srce našeg virtualnog stroja, koji pruža tražilicu za više transakcija.
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] )
Uvjeti su razvrstani i umetnuti u predložak skripte dizajniran za opisivanje SMT sustava u Pythonu.
Prazan predložak
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 zadnje stanje u cijelom lancu vrijede pravila koja su navedena u odjeljku transakcije prijenosa.
To znači da će Z3Prover tražiti upravo takve skupove uvjeta koji će u konačnici omogućiti povlačenje sredstava iz ugovora.
Kao rezultat toga, automatski dobivamo potpuno funkcionalan SMT model našeg ugovora.
Vidite da je vrlo sličan modelu iz mog prethodnog članka, koji sam ručno sastavio.
Dovrš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 pokretanja, Z3Prover rješava pametni ugovor i pruža nam lanac transakcija koji će nam omogućiti povlačenje sredstava:
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 trajektu, možete eksperimentirati s 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
}
Budući da je ovo prva verzija, sintaksa je vrlo ograničena i može biti pogrešaka.
U sljedećim člancima planiram pokriti daljnji razvoj VM-a i pokazati kako uz njegovu pomoć možete kreirati formalno verificirane pametne ugovore, a ne samo rješavati ih.
Virtualni stroj znakova dostupan je na
Nakon što sredim izvorni kod simboličkog VM-a i tamo dodam komentare, planiram ga objaviti na GitHubu za besplatan pristup.
Izvor: www.habr.com