Η επίσημη επαλήθευση είναι η επαλήθευση ενός προγράμματος ή αλγορίθμου χρησιμοποιώντας ένα άλλο.
Αυτή είναι μια από τις πιο ισχυρές μεθόδους που σας επιτρέπει να βρείτε όλα τα τρωτά σημεία σε ένα πρόγραμμα ή να αποδείξετε ότι δεν υπάρχουν.
Μια πιο λεπτομερής περιγραφή της επίσημης επαλήθευσης μπορεί να φανεί στο παράδειγμα επίλυσης του προβλήματος του στο προηγούμενο άρθρο μου.
Σε αυτό το άρθρο μετακινούμαι από την επίσημη επαλήθευση προβλημάτων στα προγράμματα και περιγράφω τον τρόπο
πώς μπορούν να μετατραπούν αυτόματα σε επίσημα συστήματα κανόνων.
Για να γίνει αυτό, έγραψα το δικό μου ανάλογο μιας εικονικής μηχανής, χρησιμοποιώντας συμβολικές αρχές.
Αναλύει τον κώδικα του προγράμματος και τον μεταφράζει σε ένα σύστημα εξισώσεων (SMT), το οποίο μπορεί ήδη να λυθεί μέσω προγραμματισμού.
Δεδομένου ότι οι πληροφορίες για τους συμβολικούς υπολογισμούς παρουσιάζονται στο Διαδίκτυο μάλλον αποσπασματικά,
Θα περιγράψω εν συντομία τι είναι.
Ο συμβολικός υπολογισμός είναι ένας τρόπος για την ταυτόχρονη εκτέλεση ενός προγράμματος σε ένα ευρύ φάσμα δεδομένων και είναι το κύριο εργαλείο για την επίσημη επαλήθευση του προγράμματος.
Για παράδειγμα, μπορούμε να ορίσουμε συνθήκες εισόδου όπου το πρώτο όρισμα μπορεί να λάβει οποιεσδήποτε θετικές τιμές, το δεύτερο αρνητικό, το τρίτο μηδέν και το όρισμα εξόδου, για παράδειγμα, 42.
Οι συμβολικοί υπολογισμοί σε μία εκτέλεση θα μας δώσουν την απάντηση στο εάν είναι δυνατόν να λάβουμε το επιθυμητό αποτέλεσμα και ένα παράδειγμα ενός συνόλου τέτοιων παραμέτρων εισόδου. Ή απόδειξη ότι δεν υπάρχουν τέτοιες παράμετροι.
Επιπλέον, μπορούμε να ορίσουμε τα ορίσματα εισόδου σε όλα τα πιθανά και να επιλέξουμε μόνο τα εξαγόμενα, για παράδειγμα, τον κωδικό πρόσβασης διαχειριστή.
Σε αυτήν την περίπτωση, θα βρούμε όλα τα τρωτά σημεία του προγράμματος ή θα λάβουμε απόδειξη ότι ο κωδικός πρόσβασης του διαχειριστή είναι ασφαλής.
Μπορεί να σημειωθεί ότι η κλασική εκτέλεση ενός προγράμματος με συγκεκριμένα δεδομένα εισόδου είναι μια ειδική περίπτωση συμβολικής εκτέλεσης.
Επομένως, ο χαρακτήρας μου VM μπορεί επίσης να λειτουργήσει σε λειτουργία εξομοίωσης μιας τυπικής εικονικής μηχανής.
Στα σχόλια του προηγούμενου άρθρου μπορεί κανείς να βρει δίκαιη κριτική για την επίσημη επαλήθευση με συζήτηση των αδυναμιών του.
Τα κύρια προβλήματα είναι:
- Συνδυαστική έκρηξη, αφού η επίσημη επαλήθευση καταλήγει τελικά σε P=NP
- Η επεξεργασία κλήσεων προς το σύστημα αρχείων, τα δίκτυα και άλλο εξωτερικό χώρο αποθήκευσης είναι πιο δύσκολο να επαληθευτεί
- Σφάλματα στις προδιαγραφές, όταν ο πελάτης ή ο προγραμματιστής σκόπευε ένα πράγμα, αλλά δεν το περιέγραψε με αρκετή ακρίβεια στις τεχνικές προδιαγραφές.
Ως αποτέλεσμα, το πρόγραμμα θα επαληθευτεί και θα συμμορφωθεί με τις προδιαγραφές, αλλά θα κάνει κάτι εντελώς διαφορετικό από αυτό που περίμεναν οι δημιουργοί από αυτό.
Επειδή σε αυτό το άρθρο σκέφτομαι κυρίως τη χρήση της επίσημης επαλήθευσης στην πράξη, δεν θα χτυπήσω το κεφάλι μου στον τοίχο προς το παρόν και θα επιλέξω ένα σύστημα όπου η αλγοριθμική πολυπλοκότητα και ο αριθμός των εξωτερικών κλήσεων είναι ελάχιστοι.
Δεδομένου ότι τα έξυπνα συμβόλαια ταιριάζουν καλύτερα σε αυτές τις απαιτήσεις, η επιλογή έπεσε στα συμβόλαια RIDE από την πλατφόρμα Waves: δεν είναι ολοκληρωμένα Turing και η μέγιστη πολυπλοκότητά τους είναι τεχνητά περιορισμένη.
Θα τα εξετάσουμε όμως αποκλειστικά από την τεχνική πλευρά.
Εκτός από όλα, η επίσημη επαλήθευση θα είναι ιδιαίτερα περιζήτητη για τυχόν συμβόλαια: είναι συνήθως αδύνατο να διορθωθεί ένα σφάλμα συμβολαίου μετά την κυκλοφορία του.
Και το κόστος τέτοιων σφαλμάτων μπορεί να είναι πολύ υψηλό, καθώς αρκετά μεγάλα ποσά κεφαλαίων συχνά αποθηκεύονται σε έξυπνα συμβόλαια.
Η συμβολική εικονική μηχανή μου είναι γραμμένη σε PHP και Python και χρησιμοποιεί Z3Prover από τη Microsoft Research για να λύσει τους τύπους SMT που προκύπτουν.
Στον πυρήνα της βρίσκεται μια ισχυρή αναζήτηση πολλαπλών συναλλαγών, η οποία
σας επιτρέπει να βρείτε λύσεις ή τρωτά σημεία, ακόμα κι αν απαιτεί πολλές συναλλαγές.
Ακόμα και το , ένα από τα πιο ισχυρά συμβολικά πλαίσια για την εύρεση τρωτών σημείων του Ethereum, πρόσθεσε αυτή τη δυνατότητα μόλις πριν από λίγους μήνες.
Αξίζει όμως να σημειωθεί ότι τα συμβόλαια αιθέρα είναι πιο περίπλοκα και ο Turing ολοκληρωμένος.
Η PHP μεταφράζει τον πηγαίο κώδικα του έξυπνου συμβολαίου RIDE σε ένα σενάριο python, στο οποίο το πρόγραμμα παρουσιάζεται ως σύστημα συμβατό με Z3 SMT συμβάσεων καταστάσεων και προϋποθέσεων για τις μεταβάσεις τους:
Τώρα θα περιγράψω τι συμβαίνει μέσα με περισσότερες λεπτομέρειες.
Αλλά πρώτα, λίγα λόγια για τη γλώσσα έξυπνων συμβολαίων RIDE.
Είναι μια λειτουργική και βασισμένη σε εκφράσεις γλώσσα προγραμματισμού που είναι τεμπέλης από το σχεδιασμό.
Το RIDE εκτελείται μεμονωμένα μέσα στο blockchain και μπορεί να ανακτήσει και να γράψει πληροφορίες από τον χώρο αποθήκευσης που συνδέεται με το πορτοφόλι του χρήστη.
Μπορείτε να επισυνάψετε ένα συμβόλαιο RIDE σε κάθε πορτοφόλι και το αποτέλεσμα της εκτέλεσης θα είναι μόνο TRUE ή FALSE.
TRUE σημαίνει ότι το έξυπνο συμβόλαιο επιτρέπει τη συναλλαγή και FALSE σημαίνει ότι την απαγορεύει.
Ένα απλό παράδειγμα: ένα σενάριο μπορεί να απαγορεύσει μια μεταφορά εάν το υπόλοιπο του πορτοφολιού είναι μικρότερο από 100.
Ως παράδειγμα, θα πάρω το ίδιο Λύκο, Κατσίκα και Λάχανο, αλλά ήδη παρουσιάζεται με τη μορφή έξυπνου συμβολαίου.
Ο χρήστης δεν θα μπορεί να κάνει ανάληψη χρημάτων από το πορτοφόλι στο οποίο έχει αναπτυχθεί η σύμβαση μέχρι να στείλει όλους στην άλλη πλευρά.
#Извлекаем положение всех объектов из блокчейна
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 εξάγει πρώτα όλες τις μεταβλητές από το έξυπνο συμβόλαιο με τη μορφή των κλειδιών τους και την αντίστοιχη μεταβλητή έκφρασης Boole.
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 τα μετατρέπει σε μια περιγραφή συστήματος συμβατή με Z3Prover SMT στην Python.
Τα δεδομένα είναι τυλιγμένα σε έναν βρόχο, όπου οι μεταβλητές αποθήκευσης λαμβάνουν δείκτη i, οι μεταβλητές συναλλαγής δείκτης i + 1 και οι μεταβλητές με εκφράσεις ορίζουν τους κανόνες για τη μετάβαση από την προηγούμενη κατάσταση στην επόμενη.
Αυτή είναι η ίδια η καρδιά της εικονικής μας μηχανής, η οποία παρέχει μια μηχανή αναζήτησης πολλαπλών συναλλαγών.
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] )
Οι συνθήκες ταξινομούνται και εισάγονται σε ένα πρότυπο σεναρίου που έχει σχεδιαστεί για να περιγράφει το σύστημα SMT στην Python.
Κενό πρότυπο
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()
Για την τελευταία κατάσταση σε ολόκληρη την αλυσίδα, εφαρμόζονται οι κανόνες που καθορίζονται στην ενότητα της συναλλαγής μεταφοράς.
Αυτό σημαίνει ότι η Z3Prover θα αναζητήσει ακριβώς τέτοια σύνολα όρων που θα επιτρέψουν τελικά την απόσυρση κεφαλαίων από τη σύμβαση.
Ως αποτέλεσμα, λαμβάνουμε αυτόματα ένα πλήρως λειτουργικό μοντέλο SMT του συμβολαίου μας.
Μπορείτε να δείτε ότι μοιάζει πολύ με το μοντέλο από το προηγούμενο άρθρο μου, το οποίο συνέταξα χειροκίνητα.
Ολοκληρωμένο πρότυπο
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()
Μετά την κυκλοφορία, η Z3Prover λύνει το έξυπνο συμβόλαιο και μας παρέχει μια αλυσίδα συναλλαγών που θα μας επιτρέψουν να αποσύρουμε χρήματα:
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
Εκτός από το συμβόλαιο του πλοίου, μπορείτε να πειραματιστείτε με τα δικά σας συμβόλαια ή να δοκιμάσετε αυτό το απλό παράδειγμα, το οποίο λύνεται σε 2 συναλλαγές.
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
}
Δεδομένου ότι αυτή είναι η πρώτη έκδοση, η σύνταξη είναι πολύ περιορισμένη και ενδέχεται να υπάρχουν σφάλματα.
Στα επόμενα άρθρα, σκοπεύω να καλύψω την περαιτέρω ανάπτυξη του VM και να δείξω πώς μπορείτε να δημιουργήσετε επίσημα επαληθευμένα έξυπνα συμβόλαια με τη βοήθειά του και όχι απλώς να τα λύσετε.
Η εικονική μηχανή χαρακτήρων είναι διαθέσιμη στη διεύθυνση
Αφού βάλω σε σειρά τον πηγαίο κώδικα του συμβολικού VM και προσθέσω σχόλια εκεί, σκοπεύω να το βάλω στο GitHub για δωρεάν πρόσβαση.
Πηγή: www.habr.com