Smart Contracts sind Computerprogramme, die ähnlich wie eine notarielle Aufsichtsperson Geschäftsabläufe überwachen und objektiv entscheiden, was geschehen soll. Alle Beteiligten einigen sich zuerst auf diesen Code, dann läuft er automatisch ab und kann nicht mehr umgeschrieben werden.

Allerdings hat sich herausgestellt, dass es auch bei Smart Contracts Sicherheitsprobleme geben kann: Programmfehler können dazu führen, dass Hacker Millionensummen abzweigen können. An der TU Wien wurde nun ein Tool entwickelt, das mit absoluter Zuverlässigkeit nachweisen kann, dass der Code keinen Fehler enthält und genau definierte Eigenschaften in jeder Situation erfüllt.

Für Smart Contracts werden oft Blockchain-Ökosysteme genutzt, wie man sie von Kryptowährungen wie Bitcoin oder Ethereum kennt. „Der Vorteil ist, dass die Information in der Blockchain öffentlich ist und nicht nachträglich verändert werden kann. Was einmal in der Blockchain steht, das bleibt auch dort.“, so Clara Schneidewind aus der Security-and-Privacy-Forschungsgruppe am Institut for Logic and Computation der TU Wien.

Im Jahr 2016 zeigte sich allerdings, dass solche Smart Contracts auch schiefgehen können: „Auf einer Crowdfunding-Plattform fand ein Hacker eine Möglichkeit, Kryptowährung im Wert von ungefähr 60 Mio. Euro zu stehlen“, sagt Clara Schneidewind. Schuld war ein Fehler im Code. Für das Vertrauen in Smart Contracts war es ein schwerer Schlag.

​Mathematischer Beweis für die Sicherheit

Die Experten der TU Wien haben nun ein Tool mit dem Namen „eThor“   entwickelt, mit dem sich feststellen lässt, ob der Code des Smart Contracts wirklich genau das tut, was er auch tun soll. Ähnliche Tools zum Untersuchen von Smart Contracts gibt es schon, allerdings handelt es sich dabei um sogenannte „Heuristiken“ – Methoden, die mit einer gewissen Wahrscheinlichkeit einschätzen können, ob der Vertrag vertrauenswürdig ist. Eine Garantie liefern sie aber nicht.

E-Thor hingegen ermöglicht eine präzise, logische Analyse: Dieses Tool kann herausfinden, ob der Vertrag in irgendeiner der möglichen Situationen zu falschen Resultaten führen könnte – auch in Situationen, an die man als Mensch gar nicht gedacht hätte. „Wenn unser Tool sagt, ein Vertrag ist sicher, dann ist er auch wirklich sicher. Dafür gibt es dann einen mathematischen Beweis“, erklärt Schneidewind.

Man kann mit diesem Tool selbstentworfene Verträge analysieren lassen, oder man kann auch die Codes anderer Leute testen, bevor man deren Verträgen zustimmt. „Das ist nicht nur für Security-Profis geeignet, sondern kann problemlos auch von Leuten genutzt werden, die sich zum ersten Mal mit Blockchains und Smart Contracts beschäftigen“, sagt Clara Schneidewind. „Wir stellen diesen Code gratis zur Verfügung.“

Nach Meinung der Wissenschaftlerin wäre es ideal, wenn das Tool direkt in die Ethereum-Software eingebaut würde, die Basis für viele Smart Contracts ist. Dann könnte die Software hochgeladene Smart Contracts automatisch auf Sicherheitsverletzungen im Code überwachen.