Verifikation von Smart Contracts

Dr. Lars Hupel

This article is also available in English

Fatale Fehler

In Ethereum hat es ein fehlerhafter Smart Contract zu trauriger Bekanntheit geschafft: Von einer sogenannten DAO (Decentralized Autonomous Organization) wurde ein achtstelliger USD-Betrag abgezweigt. Zu den historischen Hintergründen schrieben bereits Stefan Tilkov und Marc Jansing. Grundsätzlich dient die DAO als Beispiel für einen Contract, der einerseits eine signifikante Menge von Investitionen verwaltet, andererseits aber fehlerhaft war und dadurch zu schweren finanziellen Verlusten führte.

Es gibt keinen Grund zur Annahme, dass die bisher bekannte Reihe von spektakulären Bugs nicht noch weiter fortgesetzt werden könnte. Philosophische Ausführungen darüber, ob der Code sakrosankt ist und solche Bugs dann eben doch Features sind, will ich in diesem Artikel einmal ausklammern, dazu haben sich schon Andere geäußert. Wichtig ist aber, festzuhalten, dass es im Gegensatz zu papierbasierten Verträgen kein Gericht gibt, welches einen Smart Contract auslegen und korrigieren könnte.

Es gibt eine ganze Reihe weiterer Smart Contracts, die hohe Transaktionsmengen aufweisen und/oder einen hohen Kontostand haben und dadurch auch besonders attraktiv für Angriffsversuche sind.

Für ersteres hat Blockspur eine Liste aufbereitet. Stand Februar 2019 weist diese Liste insgesamt sechs Smart Contracts auf, bei denen die durchschnittliche Summe monatlich eingehender Transaktionen 10 Millionen USD übersteigen. Der höchste Contract hat dabei Monatseinnahmen von knapp über 47 Millionen; es handelt sich dabei um einen Contract der Tauschbörse Kraken.

Zum zweiten kann man auf Etherscan die Liste der Adressen ansehen, die derzeit den höchsten Kontostand haben. Im Februar 2019 war das mit Abstand der Vertrag für das ERC-20-Token Wrapped Ether; dieser kontrolliert derzeit über 2% aller existierenden Ether, was einem Gegenwert von etwa 320 Millionen USD entspricht. Man kann hier mit Fug und Recht von einem Contract sprechen, der too big to fail ist.

Ein Contract, der in die Blockchain ausgerollt wird, liegt normalerweise nur für die Erstellerin im Quelltext (meist Solidity) vor. Die Blockchain und alle anderen Teilnehmer*innen sehen nur den Bytecode der EVM (Ethereum VM). Konzeptuell ist das vergleichbar mit Java-Code, der in JVM-Bytecode kompiliert wird. Etherscan bietet darüber hinaus die Möglichkeit, den Quelltext zu veröffentlichen und prüft, ob dieser nach Kompilierung identisch zum in der Blockchain vorhandenen Bytecode ist. Im Falle von Wrapped Ether ist damit ersichtlich, dass es sich um einen Contract mit etwa 80 Zeilen (zuzüglich Lizenz) handelt, der der offiziellen ERC-20-Schablone ähnelt.

Neben ERC-20-Tokens und Börsen gibt es noch eine dritte Art von häufig genutzten Contracts: die sogenannten Wallets. Parity ist ein Beispiel einer Wallet, die zusätzliche Funktionen anbietet, wie etwa die Verwaltung von mehreren Zeichnungsberechtigten.

Eine andere Analyse kommt zwar zu dem Schluss, dass nur 1% Prozent aller Smart Contracts mehr als 100 Aufrufe erhielten. Trotzdem enthielten etwas mehr als ein Drittel aller Ethereum-Transaktionen Vertragsaufrufe.

Komplette Korrektheit

