Umfang

Dieses Thema kann als Projektarbeit oder Masterarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • gute B oder Event-B Kenntnisse (z.B. durch Besuch der Veranstaltung “Sicherheitskritische Systeme”)
  • Kenntnisse aus dem Compilerbau

Problem

Smart Contracts sind Programme, die z.B. in einer Blockchain hinterlegt werden. Darin kann beispielsweise formuliert werden, dass eine Geldmenge transferiert wird, sobald eine Gegenleistung erhalten wird und ein bestimmtes Datum noch nicht überschritten wurde. Eine Programmiersprache dafür ist Solidity, welche von Ethereum verwendet wird.

Da die Programmiersprache Turing-vollständig ist, können gewisse Programme bzw. Contracts unübersichtlich sein. Wenn man an obfuscated code denkt, möchte man sicher sein, dass Contracts auch tatsächlich so funktionieren wie gedacht und man keine böse Überraschung erlebt.

Die Idee ist, dass man z.B. Solidity nach B übersetzt, um dann mit LTL Formeln bestimmte Eigenschaften zu verifizieren.

Minimalanforderungen

  • Übersetzung einer Teilmenge von Solidity nach B

Kontakt

Philipp Körner
Raum 25.12.02.56
p.koerner@hhu.de