Modelling Smart Contracts as Petri Nets for Verification

Typ:	BA/ MA
Datum:
Betreuer:	Jonas Schiffl
Aushang:

Motivation

Smart Contracts are programs that run in conjuntion with distributed ledgers. They often manage resources or tokens that represent valuable assets. Smart contracts enable anyone to execute a particular program on somebody else's computer, while still being sure about the executed source code and the execution environment.

This comes at a cost: Smart contracts are hard to patch, and therefore, programming errors cannot easily be fixed. Therefore, it is vitally important that smart contracts are correct and secure upon deployment. For this, formal methods are essential.

Project description

The goal of this project is modelling smart contracts as Petri Nets in order to analyse their behavior in this formalism, and investigate which kinds of properties can be usefully examined in this way.

In the course of this project, it will be necessary to

• become familiar with the Petri Net formalism
• develop and implement a translation from an existing smart contract modelling language to Petri Nets
• devise an evaluation of how well smart contracts can be analysed in this formalism

Requirements

Understanding of first order logic and program verification as taught, e.g., in the Formale Systeme lecture.