Das Problem ist, dass ein Smart Contract in Stein gemeißelt ist und nachträgliche Korrekturen unmöglich sind. Wie uns die Erfahrung lehrt, enthält Software Fehler. Viel schlimmer: Meistens fehlt eine Spezifikation sogar ganz. Kombiniert man diese Faktoren mit der Tatsache, dass mit diesen Verträgen viel Geld gehandelt wird, erhält man eine besonders explosive Mischung.

Glücklicherweise kennt man in der Softwareentwicklung einige Verfahren, um die Code-Qualität zu verbessern. Die einfachste und günstigste Option dafür sind Tests. Alexey Novakov hat bereits über das Truffle Framework berichtet, ein Framework, mit dem sich Ethereum-Verträge nicht nur erstellen und verwalten, sondern auch testen lassen. Man kann sich also durchaus vorstellen, gängige Ansätze wie zum Beispiel TDD auch auf Smart Contracts anzuwenden. Sogar Testabdeckung kann bei Solidity gemessen werden.

Lassen wir für einen Moment den Blockchain-Kontext links liegen. Mit Tests lässt sich nur die Abwesenheit bestimmter Fehlern zeigen, aber nie die Abwesenheit aller Fehler. Wie Edsger W. Dijkstra dazu in seiner ACM Turing Lecture bereits 1972 sagte:

Program testing can be a very effective way to show the presence of bugs, but is hopelessly inadequate for showing their absence.

Wie kann man aber nun die Abwesenheit von Bugs zeigen? Man muss es beweisen. Dazu gibt es eine ganze Reihe von Verfahren, die mathematisch-logisch sicherstellen, dass sich bestimmter Programmcode an eine bestimmte Spezifikation hält. An sich ist das nichts Neues, denn in verschiedenen (objektorientierten) Programmiersprachen ist dieses Konzept als vertragsbasierte Programmierung bekannt. Der Begriff Vertrag hat hier nichts mit Smart Contracts zu tun! Stattdessen geht es in diesem Kontext darum, allgemein die Korrektheit von Funktionen zu prüfen, unabhängig davon, ob diese Funktionen auf der Blockchain oder einer JVM laufen.

Systeme für vertragsbasierte Programmierung gibt es für zahlreiche Programmiersprachen, darunter Ada und Eiffel als Pioniere, aber auch Java, C# und C++.

@Requires("x >= 0")
@Ensures("result >= 0")
static double sqrt(double x);

Wirklich hilfreich sind die allermeisten dieser Tools für Verifikationszwecke aber nicht, denn es geschieht im Regelfall nur eine Laufzeitprüfung. Man möchte aber bereits vor der Laufzeit wissen, dass die Spezifikation eingehalten wird. Ich schrieb über dieses Prinzip und ein bestimmtes Tool bereits an anderer Stelle. Kurz zusammengefasst: es geht, aber man muss sich dafür etwas mehr anstrengen. Im Falle von Java ist die Situation eher mau. JetBrains bringt mit der @Contract-Annotation einen eigenen primitiven Mechanismus mit, der aber nur sehr eingeschränkte Aussagen über die Programmsemantik erlaubt:

The @Contract annotation lets you specify a set of rules (a contract) that a method must follow. If the contract is violated, IntelliJ IDEA reports a problem.

Für Smart Contracts, mit denen Millionen von Euro verschoben werden, reichen aber Null-Checks nicht aus. Man muss schwerere Geschütze auffahren:

1. einen komplett spezifizierten Geschäftsfall
2. eine Smart-Contract-Programmiersprache mit definierter Semantik
3. eine Smart-Contract-VM mit definierter Semantik
4. einen korrekten Compiler zu VM-Bytecode
5. Nodes, die die VM korrekt implementieren

Während ein solcher Stack in industriellen Anwendungen bereits existiert, ist die Blockchain-Welt davon noch weit entfernt. Ich möchte hier einmal zusammenfassen, was bereits existiert, und prognostizieren, wohin die Reise wahrscheinlich gehen wird.

