VeriSmart

Spezifikation und funktionale Verifikation von Smart Contracts

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
Bernhard Beckert	Leitung	+49 721 608-44025	beckert1180370519Xfd4∂kit.edu
Jonas Schiffl	Verwaltung	+49 721 608-45252	jonas.schiffl337333110Xfd4∂kit.edu
Mihai Herda	Mitglied	+49 721 608-43856	herda1204053934Xfd4∂kit.edu
Michael Kirsten	Mitglied	+49 721 608-45648	kirsten1908521225Xfd4∂kit.edu