Ametlik kinnitamine on ühe programmi või algoritmi kontrollimine teise programmi või algoritmi abil.
See on üks võimsamaid meetodeid, mis võimaldab leida programmis kõik haavatavused või tõestada, et neid pole.
Formaalse kontrolli täpsemat kirjeldust võib näha probleemi lahendamise näites minu eelmises artiklis.
Selles artiklis liigun probleemide formaalse kontrollimise juurest programmide juurde ja kirjeldan, kuidas
kuidas saab neid automaatselt teisendada formaalseteks reeglisüsteemideks.
Selleks kirjutasin oma virtuaalmasina analoogi, kasutades selleks sümboolseid põhimõtteid.
See parsib programmi koodi ja tõlgib selle võrrandisüsteemiks (SMT), mida saab juba programmiliselt lahendada.
Kuna info sümboolsete arvutuste kohta on Internetis esitatud üsna fragmentaarselt,
Kirjeldan lühidalt, mis see on.
Sümboolne arvutamine on viis programmi samaaegseks käivitamiseks suurel hulgal andmetel ja see on peamine tööriist programmi ametlikuks kontrollimiseks.
Näiteks saame määrata sisendtingimused, kus esimene argument võib võtta mis tahes positiivseid väärtusi, teine negatiivne, kolmas null ja väljundargument, näiteks 42.
Ühe käiguga sümboolsed arvutused annavad meile vastuse, kas meil on võimalik soovitud tulemust saada, ja näite selliste sisendparameetrite komplektist. Või tõend, et selliseid parameetreid pole.
Lisaks saame määrata sisendargumendid kõigile võimalikele ja valida ainult väljundargumendid, näiteks administraatori parooli.
Sel juhul leiame kõik programmi haavatavused või saame tõendi, et administraatori parool on turvaline.
Võib märkida, et konkreetsete sisendandmetega programmi klassikaline täitmine on sümboolse täitmise erijuht.
Seetõttu saab minu tegelaskuju VM töötada ka tavalise virtuaalmasina emuleerimisrežiimis.
Eelmise artikli kommentaaridest võib leida õiglast kriitikat formaalse kontrollimise kohta koos selle nõrkade külgede aruteluga.
Peamised probleemid on järgmised:
- Kombinatoorne plahvatus, kuna formaalne kontrollimine taandub lõpuks P=NP-le
- Failisüsteemi, võrkude ja muu välise salvestusruumi kõnede töötlemist on keerulisem kontrollida
- Vead spetsifikatsioonis, kui klient või programmeerija kavatses üht asja, kuid ei kirjeldanud seda tehnilises kirjelduses piisavalt täpselt.
Selle tulemusena kontrollitakse programmi ja see vastab spetsifikatsioonidele, kuid teeb midagi täiesti erinevat sellest, mida loojad sellelt ootasid.
Kuna käesolevas artiklis pean silmas peamiselt formaalse verifitseerimise kasutamist praktikas, siis ma praegu pead vastu seina ei löö, vaid valin süsteemi, kus algoritmiline keerukus ja väliskõnede arv on minimaalne.
Kuna nutikad lepingud vastavad nendele nõuetele kõige paremini, langes valik Waves platvormi RIDE lepingutele: need ei ole Turingi komplekteeritud ja nende maksimaalne keerukus on kunstlikult piiratud.
Kuid me käsitleme neid eranditult tehnilisest küljest.
Lisaks kõigele on kõigi lepingute puhul eriti nõutud formaalne kontrollimine: lepinguviga on pärast selle käivitamist tavaliselt võimatu parandada.
Ja selliste vigade maksumus võib olla väga kõrge, kuna nutikatele lepingutele salvestatakse sageli üsna suuri summasid.
Minu sümboolne virtuaalmasin on kirjutatud PHP ja Python keeles ning kasutab saadud SMT valemite lahendamiseks Microsoft Researchi Z3Proverit.
Selle tuumaks on võimas mitut tehingut hõlmav otsing, mis
võimaldab leida lahendusi või turvaauke, isegi kui see nõuab palju tehinguid.
Isegi , üks võimsamaid sümboolseid raamistikke Ethereumi haavatavuste leidmiseks, lisas selle võimaluse alles paar kuud tagasi.
Kuid väärib märkimist, et eetrilepingud on keerukamad ja Turing on täielikum.
PHP tõlgib RIDE nutika lepingu lähtekoodi pythoni skriptiks, milles programm on esitatud Z3 SMT-ga ühilduva lepinguolekute ja nende ülemineku tingimuste süsteemina:
Nüüd kirjeldan täpsemalt, mis sees toimub.
Aga kõigepealt paar sõna RIDE nutika lepingukeele kohta.
See on funktsionaalne ja väljenduspõhine programmeerimiskeel, mis on disainilt laisk.
RIDE töötab plokiahelas isoleeritult ning saab kasutaja rahakotiga seotud salvestusruumist teavet hankida ja kirjutada.
Igale rahakotile saate lisada RIDE lepingu ja täitmise tulemus on ainult TÕENE või VÄÄR.
TRUE tähendab, et nutikas leping võimaldab tehingut ja FALSE tähendab, et see keelab selle.
Lihtne näide: skript võib ülekande keelata, kui rahakoti saldo on alla 100.
Näitena toon sama Hundi, Kitse ja Kapsa, kuid juba targa lepingu vormis esitatud.
Kasutaja ei saa rahakotist, millele leping on paigutatud, raha välja võtta enne, kui ta on kõik teisele poole saatnud.
#Извлекаем положение всех объектов из блокчейна
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 ekstraheerib esmalt kõik muutujad nutikast lepingust nende võtmete ja vastava Boole'i avaldise muutuja kujul.
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
Seejärel teisendab PHP need Pythonis Z3Prover SMT-ga ühilduvaks süsteemikirjelduseks.
Andmed mähitakse tsüklisse, kus salvestusmuutujad saavad indeksi i, tehingumuutujad indeksi i + 1 ja avaldistega muutujad määravad reeglid eelmisest olekust järgmisse üleminekuks.
See on meie virtuaalmasina süda, mis pakub mitut tehingut hõlmavat otsingumootorit.
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] )
Tingimused sorteeritakse ja sisestatakse skriptimalli, mis on loodud Pythonis SMT-süsteemi kirjeldamiseks.
Tühi mall
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()
Kogu ahela viimase oleku jaoks rakendatakse reegleid, mis on määratud ülekandetehingu jaotises.
See tähendab, et Z3Prover otsib just selliseid tingimuste kogumeid, mis lõpuks võimaldavad lepingust raha välja võtta.
Selle tulemusena saame automaatselt meie lepingu täielikult toimiva SMT mudeli.
Näete, et see on väga sarnane minu eelmise artikli mudeliga, mille koostasin käsitsi.
Valmis mall
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ärast käivitamist lahendab Z3Prover nutika lepingu ja pakub meile tehingute ahelat, mis võimaldab meil raha välja võtta:
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
Lisaks parvlaevalepingule saab katsetada oma lepingutega või proovida seda lihtsat näidet, mis lahendatakse 2 tehinguga.
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
}
Kuna see on kõige esimene versioon, on süntaks väga piiratud ja võib esineda vigu.
Järgnevates artiklites kavatsen käsitleda VM-i edasist arengut ning näidata, kuidas selle abil saab luua formaalselt kontrollitud nutilepinguid, mitte ainult neid lahendada.
Tegelaste virtuaalmasin on saadaval aadressil
Peale sümboolse VM lähtekoodi järjekorda seadmist ja sinna kommentaaride lisamist plaanin selle tasuta ligipääsuks GitHubisse panna.
Allikas: www.habr.com