Verifikimi formal është verifikimi i një programi ose algoritmi duke përdorur një tjetër.
Kjo është një nga metodat më të fuqishme që ju lejon të gjeni të gjitha dobësitë në një program ose të provoni se ato nuk ekzistojnë.
Një përshkrim më i detajuar i verifikimit zyrtar mund të shihet në shembullin e zgjidhjes së problemit të në artikullin tim të mëparshëm.
Në këtë artikull unë kaloj nga verifikimi zyrtar i problemeve në programe dhe përshkruaj se si
si mund të shndërrohen automatikisht në sisteme të rregullave formale.
Për ta bërë këtë, unë shkrova analogun tim të një makine virtuale, duke përdorur parime simbolike.
Ai analizon kodin e programit dhe e përkthen atë në një sistem ekuacionesh (SMT), i cili tashmë mund të zgjidhet në mënyrë programore.
Meqenëse informacioni rreth llogaritjeve simbolike paraqitet në internet në mënyrë mjaft fragmentare,
Unë do të përshkruaj shkurtimisht se çfarë është.
Llogaritja simbolike është një mënyrë për të ekzekutuar njëkohësisht një program në një gamë të gjerë të dhënash dhe është mjeti kryesor për verifikimin formal të programit.
Për shembull, ne mund të vendosim kushte hyrëse ku argumenti i parë mund të marrë çdo vlerë pozitive, i dyti negativ, i treti zero dhe argumenti i daljes, për shembull, 42.
Llogaritjet simbolike në një drejtim do të na japin përgjigjen nëse është e mundur që ne të marrim rezultatin e dëshiruar dhe një shembull të një grupi parametrash të tillë hyrës. Ose dëshmi se nuk ka parametra të tillë.
Për më tepër, ne mund të vendosim argumentet hyrëse për të gjitha ato të mundshme dhe të zgjedhim vetëm ato dalëse, për shembull, fjalëkalimin e administratorit.
Në këtë rast, ne do të gjejmë të gjitha dobësitë e programit ose do të marrim prova që fjalëkalimi i administratorit është i sigurt.
Mund të vërehet se ekzekutimi klasik i një programi me të dhëna hyrëse specifike është një rast i veçantë i ekzekutimit simbolik.
Prandaj, karakteri im VM mund të funksionojë gjithashtu në modalitetin emulues të një makine virtuale standarde.
Në komentet e artikullit të mëparshëm mund të gjesh kritika të drejta të verifikimit formal me një diskutim të dobësive të tij.
Problemet kryesore janë:
- Shpërthim kombinator, pasi verifikimi zyrtar përfundimisht zbret në P=NP
- Përpunimi i thirrjeve në sistemin e skedarëve, rrjetet dhe ruajtje të tjera të jashtme është më i vështirë për t'u verifikuar
- Gabimet në specifikim, kur klienti ose programuesi synonte një gjë, por nuk e përshkruante me saktësi të mjaftueshme në specifikimin teknik.
Si rezultat, programi do të verifikohet dhe do të përputhet me specifikimet, por do të bëjë diçka krejtësisht të ndryshme nga ajo që krijuesit prisnin prej tij.
Meqenëse në këtë artikull po shqyrtoj kryesisht përdorimin e verifikimit zyrtar në praktikë, tani për tani nuk do të godas kokën pas murit dhe do të zgjedh një sistem ku kompleksiteti algoritmik dhe numri i thirrjeve të jashtme janë minimale.
Meqenëse kontratat inteligjente i përshtaten më së miri këtyre kërkesave, zgjedhja ra në kontratat RIDE nga platforma Waves: ato nuk janë të kompletuara Turing dhe kompleksiteti i tyre maksimal është i kufizuar artificialisht.
Por ne do t'i konsiderojmë ato ekskluzivisht nga ana teknike.
Për më tepër, për çdo kontratë verifikimi zyrtar do të jetë veçanërisht i kërkuar: zakonisht është e pamundur të korrigjohet një gabim i kontratës pasi të jetë nisur.
Dhe kostoja e gabimeve të tilla mund të jetë shumë e lartë, pasi shuma mjaft të mëdha fondesh shpesh ruhen në kontrata inteligjente.
Makina ime simbolike virtuale është shkruar në PHP dhe Python dhe përdor Z3Prover nga Microsoft Research për të zgjidhur formulat SMT që rezultojnë.
Në thelbin e tij është një kërkim i fuqishëm shumë-transaksional, i cili
ju lejon të gjeni zgjidhje ose dobësi, edhe nëse kërkon shumë transaksione.
Madje , një nga kornizat simbolike më të fuqishme për gjetjen e dobësive të Ethereum, e shtoi këtë aftësi vetëm disa muaj më parë.
Por vlen të përmendet se kontratat eterike janë më komplekse dhe janë Turing të plota.
PHP përkthen kodin burimor të kontratës inteligjente RIDE në një script python, në të cilin programi paraqitet si një sistem i pajtueshëm me Z3 SMT i gjendjeve të kontratës dhe kushteve për tranzicionin e tyre:
Tani do të përshkruaj atë që po ndodh brenda në më shumë detaje.
Por së pari, disa fjalë për gjuhën e kontratës inteligjente RIDE.
Është një gjuhë programimi funksionale dhe e bazuar në shprehje që është dembel nga dizajni.
RIDE funksionon i izoluar brenda blockchain dhe mund të marrë dhe shkruajë informacion nga ruajtja e lidhur me portofolin e përdoruesit.
Ju mund të bashkëngjitni një kontratë RIDE në çdo portofol dhe rezultati i ekzekutimit do të jetë vetëm E VËRTETË ose E FALSE.
E VËRTETË do të thotë që kontrata inteligjente lejon transaksionin dhe FALSE do të thotë se e ndalon atë.
Një shembull i thjeshtë: një skenar mund të ndalojë një transferim nëse balanca e portofolit është më pak se 100.
Si shembull, unë do të marr të njëjtin Ujk, Bricjap dhe Lakër, por tashmë të paraqitur në formën e një kontrate të zgjuar.
Përdoruesi nuk do të jetë në gjendje të tërheqë para nga portofoli në të cilin është vendosur kontrata derisa të ketë dërguar të gjithë në anën tjetër.
#Извлекаем положение всех объектов из блокчейна
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 fillimisht nxjerr të gjitha variablat nga kontrata inteligjente në formën e çelësave të tyre dhe variablit përkatës të shprehjes Boolean.
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 më pas i konverton ato në një përshkrim të sistemit të pajtueshëm me Z3Prover SMT në Python.
Të dhënat mbështillen në një lak, ku variablat e ruajtjes marrin indeksin i, variablat e transaksionit indeksin i + 1 dhe variablat me shprehje vendosin rregullat për kalimin nga gjendja e mëparshme në tjetrën.
Kjo është vetë zemra e makinës sonë virtuale, e cila ofron një mekanizëm kërkimi me shumë transaksione.
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] )
Kushtet janë renditur dhe futur në një shabllon skripti të krijuar për të përshkruar sistemin SMT në Python.
Shablloni bosh
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()
Për gjendjen e fundit në të gjithë zinxhirin, zbatohen rregullat që janë të specifikuara në seksionin e transaksionit të transferimit.
Kjo do të thotë që Z3Prover do të kërkojë pikërisht grupe të tilla kushtesh që në fund të fundit do të lejojnë tërheqjen e fondeve nga kontrata.
Si rezultat, ne marrim automatikisht një model SMT plotësisht funksional të kontratës sonë.
Ju mund të shihni se është shumë i ngjashëm me modelin nga artikulli im i mëparshëm, të cilin e përpilova manualisht.
Modeli i kompletuar
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()
Pas nisjes, Z3Prover zgjidh kontratën inteligjente dhe na siguron një zinxhir transaksionesh që do të na lejojnë të tërheqim fonde:
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
Përveç kontratës së tragetit, mund të eksperimentoni me kontratat tuaja ose të provoni këtë shembull të thjeshtë, i cili zgjidhet në 2 transaksione.
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
}
Meqenëse ky është versioni i parë, sintaksa është shumë e kufizuar dhe mund të ketë gabime.
Në artikujt e mëposhtëm, unë planifikoj të mbuloj zhvillimin e mëtejshëm të VM dhe të tregoj se si mund të krijoni kontrata inteligjente të verifikuara zyrtarisht me ndihmën e tij, dhe jo vetëm t'i zgjidhni ato.
Makina virtuale e karaktereve është në dispozicion në
Pasi të vendos kodin burimor të VM-së simbolike dhe të shtoj komente atje, planifikoj ta vendos në GitHub për qasje falas.
Burimi: www.habr.com