Formell verifiering är verifiering av ett program eller en algoritm med hjälp av ett annat.
Detta är en av de mest kraftfulla metoderna som låter dig hitta alla sårbarheter i ett program eller bevisa att de inte finns.
En mer detaljerad beskrivning av formell verifiering kan ses i exemplet på att lösa problemet med i min tidigare artikel.
I den här artikeln går jag från formell verifiering av problem till program och beskriver hur
hur kan de automatiskt omvandlas till formella regelsystem.
För att göra detta skrev jag min egen analog av en virtuell maskin, med hjälp av symboliska principer.
Den analyserar programkoden och översätter den till ett system av ekvationer (SMT), som redan kan lösas programmatiskt.
Eftersom information om symboliska beräkningar presenteras på Internet ganska fragmentariskt,
Jag ska kort beskriva vad det är.
Symbolisk beräkning är ett sätt att samtidigt köra ett program på ett brett spektrum av data och är huvudverktyget för formell programverifiering.
Till exempel kan vi ställa in ingångsvillkor där det första argumentet kan ta alla positiva värden, det andra negativa, det tredje noll och utmatningsargumentet, till exempel 42.
Symboliska beräkningar i en körning kommer att ge oss svaret på om det är möjligt för oss att få det önskade resultatet och ett exempel på en uppsättning sådana ingångsparametrar. Eller bevis på att det inte finns några sådana parametrar.
Dessutom kan vi ställa in ingångsargumenten till alla möjliga, och bara välja utdata, till exempel administratörslösenordet.
I det här fallet kommer vi att hitta alla programmets sårbarheter eller få bevis på att administratörens lösenord är säkert.
Det kan noteras att den klassiska exekveringen av ett program med specifika indata är ett specialfall av symbolisk exekvering.
Därför kan min karaktärs VM också fungera i emuleringsläge för en vanlig virtuell maskin.
I kommentarerna till föregående artikel kan man hitta rättvis kritik av formell verifiering med en diskussion om dess svagheter.
Huvudproblemen är:
- Kombinatorisk explosion, eftersom formell verifiering i slutändan kommer ner på P=NP
- Att behandla samtal till filsystemet, nätverk och annan extern lagring är svårare att verifiera
- Buggar i specifikationen, när kunden eller programmeraren avsåg en sak, men inte beskrev det tillräckligt exakt i den tekniska specifikationen.
Som ett resultat kommer programmet att verifieras och följa specifikationen, men kommer att göra något helt annat än vad skaparna förväntade sig av det.
Eftersom jag i den här artikeln främst överväger användningen av formell verifiering i praktiken kommer jag inte att dunka huvudet i väggen för tillfället, utan kommer att välja ett system där den algoritmiska komplexiteten och antalet externa samtal är minimalt.
Eftersom smarta kontrakt bäst passar dessa krav föll valet på RIDE-kontrakt från Waves-plattformen: de är inte Turing kompletta, och deras maximala komplexitet är artificiellt begränsad.
Men vi kommer att överväga dem uteslutande från den tekniska sidan.
Utöver allt kommer formell verifiering att vara särskilt efterfrågad för eventuella kontrakt: det är vanligtvis omöjligt att rätta till ett kontraktsfel efter att det har lanserats.
Och kostnaden för sådana fel kan vara mycket hög, eftersom ganska stora mängder pengar ofta lagras på smarta kontrakt.
Min symboliska virtuella maskin är skriven i PHP och Python och använder Z3Prover från Microsoft Research för att lösa de resulterande SMT-formlerna.
Kärnan är en kraftfull multi-transaktionell sökning, som
låter dig hitta lösningar eller sårbarheter, även om det kräver många transaktioner.
Även , ett av de mest kraftfulla symboliska ramverken för att hitta Ethereum-sårbarheter, lade till denna funktion för några månader sedan.
Men det är värt att notera att eterkontrakt är mer komplexa och Turing kompletta.
PHP översätter källkoden för det smarta RIDE-kontraktet till ett python-skript, där programmet presenteras som ett Z3 SMT-kompatibelt system med kontraktstillstånd och villkor för deras övergångar:
Nu ska jag beskriva vad som händer inuti mer i detalj.
Men först några ord om det smarta kontraktsspråket RIDE.
Det är ett funktionellt och uttrycksbaserat programmeringsspråk som är lat till sin design.
RIDE körs isolerat inom blockkedjan och kan hämta och skriva information från lagring kopplad till användarens plånbok.
Du kan bifoga ett RIDE-kontrakt till varje plånbok, och resultatet av utförandet blir endast SANT eller FALSK.
TRUE betyder att det smarta kontraktet tillåter transaktionen, och FALSE betyder att det förbjuder det.
Ett enkelt exempel: ett skript kan förbjuda en överföring om saldot i plånboken är mindre än 100.
Som ett exempel kommer jag att ta samma varg, get och kål, men redan presenterad i form av ett smart kontrakt.
Användaren kommer inte att kunna ta ut pengar från plånboken som kontraktet är utplacerat på förrän han har skickat alla till andra sidan.
#Извлекаем положение всех объектов из блокчейна
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 extraherar först alla variabler från det smarta kontraktet i form av deras nycklar och motsvarande booleska uttrycksvariabel.
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 konverterar dem sedan till en Z3Prover SMT-kompatibel systembeskrivning i Python.
Data lindas in i en loop, där lagringsvariabler tar emot index i, transaktionsvariabler index i + 1, och variabler med uttryck sätter reglerna för övergång från föregående tillstånd till nästa.
Detta är själva hjärtat i vår virtuella maskin, som tillhandahåller en sökmotor för flera transaktioner.
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] )
Villkoren sorteras och infogas i en skriptmall utformad för att beskriva SMT-systemet i Python.
Tom 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()
För den sista staten i hela kedjan tillämpas de regler som anges i avsnittet om överföringstransaktioner.
Detta innebär att Z3Prover kommer att leta efter just sådana uppsättningar villkor som i slutändan kommer att göra det möjligt att dra pengar från kontraktet.
Som ett resultat får vi automatiskt en fullt fungerande SMT-modell av vårt kontrakt.
Du kan se att den är väldigt lik modellen från min tidigare artikel, som jag sammanställt manuellt.
Färdig 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()
Efter lanseringen löser Z3Prover det smarta kontraktet och ger oss en kedja av transaktioner som gör att vi kan ta ut pengar:
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
Utöver färjekontraktet kan du experimentera med dina egna kontrakt eller prova detta enkla exempel, som löses i 2 transaktioner.
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
}
Eftersom detta är den allra första versionen är syntaxen väldigt begränsad och det kan finnas buggar.
I följande artiklar planerar jag att täcka vidareutvecklingen av VM:n, och visa hur du kan skapa formellt verifierade smarta kontrakt med dess hjälp, och inte bara lösa dem.
Den virtuella karaktärsmaskinen är tillgänglig på
Efter att ha ställt in källkoden för den symboliska VM:n och lagt till kommentarer där, planerar jag att lägga den på GitHub för fri tillgång.
Källa: will.com