Eine Übersetzung von Smart Contracts nach B
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örnerRaum 25.12.02.56
p.koerner@hhu.de