Spezifikation und Verifikation von Smart Contracts in Hyperledger Fabric

Typ:	MA
Datum:	2018-06-21
Betreuer:	Michael Kirsten Mihai Herda
Aushang:

Hintergrund

Smart Contracts sind Programme, die in einer Blockchain ausgeführt werden. Sie bilden Verträge und andere Arten von Absprachen zwischen zwei oder mehr Parteien ab und setzen die in ihnen definierten Bedingungen automatisiert und transparent um. Typische Anwendungsbereiche sind beispielsweise Geschäftsbeziehungen, bei denen die Blockchain und die darin laufenden Programme gleichzeitig als Datenbank und als Schutz vor Betrug dienen, oder Wahlen, wobei durch die Blockchain die Gleichheit und Geheimhaltung der Stimmen gewährleistet werden.

Ziel

Ziel dieser Arbeit ist es, Wege für die Spezifikation und formale Verifikation von Smart Contracts des Frameworks Hyperledger Fabric zu schaffen. Mithilfe des deduktiven Programm-Verifikationssystems KeY soll eine Basis geschaffen werden, die es ermöglicht, funktionale Eigenschaften von Smart Contracts zu beschreiben und zu beweisen, sodass die Blockchain- bzw. Smart-Contract-Technologie mit all ihren Vorteilen sicher und zuverlässig verwendet werden kann.

Aufgaben

Hierzu sind Anpassungen der Spezifikationssprache JML notwendig, die die typischen Eigenschaften von Smart Contracts mit einbeziehen. Anschließend soll die Möglichkeit geschaffen werden, einen Smart Contract samt Spezifikation in KeY zu laden und in die logische Sprache JavaDL zu übersetzen. Diese zwei Schwerpunkte, Spezifikation und Verifikation, sollen zunächst im Hinblick auf einzelne, für sich stehende Smart Contracts untersucht werden. Fokus ist die Anpassung von KeY an die Zieltechnologie, d.h. die verwendeten Smart Contracts. Um den in diesem Projekt gewählten Ansatz zu validieren, soll die Spezifikation und Verifikation von anfangs gewählten Anwendungsfällen in einem prototypischen Verifikationswerkzeug umgesetzt werden. Hierzu sollen möglichst direkt in der Blockchain verwendbare Smart Contracts genutzt werden.