Sicherheit für Smart Contracts

„Smarte Verträge“ können das Geschäftsleben auf Blockchain-Basis einfacher machen – doch bisher gab es auch Risiken. Ein Tool der TU Wien kann nun wichtige Sicherheiten garantieren.

In Blau und Grau gehaltenes Symbolbild mit Zeichen und Zahlen, um digitale Verträge darzustellen.

Smart Contracts sind für Online-Transaktionen wichtig.

Verträge sind eine komplizierte Angelegenheit. Oft braucht man eine unabhängige Instanz, die entscheidet, ob die Vertragsbedingungen eingehalten wurden und wer am Ende wem wie viel Geld schuldet. Es gibt aber eine Möglichkeit, diesen Vorgang zu automatisieren: Smart Contracts sind Computercodes, die ähnlich wie eine notarielle Aufsichtsperson die Abläufe überwachen und ganz 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 stellte sich heraus, dass es 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 solche Probleme behebt – und zwar mit mathematischer Präzision. Es kann die Smart Contracts analysieren und mit absoluter Zuverlässigkeit nachweisen, dass der Code keinen Fehler enthält und genau definierte Eigenschaften in jeder Situation erfüllt.

Blockchain mit eingebautem Computercode

Verträge können ein kompliziertes Netz an Klauseln enthalten. Wenn diese Bedingung erfüllt wurde, muss ein bestimmter Betrag von einem Konto auf ein anderes verschoben werden, aber wenn diese Frist verpasst wird, ist jene Pönale fällig. Beliebt ist das etwa bei Crowdfunding-Plattformen: Man verspricht, einen bestimmten Betrag zu zahlen, aber nur, wenn die Anbieterseite bestimmte Zusagen einhält.

Solche Aussagen lassen sich in die Sprache von Computercodes übersetzen. „Für solche Smart Contracts nutzt man Blockchains, wie man sie von Kryptowährungen wie Bitcoin kennt“, erklärt Clara Schneidewind aus der Security-and-Privacy-Forschungsgruppe am Institut für Logic and Computation der TU Wien. 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.

Mit der Blockchain der bekannten Kryptowährung Bitcoin werden in erster Linie ganz gewöhnliche Finanztransaktionen abgewickelt. Es gibt aber auch Kryptowährungen, die mehr Möglichkeiten bieten. Die derzeit zweitwichtigste Kryptowährung mit dem Namen Ethereum erlaubt die Verwendung von Smart Contracts. Man kann also nicht nur Geld überweisen, sondern sich mit anderen Leuten auf einen Code einigen. Dieser Code ist in der Blockchain offen für alle sichtbar und führt dann ganz automatisch die vereinbarten Transaktionen durch.

Millionenbetrug wegen Programmfehler

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

Doch nicht nur das Ausführen von Transaktionen kann man automatisieren, sondern auch das Suchen nach Programmfehlern. „Wir haben ein Tool mit dem Namen eThor entwickelt, mit dem man ganz einfach feststellen kann, ob der Code des Smart Contracts wirklich genau das tut, was er tun soll“, sagt Schneidewind.

Ähnliche Tools zum Untersuchen von Smart Contracts gab es schon bisher, allerdings handelte es sich dabei bloß um sogenannte „Heuristiken“ – das sind Methoden, die mit einigermaßen großer Sicherheit einschätzen können, ob der Vertrag vertrauenswürdig ist. Eine Garantie liefern sie aber nicht. Das eThor-Tool hingegen liefert eine präzise logische Analyse: Es kann herausfinden, ob der Vertrag in irgendeiner auch nur irgendwie möglichen Situation 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. Ideal wäre es, wenn unser Tool direkt in die Ethereum-Software eingebaut werden würde. Dann könnte man jedes Mal, wenn man einen Smart Contract hochlädt, auch sofort automatisch den Hinweis bekommen, ob er eine wichtige Sicherheitseigenschaft verletzt.“

Originalpublikation

Das Originalpaper, das bei der CCS 2020 (Peer Review) akzeptiert wurde, ist hier frei zugänglich nachzulesen.

Mehr über eTHor: https://secpriv.wien/ethor/

Kontakt

Clara Schneidewind, BSc
Institut für Logic and Computation
Technische Universität Wien
clara.schneidewind@tuwien.ac.at

Prof. Matteo Maffei
Institut für Logic and Computation
Technische Universität Wien
T +43-1-58801-184860
matteo.maffei@tuwien.ac.at