Formálne overenie je overenie jedného programu alebo algoritmu pomocou iného.
Toto je jedna z najsilnejších metód, ktorá vám umožní nájsť všetky zraniteľné miesta v programe alebo dokázať, že neexistujú.
Podrobnejší popis formálneho overovania je možné vidieť na príklade riešenia problému o v mojom predchádzajúcom článku.
V tomto článku prechádzam od formálneho overovania problémov k programom a popisujem ako
ako ich možno automaticky previesť na systémy formálnych pravidiel.
Aby som to urobil, napísal som svoj vlastný analóg virtuálneho stroja pomocou symbolických princípov.
Parsuje programový kód a prekladá ho do systému rovníc (SMT), ktorý je už možné riešiť programovo.
Keďže informácie o symbolických výpočtoch sú na internete prezentované pomerne fragmentárne,
Stručne popíšem, čo to je.
Symbolický výpočet je spôsob, ako súčasne spustiť program na širokom spektre údajov a je hlavným nástrojom na formálne overenie programu.
Napríklad môžeme nastaviť vstupné podmienky, kde prvý argument môže mať akékoľvek kladné hodnoty, druhý záporné hodnoty, tretí nulu a výstupný argument môže mať napríklad 42.
Symbolické výpočty v jednom behu nám dajú odpoveď na to, či je možné, aby sme dosiahli požadovaný výsledok a príklad sady takýchto vstupných parametrov. Alebo dôkaz, že takéto parametre neexistujú.
Navyše môžeme nastaviť vstupné argumenty na všetky možné a vybrať len tie výstupné, napríklad heslo správcu.
V takom prípade nájdeme všetky slabé miesta programu alebo získame dôkaz, že heslo správcu je bezpečné.
Je možné poznamenať, že klasické vykonávanie programu so špecifickými vstupnými údajmi je špeciálnym prípadom symbolického vykonávania.
Preto môj VM postavy môže pracovať aj v režime emulácie štandardného virtuálneho počítača.
V komentároch k predchádzajúcemu článku možno nájsť férovú kritiku formálneho overovania s diskusiou o jeho slabinách.
Hlavné problémy sú:
- Kombinatorická explózia, pretože formálne overenie nakoniec príde na P = NP
- Spracovanie volaní do systému súborov, sietí a iných externých úložísk je ťažšie overiteľné
- Chyby v špecifikácii, kedy zákazník alebo programátor zamýšľal jednu vec, ale v technickej špecifikácii to nepopísal dostatočne presne.
Vďaka tomu bude program overený a bude v súlade so špecifikáciou, no bude robiť niečo úplne iné, ako od neho tvorcovia očakávali.
Keďže v tomto článku uvažujem najmä o využití formálneho overovania v praxi, nebudem si zatiaľ búchať hlavu o stenu a zvolím systém, kde je algoritmická náročnosť a počet externých hovorov minimálny.
Keďže týmto požiadavkám najviac vyhovujú smart kontrakty, voľba padla na kontrakty RIDE z platformy Waves: nie sú kompletné Turing a ich maximálna komplexnosť je umelo obmedzená.
Budeme ich však posudzovať výlučne z technickej stránky.
Okrem všetkého bude pri akýchkoľvek zmluvách žiadané najmä formálne overenie: opraviť chybu zmluvy po jej spustení je zvyčajne nemožné.
A náklady na takéto chyby môžu byť veľmi vysoké, pretože na inteligentných zmluvách sa často ukladá pomerne veľké množstvo finančných prostriedkov.
Môj symbolický virtuálny stroj je napísaný v PHP a Pythone a používa Z3Prover od Microsoft Research na riešenie výsledných vzorcov SMT.
Jeho jadrom je výkonné multitransakčné vyhľadávanie, ktoré
umožňuje nájsť riešenia alebo zraniteľné miesta, aj keď to vyžaduje veľa transakcií.
Dokonca , jeden z najsilnejších symbolických rámcov na nájdenie zraniteľností Etherea, pridal túto schopnosť len pred niekoľkými mesiacmi.
Ale stojí za zmienku, že éterové zmluvy sú zložitejšie a Turing kompletný.
PHP prekladá zdrojový kód RIDE smart kontraktu do python skriptu, v ktorom je program prezentovaný ako Z3 SMT kompatibilný systém zmluvných stavov a podmienok pre ich prechody:
Teraz podrobnejšie popíšem, čo sa deje vo vnútri.
Najprv však pár slov o jazyku RIDE smart contract.
Je to funkčný a výrazovo založený programovací jazyk, ktorý je dizajnovo lenivý.
RIDE beží izolovane v rámci blockchainu a dokáže získavať a zapisovať informácie z úložiska prepojeného s peňaženkou používateľa.
Ku každej peňaženke môžete pripojiť zmluvu RIDE a výsledok vykonania bude iba PRAVDA alebo NEPRAVDA.
TRUE znamená, že inteligentná zmluva transakciu povoľuje a FALSE znamená, že ju zakazuje.
Jednoduchý príklad: skript môže zakázať prevod, ak je zostatok v peňaženke nižší ako 100.
Ako príklad uvediem rovnakého vlka, kozu a kapustu, ale už prezentované vo forme inteligentnej zmluvy.
Používateľ si nebude môcť vybrať peniaze z peňaženky, na ktorej je zmluva nasadená, kým všetkých nepošle na druhú 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 najskôr extrahuje všetky premenné z inteligentnej zmluvy vo forme ich kľúčov a zodpovedajúcej premennej 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 ich potom prevedie na popis systému kompatibilného so Z3Prover SMT v Pythone.
Dáta sú zabalené do slučky, kde úložné premenné dostávajú index i, transakčné premenné index i + 1 a premenné s výrazmi nastavujú pravidlá prechodu z predchádzajúceho stavu do nasledujúceho.
Toto je samotné srdce nášho virtuálneho stroja, ktorý poskytuje multitransakčný vyhľadávací mechanizmus.
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] )
Podmienky sú zoradené a vložené do šablóny skriptu navrhnutej na popis SMT systému v Pythone.
Prázdna šablóna
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()
Pre posledný stav v celom reťazci platia pravidlá, ktoré sú špecifikované v sekcii prevodná transakcia.
To znamená, že Z3Prover bude hľadať presne také súbory podmienok, ktoré v konečnom dôsledku umožnia výber prostriedkov zo zmluvy.
Výsledkom je, že automaticky dostávame plne funkčný SMT model našej zmluvy.
Vidíte, že je veľmi podobný modelu z môjho predchádzajúceho článku, ktorý som zostavil ručne.
Dokončená šablóna
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 spustení Z3Prover rieši smart kontrakt a poskytuje nám reťazec transakcií, ktoré nám umožnia vyberať prostriedky:
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
Okrem zmluvy o trajekte môžete experimentovať s vlastnými zmluvami alebo vyskúšať tento jednoduchý príklad, ktorý je riešený v 2 transakciá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
}
Keďže ide o úplne prvú verziu, syntax je veľmi obmedzená a môžu sa vyskytnúť chyby.
V nasledujúcich článkoch sa plánujem venovať ďalšiemu vývoju VM a ukázať, ako sa s jeho pomocou dajú vytvárať formálne overené smart kontrakty a nielen ich riešiť.
Virtuálny stroj postavy je dostupný na adrese
Po uvedení zdrojového kódu symbolického VM do poriadku a pridaní komentárov ho plánujem umiestniť na GitHub pre voľný prístup.
Zdroj: hab.com