Die EVM selbst liegt bereits in mehreren System formalisiert vor (Isabelle, Imandra, K). Einige dieser Formalisierungen sind gleichzeitig auch ausführbar, das heißt, sie lassen sich in Programmcode transformieren, womit Punkt 5 umgesetzt wäre. Die größte Schwäche besteht allerdings momentan in den Punkten 2 und 4. Die am häufigsten genutzte Sprache für Ethereum-Contracts, Solidity, ist notorisch schwierig zu verstehen. Das belegt auch die Liste der bekannten Angriffsvektoren. Bei einem guten Sprachdesign sollten solche Listen sehr klein sein. Das ist auch der Grund, warum man üblicherweise keine Webapplikationen in C, sondern in Hochsprachen implementiert.

Akademisch wird dieses Feld aber durchaus bearbeitet. 2019 findet zum dritten Mal ein Workshop on Trusted Smart Contracts statt. Runtime Verification arbeitet an der Verifikation von ERC-20-Tokens und einem Prototyp einer Solidity-Semantik. Durch diese Analysen wurden bereits in einfachen Smart Contracts subtile Fehler aufgedeckt, z.B. > statt < oder =+ statt +=.

Auch im Bereich des Sprachdesigns gibt es durchaus Fortschritte. IOHK hat als Basis für ihre neue Smart-Contract-Sprache Plutus eine Variante des typisierten Lambda-Kalküls gewählt. Dieser Kalkül ist wissenschaftlich sehr gut verstanden und wurde für die Zwecke von Plutus in der Beweissprache Agda formalisiert. Die Hochsprache selbst ist eine eingebettete DSL in Haskell, in der bewusst auf bestimmte, schwierig zu analysierende Konstrukte verzichtet worden ist. Noch existiert zwar keine Toolchain für die Verifikation von Verträgen; dennoch wurde mit der Wahl dieser Technologien der Grundstein dafür geschaffen.

Einen Schritt weiter geht dabei die Zwischensprache Scilla, die mit dem Beweissystem Coq formalisiert ist. Dort gibt es bereits Ansätze, Beweise über Verträge zu führen. Im Paper von Sergey, Kumar und Hobor wird als Beispiel ein Vertrag für Crowdfunding-Plattformen entwickelt, die ähnlich wie Kickstarter funktionieren. Kurz gesagt sollen beliebige Backer Spenden einzahlen können. Wenn die Kampagne erfolgreich ist, erhält der Owner sämtliche Spenden. Andernfalls können Backer ihr Geld zurück erhalten. In der Beweissprache ist diese letzte Anforderung so formuliert:

Theorem can_claim_back id b d st bc:
  (* (a) The backer b has donated d, so the contract holds
     that record in its state *)
  donated b d st →
  (* (b) The campaign has not been funded. *)
  ¬funded (state st) →
  (* (c) Balance is small: not reached the goal. *)
  balance st < (get_goal (state st)) →
  (* (d) Block number exceeds the deadline. *)
  get_max_block (state st) < block_num bc →
  (* (conclusion) Backer b can get their donation back. *)
  ∃(m : message),
    sender m == b ∧
      out (step_prot c st bc m) = Some (Msg d id b 0 ok_msg)

Dabei handelt es sich nur um die Aussage, noch nicht um den Beweis, den die Autoren leider nicht öffentlich zur Verfügung gestellt haben. Sie behaupten immerhin, dass dieser nur etwa zehn Zeilen lang ist. Trotzdem besteht hier das Problem, dass Beweise in einer für Programmierer*innen ungewohnten Sprache durchgeführt werden müssen. Ferner fehlt bei Scilla noch eine realistische Implementierung der Sprache auf einer öffentlichen Blockchain.

Adäquater Aufwand?

Bleibt die Frage zu klären, ob es den Aufwand wert ist. In der Industrie gibt es bereits vereinzelte Verifikationsprojekte signifikanter Ausmaße. Ein Leuchtturmprojekt für das Isabelle-System ist die Verifikation des Betriebssystemkernels seL4. Im wegweisenden Artikel von 2009 schreiben Klein et al.:

