Verificarea formală este verificarea unui program sau algoritm folosind altul.
Aceasta este una dintre cele mai puternice metode care vă permite să găsiți toate vulnerabilitățile dintr-un program sau să demonstrați că acestea nu există.
O descriere mai detaliată a verificării formale poate fi văzută în exemplul de rezolvare a problemei in articolul meu anterior.
În acest articol trec de la verificarea formală a problemelor la programe și descriu cum
cum pot fi convertite automat în sisteme de reguli formale.
Pentru a face acest lucru, am scris propriul meu analog al unei mașini virtuale, folosind principii simbolice.
Parsează codul programului și îl traduce într-un sistem de ecuații (SMT), care poate fi deja rezolvat programatic.
Deoarece informațiile despre calculele simbolice sunt prezentate pe Internet în mod destul de fragmentar,
Voi descrie pe scurt despre ce este vorba.
Calculul simbolic este o modalitate de a executa simultan un program pe o gamă largă de date și este instrumentul principal pentru verificarea formală a programului.
De exemplu, putem seta condiții de intrare în care primul argument poate lua orice valoare pozitivă, al doilea negativ, al treilea zero și argumentul de ieșire, de exemplu, 42.
Calculele simbolice dintr-o singură rulare ne vor oferi răspunsul dacă este posibil să obținem rezultatul dorit și un exemplu de set de astfel de parametri de intrare. Sau dovada că nu există asemenea parametri.
Mai mult, putem seta argumentele de intrare la toate cele posibile și le putem selecta doar pe cele de ieșire, de exemplu, parola de administrator.
În acest caz, vom găsi toate vulnerabilitățile programului sau vom obține dovada că parola administratorului este sigură.
Se poate observa că execuția clasică a unui program cu date de intrare specifice este un caz special de execuție simbolică.
Prin urmare, personajul meu VM poate funcționa și în modul de emulare a unei mașini virtuale standard.
În comentariile la articolul precedent se poate găsi o critică justă a verificării formale cu o discuție despre punctele slabe ale acesteia.
Principalele probleme sunt:
- Explozie combinatorie, deoarece verificarea formală se reduce în cele din urmă la P=NP
- Procesarea apelurilor către sistemul de fișiere, rețele și alte stocări externe este mai dificil de verificat
- Erori în specificație, când clientul sau programatorul a intenționat un lucru, dar nu l-a descris suficient de precis în specificația tehnică.
Ca urmare, programul va fi verificat și va respecta specificația, dar va face ceva complet diferit de ceea ce creatorii se așteptau de la el.
Deoarece în acest articol mă gândesc în principal la utilizarea verificării formale în practică, deocamdată nu mă voi lovi cu capul de perete și voi alege un sistem în care complexitatea algoritmică și numărul de apeluri externe sunt minime.
Întrucât contractele inteligente se potrivesc cel mai bine acestor cerințe, alegerea a căzut pe contractele RIDE de pe platforma Waves: nu sunt Turing complete, iar complexitatea lor maximă este limitată artificial.
Dar le vom lua în considerare exclusiv din punct de vedere tehnic.
Pe lângă toate, verificarea formală va fi solicitată în special pentru orice contract: este de obicei imposibil să corectați o eroare de contract după ce aceasta a fost lansată.
Și costul unor astfel de erori poate fi foarte mare, deoarece cantități destul de mari de fonduri sunt adesea stocate pe contracte inteligente.
Mașina mea virtuală simbolică este scrisă în PHP și Python și folosește Z3Prover de la Microsoft Research pentru a rezolva formulele SMT rezultate.
La baza ei se află o căutare puternică multi-tranzacțională, care
vă permite să găsiți soluții sau vulnerabilități, chiar dacă necesită multe tranzacții.
Chiar , unul dintre cele mai puternice cadre simbolice pentru găsirea vulnerabilităților Ethereum, a adăugat această capacitate doar acum câteva luni.
Dar este de remarcat faptul că contractele cu eter sunt mai complexe și Turing complet.
PHP traduce codul sursă al contractului inteligent RIDE într-un script python, în care programul este prezentat ca un sistem compatibil Z3 SMT de stări contractuale și condiții pentru tranzițiile lor:
Acum voi descrie mai detaliat ce se întâmplă în interior.
Dar mai întâi, câteva cuvinte despre limbajul contractului inteligent RIDE.
Este un limbaj de programare funcțional și bazat pe expresii, care este leneș prin proiectare.
RIDE rulează izolat în cadrul blockchain-ului și poate prelua și scrie informații din stocarea conectată la portofelul utilizatorului.
Puteți atașa un contract RIDE fiecărui portofel, iar rezultatul execuției va fi doar ADEVĂRAT sau FALS.
TRUE înseamnă că contractul inteligent permite tranzacția, iar FALSE înseamnă că o interzice.
Un exemplu simplu: un script poate interzice un transfer dacă soldul portofelului este mai mic de 100.
Ca exemplu, voi lua același Lup, Capră și Varză, dar deja prezentate sub forma unui contract inteligent.
Utilizatorul nu va putea retrage bani din portofelul pe care este desfășurat contractul până când nu îi va trimite pe toți pe cealaltă parte.
#Извлекаем положение всех объектов из блокчейна
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 extrage mai întâi toate variabilele din contractul inteligent sub forma cheilor lor și a variabilei de expresie booleană corespunzătoare.
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 le convertește apoi într-o descriere de sistem compatibilă cu Z3Prover SMT în Python.
Datele sunt împachetate într-o buclă, unde variabilele de stocare primesc indicele i, variabilele de tranzacție indicele i + 1, iar variabilele cu expresii stabilesc regulile pentru tranziția de la starea anterioară la următoarea.
Aceasta este însăși inima mașinii noastre virtuale, care oferă un mecanism de căutare multi-tranzacțional.
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] )
Condițiile sunt sortate și inserate într-un șablon de script conceput pentru a descrie sistemul SMT în Python.
Șablon gol
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()
Pentru ultima stare din întreg lanțul se aplică regulile care sunt specificate în secțiunea tranzacție de transfer.
Aceasta înseamnă că Z3Prover va căuta exact astfel de seturi de condiții care vor permite în cele din urmă retragerea fondurilor din contract.
Ca urmare, primim automat un model SMT complet funcțional al contractului nostru.
Puteți vedea că este foarte asemănător cu modelul din articolul meu anterior, pe care l-am compilat manual.
Șablon finalizat
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()
După lansare, Z3Prover rezolvă contractul inteligent și ne oferă un lanț de tranzacții care ne va permite să retragem fonduri:
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
Pe langa contractul de feribot, puteti experimenta propriile contracte sau incercati acest exemplu simplu, care se rezolva in 2 tranzactii.
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
}
Deoarece aceasta este prima versiune, sintaxa este foarte limitată și pot exista erori.
În articolele următoare, intenționez să acopăr dezvoltarea ulterioară a VM și să arăt cum puteți crea contracte inteligente verificate oficial cu ajutorul acestuia și nu doar să le rezolvați.
Mașina virtuală de caractere este disponibilă la
După ce am pus în ordine codul sursă al VM-ului simbolic și am adăugat comentarii acolo, plănuiesc să îl pun pe GitHub pentru acces gratuit.
Sursa: www.habr.com