Formální ověření je ověření jednoho programu nebo algoritmu pomocí jiného.
Jedná se o jednu z nejúčinnějších metod, která vám umožní najít všechna zranitelná místa v programu nebo prokázat, že neexistují.
Podrobnější popis formálního ověření je vidět na příkladu řešení problému o v mém předchozím článku.
V tomto článku přecházím od formálního ověřování problému k programům a popisuji jak
jak je můžete automaticky převést na systémy formálních pravidel.
Abych to udělal, napsal jsem svou analogii virtuálního stroje na symbolických principech.
Parsuje programový kód a převádí jej do soustavy rovnic (SMT), kterou lze již programově řešit.
Vzhledem k tomu, že informace o symbolických výpočtech jsou na internetu prezentovány spíše fragmentárně,
Stručně popíšu, co to je.
Symbolické výpočty představují způsob, jak současně spustit program na širokém spektru dat a jsou hlavním nástrojem pro formální ověření programu.
Můžeme například nastavit vstupní podmínky, kdy první argument může mít libovolnou kladnou hodnotu, druhý může být záporný, třetí může být nula a výstupní argument je například 42.
Symbolické výpočty v jednom běhu nám dají odpověď, zda je pro nás možné získat požadovaný výsledek a příklad sady takových vstupních parametrů. Nebo důkaz, že takové parametry neexistují.
Navíc můžeme nastavit vstupní argumenty obecně jako všechny možné a zvolit pouze výstup, například heslo administrátora.
V tomto případě najdeme všechny zranitelnosti programu, případně získáme důkaz, že heslo správce je bezpečné.
Je vidět, že klasické provádění programu se specifickými vstupními daty je speciálním případem symbolického.
Moje postava VM tedy může pracovat i v emulačním režimu standardního virtuálního stroje.
V komentářích k předchozímu článku lze také nalézt spravedlivou kritiku formálního ověření s diskusí o jeho slabinách.
Hlavní problémy jsou:
- Kombinatorická exploze, protože formální ověření nakonec spočívá na P=NP
- Ověření volání do systému souborů, sítí a dalších externích úložišť je obtížnější
- Chyby ve specifikaci, kdy si zákazník nebo programátor jednu věc vymyslel, ale v TOR ji přesně nepopsal.
Díky tomu bude program ověřen a bude odpovídat specifikaci, ale bude dělat něco úplně jiného, než od něj tvůrci očekávali.
Vzhledem k tomu, že v tomto článku uvažuji především o aplikaci formálního ověřování v praxi, nebudu si prozatím tlouct čelo o zeď a zvolím systém, kde je algoritmická náročnost a počet externích hovorů minimální.
Vzhledem k tomu, že smart kontrakty těmto požadavkům nejlépe vyhovují, padla volba na kontrakty RIDE z platformy Waves: nejsou kompletní podle Turinga a jejich maximální složitost je uměle omezena.
Budeme je ale posuzovat výhradně z technické stránky.
Ke všemu bude u jakýchkoli smluv požadováno především formální ověření: chybu smlouvy po jejím spuštění zpravidla nelze opravit.
A cena takových chyb může být velmi vysoká, protože na smart kontraktech jsou často uloženy poměrně velké částky finančních prostředků.
Moje postava VM je napsána v PHP a Pythonu a k řešení výsledných vzorců SMT používá Z3Prover společnosti Microsoft Research.
Jeho jádrem je výkonné multitransakční vyhledávání, které
umožňuje najít řešení nebo zranitelnosti, i když to vyžaduje mnoho transakcí.
Dokonce , jeden z nejvýkonnějších charakterových frameworků pro hledání zranitelností Etherea, přidal tuto schopnost teprve před několika měsíci.
Ale stojí za zmínku, že etherové smlouvy jsou složitější a mají Turingovu úplnost.
PHP překládá zdrojový kód RIDE smart contractu do python skriptu, ve kterém je program prezentován jako Z3 SMT kompatibilní systém smluvních stavů a podmínek jejich přechodu:
Nyní popíšu, co se děje uvnitř, podrobněji.
Nejprve však pár slov o jazyce RIDE smart contract.
Jedná se o funkční a výrazově založený programovací jazyk, který je svou konstrukcí líný.
RIDE běží izolovaně uvnitř blockchainu a může extrahovat a zapisovat informace z úložiště spojeného s peněženkou uživatele.
Ke každé peněžence lze připojit smlouvu RIDE a výsledek exekuce bude pouze PRAVDA nebo NEPRAVDA.
PRAVDA znamená, že chytrý kontrakt transakci povoluje, a NEPRAVDA, že ji zakazuje.
Jednoduchý příklad: skript může zakázat převod, pokud je zůstatek v peněžence menší než 100.
Jako příklad vezmu stejného vlka, kozu a zelí, ale již prezentované ve formě chytré smlouvy.
Uživatel nebude moci vybrat peníze z peněženky, na které je smlouva nasazena, dokud všechny nepošle na druhou stranu.
#Извлекаем положение всех объектов из блокчейна
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 nejprve extrahuje všechny proměnné z chytré smlouvy ve formě jejich klíčů a odpovídajícího booleovského výrazu.
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 je poté převede na popis systému python kompatibilní se Z3Prover SMT.
Data jsou zabalena do smyčky, kde proměnné úložiště obdrží index i, transakční proměnné index i + 1 a proměnné s výrazy nastavují pravidla pro přechod z předchozího stavu do dalšího.
Toto je samotné srdce našeho virtuálního stroje, který poskytuje multitransakční vyhledávač.
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] )
Podmínky jsou seřazeny a vloženy do šablony skriptu navržené pro popis SMT systému v pythonu.
Prázdná šablona
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()
Pro poslední stav celého řetězce platí pravidla, která jsou nastavena v sekci převodní transakce.
To znamená, že Z3Prover bude hledat přesně takové sady stavů, které vám nakonec umožní vybrat prostředky ze smlouvy.
Výsledkem je, že automaticky získáváme plně funkční SMT model naší smlouvy.
Vidíte, že je velmi podobný modelu z mého předchozího článku, který jsem sestavil ručně.
Dokončená šablona
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()
Po spuštění Z3Prover vyřeší smart kontrakt a zobrazí za nás řetězec transakcí, které nám umožní vybírat prostředky:
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ě smlouvy o křížení můžete experimentovat s vlastními smlouvami nebo vyzkoušet tento jednoduchý příklad, který je řešen ve 2 transakcích.
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
}
Protože se jedná o úplně první verzi, syntaxe je velmi omezená a mohou se vyskytovat chyby.
V dalších článcích plánuji pokrýt další vývoj VM a ukázat, jak s ním můžete vytvářet formálně ověřené smart kontrakty a nejen je řešit.
Virtuální stroj postavy je dostupný na adrese
Po uvedení zdrojového kódu znakového VM do pořádku a přidání komentářů ho plánuji dát na github ve volném přístupu.
Zdroj: www.habr.com