Bei der formalen Verifizierung handelt es sich um die Verifizierung eines Programms oder Algorithmus mithilfe eines anderen.
Dies ist eine der leistungsstärksten Methoden, mit der Sie alle Schwachstellen in einem Programm finden oder nachweisen können, dass sie nicht vorhanden sind.
Eine detailliertere Beschreibung der formalen Verifizierung findet sich am Beispiel der Lösung des Problems von in meinem vorherigen Artikel.
In diesem Artikel gehe ich von der formalen Überprüfung von Problemen zu Programmen über und beschreibe, wie
wie können sie automatisch in formale Regelsysteme umgewandelt werden?
Zu diesem Zweck habe ich mein eigenes Analogon einer virtuellen Maschine geschrieben und dabei symbolische Prinzipien verwendet.
Es analysiert den Programmcode und übersetzt ihn in ein Gleichungssystem (SMT), das bereits programmgesteuert gelöst werden kann.
Da Informationen zu symbolischen Berechnungen im Internet eher fragmentarisch dargestellt werden,
Ich werde kurz beschreiben, was es ist.
Die symbolische Berechnung ist eine Möglichkeit, ein Programm gleichzeitig auf einer Vielzahl von Daten auszuführen, und das Hauptwerkzeug für die formale Programmverifizierung.
Beispielsweise können wir Eingabebedingungen festlegen, bei denen das erste Argument einen beliebigen positiven Wert annehmen kann, das zweite einen negativen Wert, das dritte eine Null und das Ausgabeargument beispielsweise 42.
Symbolische Berechnungen in einem Durchgang geben uns die Antwort darauf, ob es uns möglich ist, das gewünschte Ergebnis zu erhalten, und ein Beispiel für einen Satz solcher Eingabeparameter. Oder der Beweis, dass es solche Parameter nicht gibt.
Darüber hinaus können wir die Eingabeargumente auf alle möglichen festlegen und nur die Ausgabeargumente auswählen, zum Beispiel das Administratorkennwort.
In diesem Fall finden wir alle Schwachstellen des Programms oder erhalten den Nachweis, dass das Administratorkennwort sicher ist.
Es ist zu beachten, dass die klassische Ausführung eines Programms mit bestimmten Eingabedaten ein Sonderfall der symbolischen Ausführung ist.
Daher kann meine Charakter-VM auch im Emulationsmodus einer standardmäßigen virtuellen Maschine arbeiten.
In den Kommentaren zum vorherigen Artikel findet man berechtigte Kritik an der formalen Verifizierung mit einer Diskussion ihrer Schwächen.
Die Hauptprobleme sind:
- Kombinatorische Explosion, da die formale Verifizierung letztlich auf P=NP hinausläuft
- Die Verarbeitung von Aufrufen an das Dateisystem, Netzwerke und andere externe Speicher ist schwieriger zu überprüfen
- Fehler in der Spezifikation, wenn der Kunde oder Programmierer etwas beabsichtigt hat, es aber in der technischen Spezifikation nicht genau genug beschrieben hat.
Dadurch wird das Programm verifiziert und entspricht der Spezifikation, wird aber etwas völlig anderes tun, als die Ersteller von ihm erwartet haben.
Da ich in diesem Artikel vor allem den Einsatz formaler Verifikation in der Praxis betrachte, werde ich vorerst nicht mit dem Kopf gegen die Wand schlagen und ein System wählen, bei dem die algorithmische Komplexität und die Anzahl externer Aufrufe minimal sind.
Da Smart Contracts diesen Anforderungen am besten gerecht werden, fiel die Wahl auf RIDE-Verträge der Waves-Plattform: Sie sind nicht Turing-vollständig und ihre maximale Komplexität ist künstlich begrenzt.
Wir werden sie jedoch ausschließlich von der technischen Seite betrachten.
Darüber hinaus ist bei allen Verträgen vor allem die formelle Prüfung gefragt: Es ist in der Regel unmöglich, einen Vertragsfehler nach Vertragsabschluss zu korrigieren.
Und die Kosten solcher Fehler können sehr hoch sein, da oft recht große Geldbeträge in Smart Contracts gespeichert sind.
Meine symbolische virtuelle Maschine ist in PHP und Python geschrieben und verwendet Z3Prover von Microsoft Research, um die resultierenden SMT-Formeln zu lösen.
Im Mittelpunkt steht eine leistungsstarke multitransaktionale Suche, die
ermöglicht es Ihnen, Lösungen oder Schwachstellen zu finden, auch wenn dafür viele Transaktionen erforderlich sind.
Auch , eines der leistungsstärksten symbolischen Frameworks zum Auffinden von Ethereum-Schwachstellen, hat diese Funktion erst vor einigen Monaten hinzugefügt.
Es ist jedoch erwähnenswert, dass Ether-Verträge komplexer und Turing-vollständiger sind.
PHP übersetzt den Quellcode des RIDE-Smart-Vertrags in ein Python-Skript, in dem das Programm als Z3 SMT-kompatibles System von Vertragszuständen und Bedingungen für deren Übergänge dargestellt wird:
Jetzt werde ich genauer beschreiben, was im Inneren passiert.
Doch zunächst ein paar Worte zur RIDE-Smart-Contract-Sprache.
Es handelt sich um eine funktionale und ausdrucksbasierte Programmiersprache, die von Natur aus faul ist.
RIDE läuft isoliert innerhalb der Blockchain und kann Informationen aus dem mit der Wallet des Benutzers verknüpften Speicher abrufen und schreiben.
Sie können jedem Wallet einen RIDE-Vertrag beifügen, und das Ergebnis der Ausführung ist nur WAHR oder FALSCH.
TRUE bedeutet, dass der Smart Contract die Transaktion zulässt, und FALSE bedeutet, dass er sie verbietet.
Ein einfaches Beispiel: Ein Skript kann eine Überweisung verbieten, wenn das Wallet-Guthaben weniger als 100 beträgt.
Als Beispiel nehme ich den gleichen Wolf, die gleiche Ziege und den gleichen Kohl, aber bereits in Form eines Smart Contracts präsentiert.
Der Benutzer kann kein Geld von der Wallet abheben, auf der der Vertrag läuft, bis er alle auf die andere Seite geschickt hat.
#Извлекаем положение всех объектов из блокчейна
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 extrahiert zunächst alle Variablen aus dem Smart Contract in Form ihrer Schlüssel und der entsprechenden booleschen Ausdrucksvariablen.
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 wandelt sie dann in eine Z3Prover SMT-kompatible Systembeschreibung in Python um.
Die Daten werden in eine Schleife eingebunden, in der Speichervariablen den Index i, Transaktionsvariablen den Index i + 1 erhalten und Variablen mit Ausdrücken die Regeln für den Übergang vom vorherigen Zustand zum nächsten festlegen.
Dies ist das Herzstück unserer virtuellen Maschine, die eine multitransaktionale Suchmaschine bereitstellt.
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] )
Die Bedingungen werden sortiert und in eine Skriptvorlage eingefügt, die das SMT-System in Python beschreiben soll.
Leere Vorlage
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 letzten Zustand in der gesamten Kette gelten die Regeln, die im Abschnitt „Übertragungstransaktion“ angegeben sind.
Das bedeutet, dass Z3Prover nach genau solchen Konditionen sucht, die es letztendlich ermöglichen, Gelder aus dem Vertrag zurückzuziehen.
Als Ergebnis erhalten wir automatisch ein voll funktionsfähiges SMT-Modell unseres Vertrags.
Sie können sehen, dass es dem Modell aus meinem vorherigen Artikel, das ich manuell zusammengestellt habe, sehr ähnlich ist.
Fertige Vorlage
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()
Nach dem Start löst Z3Prover den Smart Contract und stellt uns eine Transaktionskette zur Verfügung, die es uns ermöglicht, Gelder abzuheben:
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
Zusätzlich zum Fährvertrag können Sie mit Ihren eigenen Verträgen experimentieren oder dieses einfache Beispiel ausprobieren, das in 2 Transaktionen gelöst wird.
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
}
Da es sich um die allererste Version handelt, ist die Syntax sehr eingeschränkt und es können Fehler auftreten.
In den folgenden Artikeln möchte ich auf die Weiterentwicklung der VM eingehen und zeigen, wie man mit ihrer Hilfe formal verifizierte Smart Contracts erstellen und nicht nur lösen kann.
Die virtuelle Charaktermaschine ist verfügbar unter
Nachdem ich den Quellcode der symbolischen VM geordnet und dort Kommentare hinzugefügt habe, plane ich, ihn für den kostenlosen Zugriff auf GitHub bereitzustellen.
Source: habr.com