Formala konfirmo estas la konfirmo de unu programo aŭ algoritmo uzante alian.
Ĉi tiu estas unu el la plej potencaj metodoj, kiuj permesas vin trovi ĉiujn vundeblecojn en programo aŭ pruvi, ke ili ne ekzistas.
Pli detala priskribo de formala konfirmo povas esti vidita en la ekzemplo de solvado de la problemo de en mia antaŭa artikolo.
En ĉi tiu artikolo mi transiras de formala konfirmo de problemoj al programoj kaj priskribas kiel
kiel ili povas esti konvertitaj en formalajn regulsistemojn aŭtomate.
Por fari tion, mi skribis mian propran analogon de virtuala maŝino, uzante simbolajn principojn.
Ĝi analizas la programkodon kaj tradukas ĝin en sistemon de ekvacioj (SMT), kiu jam povas esti solvita programe.
Ĉar informoj pri simbolaj kalkuloj estas prezentitaj en Interreto sufiĉe fragmente,
Mi mallonge priskribos kio ĝi estas.
Simbola komputado estas maniero samtempe efektivigi programon sur larĝa gamo de datumoj kaj estas la ĉefa ilo por formala programkontrolo.
Ekzemple, ni povas agordi enigkondiĉojn kie la unua argumento povas preni iujn ajn pozitivajn valorojn, la duan negativan, la trian nulon, kaj la eligargumenton, ekzemple, 42.
Simbolaj kalkuloj en unu kuro donos al ni la respondon ĉu estas eble por ni akiri la deziratan rezulton kaj ekzemplon de aro de tiaj eniga parametroj. Aŭ pruvo, ke tiaj parametroj ne ekzistas.
Plie, ni povas agordi la enigajn argumentojn al ĉiuj eblaj, kaj elekti nur la eligaĵojn, ekzemple la pasvorton de administranto.
En ĉi tiu kazo, ni trovos ĉiujn vundeblecojn de la programo aŭ ricevos pruvon, ke la pasvorto de la administranto estas sekura.
Oni povas rimarki, ke la klasika ekzekuto de programo kun specifaj enigdatenoj estas speciala kazo de simbola ekzekuto.
Sekve, mia karaktero VM ankaŭ povas funkcii en imita reĝimo de norma virtuala maŝino.
En la komentoj al la antaŭa artikolo oni povas trovi justan kritikon de formala konfirmo kun diskuto pri ĝiaj malfortoj.
La ĉefaj problemoj estas:
- Kombina eksplodo, ĉar formala konfirmo finfine venas malsupren al P=NP
- Prilaborado de vokoj al la dosiersistemo, retoj kaj alia ekstera stokado estas pli malfacile kontroli
- Cimoj en la specifo, kiam la kliento aŭ programisto celis unu aferon, sed ne priskribis ĝin sufiĉe precize en la teknika specifo.
Kiel rezulto, la programo estos kontrolita kaj konformas al la specifo, sed faros ion tute alian ol kion la kreintoj atendis de ĝi.
Ĉar en ĉi tiu artikolo mi ĉefe pripensas la uzon de formala konfirmo en la praktiko, mi nun ne batos mian kapon kontraŭ la muron, kaj elektos sistemon kie la algoritma komplekseco kaj la nombro da eksteraj vokoj estas minimumaj.
Ĉar inteligentaj kontraktoj plej konvenas al ĉi tiuj postuloj, la elekto falis sur RIDE-kontraktoj de la platformo Waves: ili ne estas Turing kompletaj, kaj ilia maksimuma komplekseco estas artefarite limigita.
Sed ni konsideros ilin ekskluzive de la teknika flanko.
Aldone al ĉio, formala konfirmo estos precipe postulata por iuj kontraktoj: estas kutime neeble korekti kontraktan eraron post kiam ĝi estis lanĉita.
Kaj la kosto de tiaj eraroj povas esti tre alta, ĉar sufiĉe grandaj kvantoj da financo ofte estas stokitaj en inteligentaj kontraktoj.
Mia simbola virtuala maŝino estas skribita en PHP kaj Python, kaj uzas Z3Prover de Microsoft Research por solvi la rezultajn SMT-formulojn.
Ĉe ĝia kerno estas potenca mult-transakcia serĉo, kiu
permesas vin trovi solvojn aŭ vundeblecojn, eĉ se ĝi postulas multajn transakciojn.
Eĉ la , Unu el la plej potencaj simbolaj kadroj por trovi Ethereum-vundeblecojn, nur aldonis ĉi tiun kapablon antaŭ kelkaj monatoj.
Sed indas noti, ke eteraj kontraktoj estas pli kompleksaj kaj Turing kompleta.
PHP tradukas la fontkodon de la inteligenta kontrakto RIDE en python-skripton, en kiu la programo estas prezentita kiel Z3-SMT-kongrua sistemo de kontraktoŝtatoj kaj kondiĉoj por iliaj transiroj:
Nun mi pli detale priskribos kio okazas interne.
Sed unue, kelkajn vortojn pri la inteligenta kontraktolingvo RIDE.
Ĝi estas funkcia kaj esprim-bazita programlingvo kiu estas maldiligenta laŭ dezajno.
RIDE funkcias izole ene de la blokĉeno kaj povas preni kaj skribi informojn de stokado ligita al la monujo de la uzanto.
Vi povas kunligi RIDE-kontrakton al ĉiu monujo, kaj la rezulto de ekzekuto estos nur VERA aŭ FALSA.
VERA signifas, ke la inteligenta kontrakto permesas la transakcion, kaj FALSA signifas, ke ĝi malpermesas ĝin.
Simpla ekzemplo: skripto povas malpermesi translokigon se la monujo-saldo estas malpli ol 100.
Kiel ekzemplon, mi prenos la samajn Lupon, Kapron kaj Brasikon, sed jam prezentitajn en formo de inteligenta kontrakto.
La uzanto ne povos eltiri monon de la monujo sur kiu la kontrakto estas deplojita ĝis li sendis ĉiujn al la alia flanko.
#Извлекаем положение всех объектов из блокчейна
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 unue ĉerpas ĉiujn variablojn de la inteligenta kontrakto en la formo de iliaj ŝlosiloj kaj la responda Bulea esprimo variablo.
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 tiam konvertas ilin en Z3Prover SMT-kongruan sisteman priskribon en Python.
La datumoj estas envolvitaj en buklo, kie stokaj variabloj ricevas indekson i, transakciaj variabloj indekson i + 1, kaj variabloj kun esprimoj starigas la regulojn por transiro de la antaŭa stato al la sekva.
Ĉi tio estas la koro mem de nia virtuala maŝino, kiu provizas mult-transakcian serĉan mekanismon.
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] )
La kondiĉoj estas ordigitaj kaj enmetitaj en skriptŝablonon desegnita por priskribi la SMT-sistemon en Python.
Blanka ŝablono
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()
Por la lasta ŝtato en la tuta ĉeno, la reguloj specifitaj en la transakcia sekcio estas aplikataj.
Ĉi tio signifas, ke Z3Prover serĉos ĝuste tiajn arojn de kondiĉoj, kiuj finfine permesos retiriĝi financojn de la kontrakto.
Kiel rezulto, ni aŭtomate ricevas plene funkcian SMT-modelon de nia kontrakto.
Vi povas vidi, ke ĝi estas tre simila al la modelo de mia antaŭa artikolo, kiun mi kompilis permane.
Kompletigita ŝablono
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()
Post lanĉo, Z3Prover solvas la inteligentan kontrakton kaj provizas al ni ĉenon de transakcioj, kiuj permesos al ni eltiri financojn:
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
Krom la pramkontrakto, vi povas eksperimenti kun viaj propraj kontraktoj aŭ provi ĉi tiun simplan ekzemplon, kiu estas solvita en 2 transakcioj.
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
}
Ĉar ĉi tiu estas la unua versio, la sintakso estas tre limigita kaj povas esti eraroj.
En la sekvaj artikoloj, mi planas kovri la pluan disvolviĝon de la VM, kaj montri kiel vi povas krei formale kontrolitajn inteligentajn kontraktojn kun ĝia helpo, kaj ne nur solvi ilin.
La karaktero virtuala maŝino haveblas ĉe
Post meti la fontkodon de la simbola VM en ordo kaj aldoni komentojn tie, mi planas meti ĝin sur GitHub por libera aliro.
fonto: www.habr.com