Complete formal verification is the only known way to guarantee that a system is free of programming errors. We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, and hardware, and we used a unique design approach that fuses formal and operating systems techniques. […] Functional correctness means here that the implementation always strictly follows our high-level abstract specification of kernel behaviour. This encompasses traditional design and implementation safety properties such as the kernel will never crash, and it will never perform an unsafe operation. It also proves much more: we can predict precisely how the kernel will behave in every possible situation.

Dieser hohe Standard an Zusicherungen ist auch erstrebenswert, wenn man mit hohen Geldbeträgen ohne juristischem doppelten Boden hantiert. Er hat aber auch seinen Preis:

The cost of the proof is higher, in total about 20 [person years]. This includes significant research and about 9 py invested in formal language frameworks, proof tools, proof automation, theorem prover extensions and libraries. The total effort for the seL4-specific proof was 11 py.

Die Autoren führen weiter aus, dass die übliche Schätzregel, um die Common Criteria EAL6 zu erfüllen, 10.000 USD pro Zeile Code beträgt. Dabei ist EAL6 ein niedrigerer Standard als formale Verifikation mit Isabelle, wie im seL4-Projekt geschehen.

Es ist also sorgfältig abzuwägen, was teurer ist: die kostspielige Entwicklung von Smart Contracts abgesichert durch formale Methoden oder der kostspielige potenzielle Verlust von hohen Geldbeträgen. Bei Systemen wie seL4, die als Microkernel in zahlreichen Geräten verwendet werden, kommen bei der Abwägung noch Menschenleben dazu, die bei fehlerhafter Software gefährdet sein könnten:

More than 30 years of research in theorem proving has addressed this issue, and we can now achieve a degree of trustworthiness of formal, machine-checked proof that far surpasses the confidence levels we rely on in engineering or mathematics for our daily survival.

Große Teile des Papers sind auch ohne sich in theoretischer Informatik auszukennen nachvollziehbar und enthalten einige wertvolle Informationen über den Stand der Technik.

Meta-Methoden

Unabhängig von den obigen Überlegungen kann man sich auch vorstellen, Beweise selbst in die Blockchain zu integrieren. Beweise sind wie viele andere mathematische Probleme schwer durchzuführen, aber einfach zu prüfen. Manchmal werden solche Probleme auch als Einwegfunktionen bezeichnet. Hash-Algorithmen sind zum Beispiel absichtlich so konstruiert, dass sich zwar der Hash einfach aus dem Text berechnen lässt, aber nicht umgekehrt der Text aus dem Hash. Mit Beweisen verhält es sich ähnlich: Ist ein Beweis gegeben, lässt sich schnell nachvollziehen, ob eine bestimmte Aussage bewiesen worden ist, aber der umgekehrte Weg ist ein unentscheidbares Problem.

In der Vergangenheit gab es deswegen schon Versuche, für Beweise Belohnungen auszuschreiben. Ein solches Projekt war zum Beispiel der Proof Market, wo man eine beliebige Behauptung aufstellen und mit einer Prämie (Bitcoin) versehen konnte. Wer die Behauptung erfolgreich bewiesen hat, erhielt die Prämie. Leider wurden im wesentlichen nur fehlerhafte Beweise eingereicht, die bekannte Lücken im Checker ausgenutzt haben. Die Seite wurde dementsprechend 2015 geschlossen.

Ein weiteres Projekt – Qeditas von IOHK – wollte das Aufbauen einer Bibliothek von formalisierter Mathematik antreiben. Seit dem Launch ist allerdings nicht viel passiert.

Der Gedanke, den Entwicklungsprozess von Smart Contracts von ihrer Verifikation abzukoppeln – letztere vielleicht sogar zu crowdsourcen –, ist also bis auf weiteres nur eine Vision.