Muodollinen varmennus on yhden ohjelman tai algoritmin todentamista käyttämällä toista.
Tämä on yksi tehokkaimmista menetelmistä, jonka avulla voit löytää kaikki ohjelman haavoittuvuudet tai todistaa, että niitä ei ole olemassa.
Tarkempi kuvaus muodollisesta todentamisesta on nähtävissä esimerkissä ongelman ratkaisusta edellisessä artikkelissani.
Tässä artikkelissa siirryn ongelmien muodollisesta todentamisesta ohjelmiin ja kuvailen miten
kuinka ne voidaan muuntaa automaattisesti muodollisiksi sääntöjärjestelmiksi.
Tätä varten kirjoitin oman analogin virtuaalikoneesta käyttämällä symbolisia periaatteita.
Se jäsentää ohjelmakoodin ja kääntää sen yhtälöjärjestelmäksi (SMT), joka voidaan jo ratkaista ohjelmallisesti.
Koska tiedot symbolisista laskelmista esitetään Internetissä melko hajanaisesti,
Kerron lyhyesti, mikä se on.
Symbolinen laskenta on tapa suorittaa ohjelma samanaikaisesti useilla tiedoilla ja se on muodollisen ohjelman varmentamisen päätyökalu.
Voimme esimerkiksi asettaa syöttöehdot, joissa ensimmäinen argumentti voi saada minkä tahansa positiivisen arvon, toinen negatiivinen, kolmas nolla ja lähtöargumentti esimerkiksi 42.
Symboliset laskelmat yhdessä ajossa antavat meille vastauksen siihen, onko mahdollista saada haluttu tulos ja esimerkki joukosta tällaisia syöttöparametreja. Tai todiste siitä, ettei tällaisia parametreja ole.
Lisäksi voimme asettaa syöttöargumentit kaikkiin mahdollisiin ja valita vain lähtöargumentit, esimerkiksi järjestelmänvalvojan salasanan.
Tässä tapauksessa löydämme kaikki ohjelman haavoittuvuudet tai saamme todisteen järjestelmänvalvojan salasanan turvallisuudesta.
Voidaan huomata, että ohjelman klassinen suoritus tietyllä syötedatalla on symbolisen suorituksen erikoistapaus.
Siksi hahmoni VM voi toimia myös tavallisen virtuaalikoneen emulointitilassa.
Edellisen artikkelin kommenteista löytyy reilua kritiikkiä muodollista verifiointia kohtaan ja keskustelua sen heikkouksista.
Tärkeimmät ongelmat ovat:
- Kombinatorinen räjähdys, koska muodollinen verifiointi päättyy lopulta P=NP:hen
- Kutsujen käsittely tiedostojärjestelmään, verkkoihin ja muuhun ulkoiseen tallennustilaan on vaikeampi varmistaa
- Selvityksen vikoja, kun asiakas tai ohjelmoija aikoi yhtä asiaa, mutta ei kuvaillut sitä riittävän tarkasti teknisessä eritelmässä.
Seurauksena on, että ohjelma varmistetaan ja täyttää vaatimukset, mutta se tekee jotain täysin erilaista kuin mitä tekijät siltä odottivat.
Koska tässä artikkelissa pohdin lähinnä muodollisen todentamisen käyttöä käytännössä, en toistaiseksi hakkaa päätäni seinään, vaan valitsen järjestelmän, jossa algoritminen monimutkaisuus ja ulkopuheluiden määrä ovat minimaaliset.
Koska älykkäät sopimukset sopivat parhaiten näihin vaatimuksiin, valinta osui Waves-alustan RIDE-sopimuksiin: ne eivät ole Turingin valmiita, ja niiden maksimaalinen monimutkaisuus on keinotekoisesti rajoitettu.
Mutta tarkastelemme niitä yksinomaan tekniseltä puolelta.
Kaiken lisäksi muodollinen todentaminen tulee olemaan erityisen kysyntää kaikissa sopimuksissa: sopimusvirhettä on yleensä mahdotonta korjata sen käynnistämisen jälkeen.
Ja tällaisten virheiden kustannukset voivat olla erittäin korkeat, koska älykkäisiin sopimuksiin tallennetaan usein melko suuria varoja.
Symbolinen virtuaalikoneeni on kirjoitettu PHP:llä ja Pythonilla, ja se käyttää Microsoft Researchin Z3Proveria ratkaistakseen tuloksena olevat SMT-kaavat.
Sen ytimessä on tehokas monitapahtumahaku, joka
avulla voit löytää ratkaisuja tai haavoittuvuuksia, vaikka se vaatisi monia tapahtumia.
Jopa , joka on yksi tehokkaimmista symbolisista kehyksistä Ethereumin haavoittuvuuksien löytämiseksi, lisäsi tämän ominaisuuden vasta muutama kuukausi sitten.
Mutta on syytä huomata, että eetterisopimukset ovat monimutkaisempia ja Turing täydellisempiä.
PHP kääntää RIDE-älysopimuksen lähdekoodin python-skriptiksi, jossa ohjelma esitetään Z3 SMT -yhteensopivana sopimustilojen ja niiden siirtymien ehtojen järjestelmänä:
Nyt kuvailen tarkemmin mitä sisällä tapahtuu.
Mutta ensin muutama sana RIDE-älykkäästä sopimuskielestä.
Se on toiminnallinen ja ilmaisupohjainen ohjelmointikieli, joka on rakenteeltaan laiska.
RIDE toimii erillään lohkoketjussa ja voi hakea ja kirjoittaa tietoja käyttäjän lompakkoon linkitetystä tallennustilasta.
Voit liittää RIDE-sopimuksen jokaiseen lompakkoon, ja suorituksen tulos on vain TOSI tai EPÄTOSI.
TOSI tarkoittaa, että älykäs sopimus sallii tapahtuman, ja EPÄTOSI tarkoittaa, että se estää sen.
Yksinkertainen esimerkki: komentosarja voi estää siirron, jos lompakon saldo on alle 100.
Esimerkkinä otan saman suden, vuohen ja kaalin, mutta ne on jo esitetty älysopimuksen muodossa.
Käyttäjä ei voi nostaa rahaa lompakosta, johon sopimus on sijoitettu, ennen kuin hän on lähettänyt kaikki toiselle puolelle.
#Извлекаем положение всех объектов из блокчейна
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 poimii ensin kaikki muuttujat älykkäästä sopimuksesta avaimien ja vastaavan Boolen lausekemuuttujan muodossa.
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
Sitten PHP muuntaa ne Z3Prover SMT -yhteensopivaksi järjestelmäkuvaukseksi Pythonissa.
Data kääritään silmukkaan, jossa tallennusmuuttujat saavat indeksin i, tapahtumamuuttujat indeksi i + 1 ja muuttujat lausekkeineen asettavat säännöt siirtymiselle edellisestä tilasta seuraavaan.
Tämä on virtuaalikoneemme ydin, joka tarjoaa usean tapahtuman hakukoneen.
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] )
Ehdot lajitellaan ja lisätään komentosarjamalliin, joka on suunniteltu kuvaamaan Pythonin SMT-järjestelmää.
Tyhjä malli
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()
Koko ketjun viimeiseen tilaan sovelletaan siirtotapahtuma-osiossa määritettyjä sääntöjä.
Tämä tarkoittaa, että Z3Prover etsii juuri sellaisia ehtoja, jotka lopulta mahdollistavat varojen poistamisen sopimuksesta.
Tämän seurauksena saamme automaattisesti sopimuksemme täysin toimivan SMT-mallin.
Voit nähdä, että se on hyvin samanlainen kuin edellisen artikkelini malli, jonka olen laatinut manuaalisesti.
Valmis malli
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()
Lanseerauksen jälkeen Z3Prover ratkaisee älykkään sopimuksen ja tarjoaa meille tapahtumaketjun, jonka avulla voimme nostaa varoja:
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
Lauttasopimuksen lisäksi voit kokeilla omia sopimuksia tai kokeilla tätä yksinkertaista esimerkkiä, joka ratkeaa kahdella kaupalla.
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
}
Koska tämä on ensimmäinen versio, syntaksi on hyvin rajoitettu ja siinä voi olla virheitä.
Seuraavissa artikkeleissa aion käsitellä VM:n jatkokehitystä ja näyttää, kuinka voit luoda sen avulla virallisesti vahvistettuja älykkäitä sopimuksia, ei vain ratkaista niitä.
Hahmon virtuaalikone on saatavilla osoitteessa
Kun olen laittanut symbolisen virtuaalikoneen lähdekoodin järjestykseen ja lisännyt siihen kommentteja, aion laittaa sen GitHubiin ilmaiseksi.
Lähde: will.com