VeriSmart

Spezifikation und funktionale Verifikation von Smart Contracts

Software Campus

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.

Smart Contracts erfordern eine besonders hohe Zuverlässigkeit: Mit ihnen werden finanzielle Güter, Rechte und andere Werte verwaltet, weswegen sie ein sensibles Ziel für potentielle Angreifer darstellen. Daher ist es notwendig, für die Qualitätssicherung von Smart Contracts formale Methoden einzusetzen.

Ziel dieses Projekts ist es, Wege für die Spezifikation und formale Verifikation von Smart Contracts zu schaffen. Aufbauend auf existierenden Technologien und Werkzeugen der formalen Verifikation soll eine Basis geschaffen werden, die es ermöglicht, funktionale Eigenschaften von Smart Contracts zu beschreiben und zu beweisen, sodass die Blockchain-/Smart-Contract-Technologie mit all ihren Vorteilen sicher und zuverlässig verwendet werden kann.

Das Projekt wird geleitet von Prof. Bernhard Beckert und verwaltet von Jonas Schiffl. Es ist Teil des BMBF-geförderten Software Campus-Projekts. Kooperationspartner des Projekts ist die DATEV eG.

Personen

Name Rolle Tel. E-Mail
Leitung +49 721 608-44025 beckert791659686Xfd4∂kit.edu
Verwaltung +49 721 608-45252 jonas.schiffl49501910Xfd4∂kit.edu
Mitglied +49 721 608-43856 herda1225808517Xfd4∂kit.edu
Michael Kirsten Mitglied +49 721 608-45648 kirsten969423184Xfd4∂kit.edu