Oficialus patikrinimas yra vienos programos ar algoritmo patikrinimas naudojant kitą.
Tai vienas iš galingiausių metodų, leidžiančių rasti visas programos spragas arba įrodyti, kad jų nėra.
Išsamesnį formalaus patikrinimo aprašymą galima pamatyti problemos sprendimo pavyzdyje mano ankstesniame straipsnyje.
Šiame straipsnyje aš pereinu nuo formalaus problemų patikrinimo prie programų ir aprašysiu, kaip tai padaryti
kaip jas galima automatiškai konvertuoti į formalias taisyklių sistemas.
Norėdami tai padaryti, aš parašiau savo virtualios mašinos analogą, naudodamas simbolinius principus.
Jis analizuoja programos kodą ir paverčia jį lygčių sistema (SMT), kurią jau galima išspręsti programiškai.
Kadangi informacija apie simbolinius skaičiavimus internete pateikiama gana fragmentiškai,
Trumpai aprašysiu, kas tai yra.
Simbolinis skaičiavimas yra būdas vienu metu vykdyti programą įvairiems duomenims ir yra pagrindinis formalaus programos patikrinimo įrankis.
Pavyzdžiui, galime nustatyti įvesties sąlygas, kai pirmasis argumentas gali turėti bet kokias teigiamas reikšmes, antrasis neigiamas, trečiasis nulis, o išvesties argumentas, pavyzdžiui, 42.
Simboliniai skaičiavimai vienu metu suteiks atsakymą, ar įmanoma gauti norimą rezultatą, ir tokių įvesties parametrų rinkinio pavyzdį. Arba įrodymas, kad tokių parametrų nėra.
Be to, galime nustatyti visus įmanomus įvesties argumentus, o pasirinkti tik išvesties, pavyzdžiui, administratoriaus slaptažodį.
Tokiu atveju rasime visas programos spragas arba gausime įrodymą, kad administratoriaus slaptažodis yra saugus.
Galima pastebėti, kad klasikinis programos vykdymas su konkrečiais įvesties duomenimis yra ypatingas simbolinio vykdymo atvejis.
Todėl mano veikėjas VM taip pat gali dirbti standartinės virtualios mašinos emuliacijos režimu.
Ankstesnio straipsnio komentaruose galima rasti teisingos formalaus patikrinimo kritikos, aptariant jos trūkumus.
Pagrindinės problemos yra šios:
- Kombinatorinis sprogimas, nes formalus patikrinimas galiausiai yra P = NP
- Sunkiau patikrinti skambučių į failų sistemą, tinklus ir kitą išorinę saugyklą apdorojimą
- Klaidos specifikacijoje, kai užsakovas ar programuotojas numatė vieną dalyką, bet nepakankamai tiksliai to apibūdino techninėje specifikacijoje.
Dėl to programa bus patikrinta ir atitiks specifikaciją, tačiau padarys kažką visiškai kitokio, nei iš jos tikėjosi kūrėjai.
Kadangi šiame straipsnyje daugiausia svarstau apie formalaus patikrinimo panaudojimą praktikoje, kol kas nedaužysiu galvos į sieną, o rinksiuosi tokią sistemą, kurioje algoritminis sudėtingumas ir išorinių skambučių skaičius būtų minimalus.
Kadangi išmaniosios sutartys geriausiai atitinka šiuos reikalavimus, pasirinkimas teko RIDE sutartims iš „Waves“ platformos: jos nėra baigtos „Turing“, o jų maksimalus sudėtingumas yra dirbtinai apribotas.
Tačiau mes juos apsvarstysime tik iš techninės pusės.
Be to, bet kokioms sutartims ypač reikės formalaus patikrinimo: sutarties klaidos po jos paskelbimo ištaisyti dažniausiai neįmanoma.
Ir tokių klaidų kaina gali būti labai didelė, nes išmaniosiose sutartyse dažnai saugomos gana didelės lėšų sumos.
Mano simbolinė virtuali mašina yra parašyta PHP ir Python kalbomis ir naudoja Z3Prover iš Microsoft Research, kad išspręstų gautas SMT formules.
Jos esmė yra galinga kelių operacijų paieška, kuri
leidžia rasti sprendimus ar pažeidžiamumą, net jei tam reikia atlikti daug operacijų.
Net , viena iš galingiausių simbolinių sistemų Ethereum pažeidžiamumui rasti, šią galimybę pridėjo tik prieš kelis mėnesius.
Tačiau verta paminėti, kad eterio sutartys yra sudėtingesnės, o Turingo – išsamesnės.
PHP verčia RIDE išmaniosios sutarties šaltinio kodą į python scenarijų, kuriame programa pateikiama kaip su Z3 SMT suderinama sutarties būsenų ir jų perėjimų sąlygų sistema:
Dabar išsamiau aprašysiu, kas vyksta viduje.
Tačiau pirmiausia keli žodžiai apie RIDE išmaniąją sutarties kalbą.
Tai funkcinė ir išraiškomis pagrįsta programavimo kalba, kurios dizainas yra tingus.
RIDE veikia atskirai blokų grandinėje ir gali nuskaityti bei įrašyti informaciją iš saugyklos, susietos su vartotojo pinigine.
Prie kiekvienos piniginės galite pridėti RIDE sutartį, o vykdymo rezultatas bus tik TEISINGAS arba NETIESAS.
TRUE reiškia, kad išmanioji sutartis leidžia atlikti operaciją, o FALSE reiškia, kad ji tai draudžia.
Paprastas pavyzdys: scenarijus gali uždrausti pervedimą, jei piniginės likutis yra mažesnis nei 100.
Kaip pavyzdį paimsiu tą patį Vilką, Ožką ir Kopūstą, bet jau pateiktą išmaniosios sutarties forma.
Vartotojas negalės atsiimti pinigų iš piniginės, kurioje yra sudaryta sutartis, kol nenusiųs visų į kitą pusę.
#Извлекаем положение всех объектов из блокчейна
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 pirmiausia ištraukia visus išmaniosios sutarties kintamuosius jų raktų ir atitinkamo Būlio išraiškos kintamojo pavidalu.
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
Tada PHP konvertuoja juos į su Z3Prover SMT suderinamą sistemos aprašą Python.
Duomenys suvynioti į kilpą, kurioje saugojimo kintamieji gauna indeksą i, operacijų kintamieji indeksą i + 1, o kintamieji su išraiškomis nustato perėjimo iš ankstesnės būsenos į kitą taisykles.
Tai pati mūsų virtualios mašinos širdis, kuri suteikia kelių operacijų paieškos variklį.
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] )
Sąlygos surūšiuojamos ir įterpiamos į scenarijaus šabloną, skirtą SMT sistemai apibūdinti Python.
Tuščias šablonas
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()
Paskutinei visos grandinės būsenai taikomos taisyklės, nurodytos pervedimo operacijos skyriuje.
Tai reiškia, kad „Z3Prover“ ieškos būtent tokių sąlygų, kurios galiausiai leis atsiimti lėšas iš sutarties.
Dėl to automatiškai gauname visiškai funkcionalų mūsų sutarties SMT modelį.
Matote, kad jis labai panašus į modelį iš ankstesnio mano straipsnio, kurį sudariau rankiniu būdu.
Užbaigtas šablonas
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()
Po paleidimo „Z3Prover“ išsprendžia išmaniąją sutartį ir pateikia mums operacijų grandinę, kuri leis mums atsiimti lėšas:
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
Be kelto sutarties, galite eksperimentuoti su savo sutartimis arba išbandyti šį paprastą pavyzdį, kuris išsprendžiamas 2 sandoriais.
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
}
Kadangi tai pati pirmoji versija, sintaksė yra labai ribota ir gali būti klaidų.
Tolesniuose straipsniuose planuoju apžvelgti tolesnę VM plėtrą ir parodyti, kaip jos pagalba galima sukurti formaliai patikrintas išmaniąsias sutartis, o ne tik jas išspręsti.
Simbolių virtualioji mašina pasiekiama adresu
Sutvarkęs simbolinės VM šaltinio kodą ir pridėjęs ten komentarus, planuoju jį įdėti į GitHub, kad būtų galima nemokamai pasiekti.
Šaltinis: www.habr.com