Zum Hauptinhalt springen
Change page

Formale Verifikation von Smart Contracts

Seite bearbeiten (opens in a new tab)

Smart Contracts machen es möglich, dezentrale, vertrauenslose und robuste Anwendungen zu erstellen, die neue Anwendungsfälle einführen und Mehrwert für Benutzer erschließen. Da Smart Contracts große Werte verwalten, ist Sicherheit ein kritischer Aspekt für Entwickler.

Die formale Verifikation ist eine der empfohlenen Techniken zur Verbesserung der Sicherheit von Smart Contracts. Die formale Verifikation, die formale Methoden (opens in a new tab) zur Spezifikation, zum Entwurf und zur Verifikation von Programmen verwendet, wird seit Jahren eingesetzt, um die Korrektheit kritischer Hardware- und Softwaresysteme sicherzustellen.

Wenn sie bei Smart Contracts angewendet wird, kann die formale Verifikation beweisen, dass die Geschäftslogik eines Vertrags einer vordefinierten Spezifikation entspricht. Im Vergleich zu anderen Methoden zur Beurteilung der Korrektheit von Vertragscode, wie z. B. Tests, bietet die formale Verifikation stärkere Garantien dafür, dass ein Smart Contract funktional korrekt ist.

Was ist formale Verifikation?

Formale Verifikation bezieht sich auf den Prozess der Bewertung der Korrektheit eines Systems in Bezug auf eine formale Spezifikation. Einfacher ausgedrückt ermöglicht uns die formale Verifikation zu überprüfen, ob das Verhalten eines Systems bestimmte Anforderungen erfüllt (d. h. es tut, was wir wollen).

Erwartete Verhaltensweisen des Systems (in diesem Fall eines Smart Contracts) werden mithilfe formaler Modellierung beschrieben, während Spezifikationssprachen die Erstellung formaler Eigenschaften ermöglichen. Techniken der formalen Verifikation können dann verifizieren, dass die Implementierung eines Vertrags seiner Spezifikation entspricht, und einen mathematischen Beweis für dessen Korrektheit ableiten. Wenn ein Vertrag seine Spezifikation erfüllt, wird er als „funktional korrekt“, „correct by design“ oder „correct by construction“ beschrieben.

Was ist ein formales Modell?

In der Informatik ist ein formales Modell (opens in a new tab) eine mathematische Beschreibung eines Rechenprozesses. Programme werden in mathematische Funktionen (Gleichungen) abstrahiert, wobei das Modell beschreibt, wie Ausgaben von Funktionen bei einer bestimmten Eingabe berechnet werden.

Formale Modelle bieten eine Abstraktionsebene, über die die Analyse des Verhaltens eines Programms bewertet werden kann. Die Existenz formaler Modelle ermöglicht die Erstellung einer formalen Spezifikation, die gewünschte Eigenschaften des betreffenden Modells beschreibt.

Für die Modellierung von Smart Contracts zur formalen Verifikation werden verschiedene Techniken verwendet. Einige Modelle werden beispielsweise verwendet, um über das High-Level-Verhalten eines Smart Contracts nachzudenken. Diese Modellierungstechniken wenden eine Black-Box-Sicht auf Smart Contracts an und betrachten sie als Systeme, die Eingaben akzeptieren und basierend auf diesen Eingaben Berechnungen ausführen.

High-Level-Modelle konzentrieren sich auf die Beziehung zwischen Smart Contracts und externen Akteuren, wie z. B. Externally Owned Accounts (EOAs), Vertragskonten und der Blockchain-Umgebung. Solche Modelle sind nützlich, um Eigenschaften zu definieren, die festlegen, wie sich ein Vertrag als Reaktion auf bestimmte Benutzerinteraktionen verhalten soll.

Umgekehrt konzentrieren sich andere formale Modelle auf das Low-Level-Verhalten eines Smart Contracts. Während High-Level-Modelle dabei helfen können, über die Funktionalität eines Vertrags nachzudenken, erfassen sie möglicherweise keine Details über die internen Abläufe der Implementierung. Low-Level-Modelle wenden eine White-Box-Sicht auf die Programmanalyse an und stützen sich auf Low-Level-Darstellungen von Smart-Contract-Anwendungen, wie z. B. Programm-Traces und Kontrollflussgraphen (opens in a new tab), um über Eigenschaften nachzudenken, die für die Ausführung eines Vertrags relevant sind.

Low-Level-Modelle gelten als ideal, da sie die tatsächliche Ausführung eines Smart Contracts in der Ausführungsumgebung von Ethereum (d. h. der EVM) darstellen. Low-Level-Modellierungstechniken sind besonders nützlich, um kritische Sicherheitseigenschaften in Smart Contracts zu etablieren und potenzielle Schwachstellen zu erkennen.

Was ist eine formale Spezifikation?

Eine Spezifikation ist einfach eine technische Anforderung, die ein bestimmtes System erfüllen muss. In der Programmierung repräsentieren Spezifikationen allgemeine Vorstellungen über die Ausführung eines Programms (d. h. was das Programm tun soll).

Im Kontext von Smart Contracts beziehen sich formale Spezifikationen auf Eigenschaften – formale Beschreibungen der Anforderungen, die ein Vertrag erfüllen muss. Solche Eigenschaften werden als „Invarianten“ beschrieben und stellen logische Zusicherungen über die Ausführung eines Vertrags dar, die unter allen möglichen Umständen ohne Ausnahmen wahr bleiben müssen.

Daher können wir uns eine formale Spezifikation als eine Sammlung von in einer formalen Sprache verfassten Aussagen vorstellen, die die beabsichtigte Ausführung eines Smart Contracts beschreiben. Spezifikationen decken die Eigenschaften eines Vertrags ab und definieren, wie sich der Vertrag unter verschiedenen Umständen verhalten soll. Der Zweck der formalen Verifikation besteht darin, festzustellen, ob ein Smart Contract diese Eigenschaften (Invarianten) besitzt und dass diese Eigenschaften während der Ausführung nicht verletzt werden.

Formale Spezifikationen sind entscheidend für die Entwicklung sicherer Implementierungen von Smart Contracts. Verträge, die Invarianten nicht implementieren oder deren Eigenschaften während der Ausführung verletzt werden, sind anfällig für Schwachstellen, die die Funktionalität beeinträchtigen oder böswillige Exploits verursachen können.

Arten formaler Spezifikationen für Smart Contracts

Formale Spezifikationen ermöglichen mathematisches Schlussfolgern über die Korrektheit der Programmausführung. Wie bei formalen Modellen können formale Spezifikationen entweder High-Level-Eigenschaften oder das Low-Level-Verhalten einer Vertragsimplementierung erfassen.

Formale Spezifikationen werden unter Verwendung von Elementen der Programmlogik (opens in a new tab) abgeleitet, die ein formales Schlussfolgern über die Eigenschaften eines Programms ermöglichen. Eine Programmlogik verfügt über formale Regeln, die (in mathematischer Sprache) das erwartete Verhalten eines Programms ausdrücken. Bei der Erstellung formaler Spezifikationen werden verschiedene Programmlogiken verwendet, darunter Erreichbarkeitslogik (opens in a new tab), Temporallogik (opens in a new tab) und Hoare-Logik (opens in a new tab).

Formale Spezifikationen für Smart Contracts können grob in High-Level- oder Low-Level-Spezifikationen eingeteilt werden. Unabhängig davon, zu welcher Kategorie eine Spezifikation gehört, muss sie die Eigenschaft des zu analysierenden Systems angemessen und eindeutig beschreiben.

High-Level-Spezifikationen

Wie der Name schon sagt, beschreibt eine High-Level-Spezifikation (auch „modellorientierte Spezifikation“ genannt) das High-Level-Verhalten eines Programms. High-Level-Spezifikationen modellieren einen Smart Contract als endlichen Automaten (opens in a new tab) (Finite State Machine, FSM), der durch die Ausführung von Operationen zwischen Zuständen wechseln kann, wobei Temporallogik verwendet wird, um formale Eigenschaften für das FSM-Modell zu definieren.

Temporallogiken (opens in a new tab) sind „Regeln zum Schlussfolgern über zeitlich qualifizierte Aussagen (z. B. ‚Ich bin immer hungrig‘ oder ‚Ich werde irgendwann hungrig sein‘)“. Bei der Anwendung auf die formale Verifikation werden Temporallogiken verwendet, um Zusicherungen über das korrekte Verhalten von als Zustandsautomaten modellierten Systemen zu treffen. Insbesondere beschreibt eine Temporallogik die zukünftigen Zustände, in denen sich ein Smart Contract befinden kann, und wie er zwischen Zuständen wechselt.

High-Level-Spezifikationen erfassen im Allgemeinen zwei kritische temporale Eigenschaften für Smart Contracts: Sicherheit (Safety) und Lebendigkeit (Liveness). Sicherheitseigenschaften repräsentieren die Idee, dass „niemals etwas Schlimmes passiert“, und drücken normalerweise Invarianz aus. Eine Sicherheitseigenschaft kann allgemeine Softwareanforderungen definieren, wie z. B. die Freiheit von Deadlocks (opens in a new tab), oder domänenspezifische Eigenschaften für Verträge ausdrücken (z. B. Invarianten zur Zugriffskontrolle für Funktionen, zulässige Werte von Zustandsvariablen oder Bedingungen für Token-Transfers).

Nehmen wir zum Beispiel diese Sicherheitsanforderung, die Bedingungen für die Verwendung von transfer() oder transferFrom() in ERC-20-Token-Verträgen abdeckt: „Der Kontostand eines Senders ist niemals niedriger als die angeforderte Menge an zu sendenden Token.“ Diese natürlichsprachliche Beschreibung einer Vertragsinvariante kann in eine formale (mathematische) Spezifikation übersetzt werden, die dann streng auf ihre Gültigkeit überprüft werden kann.

Lebendigkeitseigenschaften sichern zu, dass „irgendwann etwas Gutes passiert“, und betreffen die Fähigkeit eines Vertrags, durch verschiedene Zustände fortzuschreiten. Ein Beispiel für eine Lebendigkeitseigenschaft ist „Liquidität“, die sich auf die Fähigkeit eines Vertrags bezieht, seine Guthaben auf Anfrage an Benutzer zu transferieren. Wenn diese Eigenschaft verletzt wird, könnten Benutzer keine im Vertrag gespeicherten Vermögenswerte abheben, wie es beim Parity-Wallet-Vorfall (opens in a new tab) der Fall war.

Low-Level-Spezifikationen

High-Level-Spezifikationen nehmen als Ausgangspunkt ein Finite-State-Modell eines Vertrags und definieren gewünschte Eigenschaften dieses Modells. Im Gegensatz dazu modellieren Low-Level-Spezifikationen (auch „eigenschaftsorientierte Spezifikationen“ genannt) Programme (Smart Contracts) oft als Systeme, die eine Sammlung mathematischer Funktionen umfassen, und beschreiben das korrekte Verhalten solcher Systeme.

Einfacher ausgedrückt analysieren Low-Level-Spezifikationen Programm-Traces und versuchen, Eigenschaften eines Smart Contracts über diese Traces zu definieren. Traces beziehen sich auf Sequenzen von Funktionsausführungen, die den Zustand eines Smart Contracts ändern; daher helfen Low-Level-Spezifikationen dabei, Anforderungen für die interne Ausführung eines Vertrags zu spezifizieren.

Formale Low-Level-Spezifikationen können entweder als Hoare-artige Eigenschaften oder als Invarianten auf Ausführungspfaden angegeben werden.

Hoare-artige Eigenschaften

Die Hoare-Logik (opens in a new tab) bietet eine Reihe formaler Regeln zum Schlussfolgern über die Korrektheit von Programmen, einschließlich Smart Contracts. Eine Hoare-artige Eigenschaft wird durch ein Hoare-Tripel {P}c{Q} dargestellt, wobei c ein Programm ist und P sowie Q Prädikate über den Zustand von c (d. h. dem Programm) sind, die formal als Vorbedingungen (Preconditions) bzw. Nachbedingungen (Postconditions) beschrieben werden.

Eine Vorbedingung ist ein Prädikat, das die für die korrekte Ausführung einer Funktion erforderlichen Bedingungen beschreibt; Benutzer, die den Vertrag aufrufen, müssen diese Anforderung erfüllen. Eine Nachbedingung ist ein Prädikat, das die Bedingung beschreibt, die eine Funktion bei korrekter Ausführung herstellt; Benutzer können erwarten, dass diese Bedingung nach dem Aufruf der Funktion wahr ist. Eine Invariante in der Hoare-Logik ist ein Prädikat, das durch die Ausführung einer Funktion erhalten bleibt (d. h. es ändert sich nicht).

Hoare-artige Spezifikationen können entweder partielle Korrektheit oder totale Korrektheit garantieren. Die Implementierung einer Vertragsfunktion ist „partiell korrekt“, wenn die Vorbedingung vor der Ausführung der Funktion wahr ist und, falls die Ausführung terminiert, auch die Nachbedingung wahr ist. Ein Beweis für die totale Korrektheit wird erbracht, wenn eine Vorbedingung vor der Ausführung der Funktion wahr ist, die Ausführung garantiert terminiert und, wenn dies der Fall ist, die Nachbedingung wahr ist.

Einen Beweis für die totale Korrektheit zu erhalten, ist schwierig, da sich einige Ausführungen vor der Terminierung verzögern oder überhaupt nicht terminieren können. Allerdings ist die Frage, ob die Ausführung terminiert, wohl ein strittiger Punkt, da der Gas-Mechanismus von Ethereum Endlosschleifen in Programmen verhindert (die Ausführung terminiert entweder erfolgreich oder endet aufgrund eines „Out-of-Gas“-Fehlers).

Smart-Contract-Spezifikationen, die mithilfe der Hoare-Logik erstellt wurden, weisen Vorbedingungen, Nachbedingungen und Invarianten auf, die für die Ausführung von Funktionen und Schleifen in einem Vertrag definiert sind. Vorbedingungen beinhalten oft die Möglichkeit fehlerhafter Eingaben in eine Funktion, wobei Nachbedingungen die erwartete Reaktion auf solche Eingaben beschreiben (z. B. das Auslösen einer bestimmten Ausnahme). Auf diese Weise sind Hoare-artige Eigenschaften effektiv, um die Korrektheit von Vertragsimplementierungen sicherzustellen.

Viele Frameworks für die formale Verifikation verwenden Hoare-artige Spezifikationen, um die semantische Korrektheit von Funktionen zu beweisen. Es ist auch möglich, Hoare-artige Eigenschaften (als Zusicherungen) direkt zum Vertragscode hinzuzufügen, indem die Anweisungen require und assert in Solidity verwendet werden.

require-Anweisungen drücken eine Vorbedingung oder Invariante aus und werden oft verwendet, um Benutzereingaben zu validieren, während assert eine für die Sicherheit notwendige Nachbedingung erfasst. Beispielsweise kann eine ordnungsgemäße Zugriffskontrolle für Funktionen (ein Beispiel für eine Sicherheitseigenschaft) erreicht werden, indem require als Vorbedingungsprüfung der Identität des aufrufenden Kontos verwendet wird. Ebenso kann eine Invariante für zulässige Werte von Zustandsvariablen in einem Vertrag (z. B. die Gesamtzahl der im Umlauf befindlichen Token) vor Verletzungen geschützt werden, indem assert verwendet wird, um den Zustand des Vertrags nach der Funktionsausführung zu bestätigen.

Trace-Level-Eigenschaften

Trace-basierte Spezifikationen beschreiben Operationen, die einen Vertrag zwischen verschiedenen Zuständen überführen, sowie die Beziehungen zwischen diesen Operationen. Wie bereits erklärt, sind Traces Sequenzen von Operationen, die den Zustand eines Vertrags auf eine bestimmte Weise ändern.

Dieser Ansatz beruht auf dem Modell von Smart Contracts als Zustandsübergangssysteme mit einigen vordefinierten Zuständen (beschrieben durch Zustandsvariablen) zusammen mit einer Menge vordefinierter Übergänge (beschrieben durch Vertragsfunktionen). Darüber hinaus wird oft ein Kontrollflussgraph (opens in a new tab) (Control Flow Graph, CFG), der eine grafische Darstellung des Ausführungsflusses eines Programms ist, zur Beschreibung der operativen Semantik eines Vertrags verwendet. Hierbei wird jeder Trace als Pfad auf dem Kontrollflussgraphen dargestellt.

In erster Linie werden Trace-Level-Spezifikationen verwendet, um über Muster der internen Ausführung in Smart Contracts nachzudenken. Durch die Erstellung von Trace-Level-Spezifikationen sichern wir die zulässigen Ausführungspfade (d. h. Zustandsübergänge) für einen Smart Contract zu. Mithilfe von Techniken wie der symbolischen Ausführung können wir formal verifizieren, dass die Ausführung niemals einem Pfad folgt, der nicht im formalen Modell definiert ist.

Verwenden wir das Beispiel eines DAO-Vertrags, der über einige öffentlich zugängliche Funktionen verfügt, um Trace-Level-Eigenschaften zu beschreiben. Hier nehmen wir an, dass der DAO-Vertrag es Benutzern ermöglicht, die folgenden Operationen auszuführen:

  • Gelder einzahlen

  • Über einen Vorschlag abstimmen, nachdem Gelder eingezahlt wurden

  • Eine Rückerstattung beanspruchen, wenn sie nicht über einen Vorschlag abstimmen

Beispielhafte Trace-Level-Eigenschaften könnten sein: „Benutzer, die keine Gelder einzahlen, können nicht über einen Vorschlag abstimmen“ oder „Benutzer, die nicht über einen Vorschlag abstimmen, sollten immer in der Lage sein, eine Rückerstattung zu beanspruchen“. Beide Eigenschaften sichern bevorzugte Ausführungssequenzen zu (eine Abstimmung kann nicht vor der Einzahlung von Geldern erfolgen und die Beanspruchung einer Rückerstattung kann nicht nach der Abstimmung über einen Vorschlag erfolgen).

Techniken zur formalen Verifikation von Smart Contracts

Model Checking

Model Checking ist eine Technik der formalen Verifikation, bei der ein Algorithmus ein formales Modell eines Smart Contracts gegen seine Spezifikation prüft. Beim Model Checking werden Smart Contracts oft als Zustandsübergangssysteme dargestellt, während Eigenschaften zu zulässigen Vertragszuständen mithilfe von Temporallogik definiert werden.

Model Checking erfordert die Erstellung einer abstrakten mathematischen Darstellung eines Systems (d. h. eines Vertrags) und den Ausdruck von Eigenschaften dieses Systems mithilfe von Formeln, die in der Aussagenlogik (opens in a new tab) verwurzelt sind. Dies vereinfacht die Aufgabe des Model-Checking-Algorithmus, nämlich zu beweisen, dass ein mathematisches Modell eine gegebene logische Formel erfüllt.

Model Checking in der formalen Verifikation wird in erster Linie verwendet, um temporale Eigenschaften zu bewerten, die das Verhalten eines Vertrags im Laufe der Zeit beschreiben. Temporale Eigenschaften für Smart Contracts umfassen Sicherheit und Lebendigkeit, die wir zuvor erklärt haben.

Beispielsweise kann eine Sicherheitseigenschaft im Zusammenhang mit der Zugriffskontrolle (z. B. Nur der Eigentümer des Vertrags kann selfdestruct aufrufen) in formaler Logik geschrieben werden. Danach kann der Model-Checking-Algorithmus verifizieren, ob der Vertrag diese formale Spezifikation erfüllt.

Model Checking verwendet die Zustandsraumexploration, bei der alle möglichen Zustände eines Smart Contracts konstruiert und versucht wird, erreichbare Zustände zu finden, die zu Eigenschaftsverletzungen führen. Dies kann jedoch zu einer unendlichen Anzahl von Zuständen führen (bekannt als das „Zustandsexplosionsproblem“), weshalb Model Checker auf Abstraktionstechniken angewiesen sind, um eine effiziente Analyse von Smart Contracts zu ermöglichen.

Theorembeweisen

Theorembeweisen ist eine Methode des mathematischen Schlussfolgerns über die Korrektheit von Programmen, einschließlich Smart Contracts. Es beinhaltet die Transformation des Modells eines Vertragssystems und seiner Spezifikationen in mathematische Formeln (logische Aussagen).

Das Ziel des Theorembeweisens ist es, die logische Äquivalenz zwischen diesen Aussagen zu verifizieren. „Logische Äquivalenz“ (auch „logische Biimplikation“ genannt) ist eine Art von Beziehung zwischen zwei Aussagen, bei der die erste Aussage genau dann wahr ist, wenn die zweite Aussage wahr ist.

Die erforderliche Beziehung (logische Äquivalenz) zwischen Aussagen über das Modell eines Vertrags und seine Eigenschaft wird als beweisbare Aussage (Theorem genannt) formuliert. Mithilfe eines formalen Inferenzsystems kann der automatisierte Theorembeweiser die Gültigkeit des Theorems verifizieren. Mit anderen Worten, ein Theorembeweiser kann schlüssig beweisen, dass das Modell eines Smart Contracts genau seinen Spezifikationen entspricht.

Während Model Checking Verträge als Übergangssysteme mit endlichen Zuständen modelliert, kann das Theorembeweisen die Analyse von Systemen mit unendlichen Zuständen handhaben. Dies bedeutet jedoch, dass ein automatisierter Theorembeweiser nicht immer wissen kann, ob ein logisches Problem „entscheidbar“ ist oder nicht.

Infolgedessen ist oft menschliche Unterstützung erforderlich, um den Theorembeweiser bei der Ableitung von Korrektheitsbeweisen zu leiten. Der Einsatz menschlicher Arbeit beim Theorembeweisen macht die Anwendung teurer als das Model Checking, das vollständig automatisiert ist.

Symbolische Ausführung

Die symbolische Ausführung ist eine Methode zur Analyse eines Smart Contracts durch die Ausführung von Funktionen unter Verwendung symbolischer Werte (z. B. x > 5) anstelle von konkreten Werten (z. B. x == 5). Als Technik der formalen Verifikation wird die symbolische Ausführung verwendet, um formal über Trace-Level-Eigenschaften im Code eines Vertrags nachzudenken.

Die symbolische Ausführung stellt einen Ausführungs-Trace als mathematische Formel über symbolische Eingabewerte dar, die auch als Pfadprädikat bezeichnet wird. Ein SMT-Solver (opens in a new tab) wird verwendet, um zu überprüfen, ob ein Pfadprädikat „erfüllbar“ ist (d. h. es existiert ein Wert, der die Formel erfüllen kann). Wenn ein anfälliger Pfad erfüllbar ist, generiert der SMT-Solver einen konkreten Wert, der die Ausführung in Richtung dieses Pfades lenkt.

Angenommen, die Funktion eines Smart Contracts nimmt als Eingabe einen uint-Wert (x) und wird rückgängig gemacht (reverts), wenn x größer als 5 und gleichzeitig kleiner als 10 ist. Einen Wert für x zu finden, der den Fehler mithilfe eines normalen Testverfahrens auslöst, würde das Durchlaufen von Dutzenden von Testfällen (oder mehr) erfordern, ohne die Gewissheit, tatsächlich eine fehlerverursachende Eingabe zu finden.

Umgekehrt würde ein Tool zur symbolischen Ausführung die Funktion mit dem symbolischen Wert ausführen: X > 5 ∧ X < 10 (d. h. x ist größer als 5 UND x ist kleiner als 10). Das zugehörige Pfadprädikat x = X > 5 ∧ X < 10 würde dann einem SMT-Solver zur Lösung übergeben. Wenn ein bestimmter Wert die Formel x = X > 5 ∧ X < 10 erfüllt, wird der SMT-Solver ihn berechnen – beispielsweise könnte der Solver 7 als Wert für x ausgeben.

Da die symbolische Ausführung auf Eingaben in ein Programm angewiesen ist und die Menge der Eingaben zur Erkundung aller erreichbaren Zustände potenziell unendlich ist, handelt es sich immer noch um eine Form des Testens. Wie im Beispiel gezeigt, ist die symbolische Ausführung jedoch effizienter als reguläres Testen, um Eingaben zu finden, die Eigenschaftsverletzungen auslösen.

Darüber hinaus erzeugt die symbolische Ausführung weniger falsch-positive Ergebnisse als andere eigenschaftsbasierte Techniken (z. B. Fuzzing), die zufällig Eingaben für eine Funktion generieren. Wenn während der symbolischen Ausführung ein Fehlerzustand ausgelöst wird, ist es möglich, einen konkreten Wert zu generieren, der den Fehler auslöst, und das Problem zu reproduzieren.

Die symbolische Ausführung kann auch ein gewisses Maß an mathematischem Korrektheitsbeweis liefern. Betrachten Sie das folgende Beispiel einer Vertragsfunktion mit Überlaufschutz:

function safe_add(uint x, uint y) returns(uint z){

  z = x + y;
  require(z>=x);
  require(z>=y);

  return z;
}

Ein Ausführungs-Trace, der zu einem Integer-Überlauf führt, müsste die Formel erfüllen: z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) Es ist unwahrscheinlich, dass eine solche Formel gelöst wird, daher dient sie als mathematischer Beweis dafür, dass die Funktion safe_add niemals überläuft.

Warum formale Verifikation für Smart Contracts verwenden?

Bedarf an Zuverlässigkeit

Die formale Verifikation wird verwendet, um die Korrektheit sicherheitskritischer Systeme zu bewerten, deren Ausfall verheerende Folgen wie Tod, Verletzung oder finanziellen Ruin haben kann. Smart Contracts sind hochwertige Anwendungen, die enorme Werte kontrollieren, und einfache Designfehler können zu unwiederbringlichen Verlusten für Benutzer (opens in a new tab) führen. Die formale Verifikation eines Vertrags vor der Bereitstellung kann jedoch die Garantien erhöhen, dass er wie erwartet funktioniert, sobald er auf der Blockchain läuft.

Zuverlässigkeit ist eine sehr begehrte Eigenschaft bei jedem Smart Contract, insbesondere weil Code, der in der Ethereum Virtual Machine (EVM) bereitgestellt wird, typischerweise unveränderlich ist. Da Upgrades nach dem Start nicht ohne Weiteres zugänglich sind, macht die Notwendigkeit, die Zuverlässigkeit von Verträgen zu garantieren, die formale Verifikation erforderlich. Die formale Verifikation ist in der Lage, knifflige Probleme wie Integer-Unterläufe und -Überläufe, Re-Entrancy und schlechte Gas-Optimierungen zu erkennen, die Prüfern und Testern entgehen könnten.

Funktionale Korrektheit beweisen

Das Testen von Programmen ist die häufigste Methode, um zu beweisen, dass ein Smart Contract bestimmte Anforderungen erfüllt. Dies beinhaltet die Ausführung eines Vertrags mit einer Stichprobe der Daten, die er voraussichtlich verarbeiten wird, und die Analyse seines Verhaltens. Wenn der Vertrag die erwarteten Ergebnisse für die Beispieldaten zurückgibt, haben Entwickler einen objektiven Beweis für seine Korrektheit.

Dieser Ansatz kann jedoch keine korrekte Ausführung für Eingabewerte beweisen, die nicht Teil der Stichprobe sind. Daher kann das Testen eines Vertrags helfen, Fehler zu erkennen (d. h. wenn einige Codepfade während der Ausführung nicht die gewünschten Ergebnisse liefern), aber es kann nicht schlüssig die Abwesenheit von Fehlern beweisen.

Umgekehrt kann die formale Verifikation formal beweisen, dass ein Smart Contract Anforderungen für eine unendliche Reihe von Ausführungen erfüllt, ohne den Vertrag überhaupt auszuführen. Dies erfordert die Erstellung einer formalen Spezifikation, die korrekte Vertragsverhaltensweisen präzise beschreibt, und die Entwicklung eines formalen (mathematischen) Modells des Vertragssystems. Dann können wir einem formalen Beweisverfahren folgen, um die Konsistenz zwischen dem Modell des Vertrags und seiner Spezifikation zu überprüfen.

Mit der formalen Verifikation ist die Frage der Überprüfung, ob die Geschäftslogik eines Vertrags Anforderungen erfüllt, eine mathematische Aussage, die bewiesen oder widerlegt werden kann. Durch den formalen Beweis einer Aussage können wir eine unendliche Anzahl von Testfällen mit einer endlichen Anzahl von Schritten verifizieren. Auf diese Weise hat die formale Verifikation bessere Aussichten zu beweisen, dass ein Vertrag in Bezug auf eine Spezifikation funktional korrekt ist.

Ideale Verifikationsziele

Ein Verifikationsziel beschreibt das System, das formal verifiziert werden soll. Die formale Verifikation wird am besten in „eingebetteten Systemen“ (kleine, einfache Softwareteile, die Teil eines größeren Systems sind) eingesetzt. Sie sind auch ideal für spezialisierte Domänen, die nur wenige Regeln haben, da dies die Anpassung von Tools zur Verifikation domänenspezifischer Eigenschaften erleichtert.

Smart Contracts erfüllen – zumindest bis zu einem gewissen Grad – beide Anforderungen. Beispielsweise macht die geringe Größe von Ethereum-Verträgen sie für die formale Verifikation zugänglich. Ebenso folgt die EVM einfachen Regeln, was die Spezifikation und Verifikation semantischer Eigenschaften für Programme, die in der EVM ausgeführt werden, erleichtert.

Schnellerer Entwicklungszyklus

Techniken der formalen Verifikation, wie Model Checking und symbolische Ausführung, sind im Allgemeinen effizienter als die reguläre Analyse von Smart-Contract-Code (die während des Testens oder Auditierens durchgeführt wird). Dies liegt daran, dass die formale Verifikation auf symbolische Werte angewiesen ist, um Zusicherungen zu testen („Was ist, wenn ein Benutzer versucht, n Ether abzuheben?“), im Gegensatz zum Testen, das konkrete Werte verwendet („Was ist, wenn ein Benutzer versucht, 5 Ether abzuheben?“).

Symbolische Eingabevariablen können mehrere Klassen konkreter Werte abdecken, sodass Ansätze der formalen Verifikation mehr Codeabdeckung in einem kürzeren Zeitrahmen versprechen. Wenn sie effektiv eingesetzt wird, kann die formale Verifikation den Entwicklungszyklus für Entwickler beschleunigen.

Die formale Verifikation verbessert auch den Prozess der Erstellung dezentraler Anwendungen (Dapps), indem sie kostspielige Designfehler reduziert. Das Aktualisieren von Verträgen (wo möglich) zur Behebung von Schwachstellen erfordert ein umfangreiches Umschreiben von Codebasen und mehr Aufwand für die Entwicklung. Die formale Verifikation kann viele Fehler in Vertragsimplementierungen erkennen, die Testern und Prüfern entgehen könnten, und bietet reichlich Gelegenheit, diese Probleme vor der Bereitstellung eines Vertrags zu beheben.

Nachteile der formalen Verifikation

Kosten für manuelle Arbeit

Die formale Verifikation, insbesondere die halbautomatische Verifikation, bei der ein Mensch den Beweiser anleitet, um Korrektheitsbeweise abzuleiten, erfordert erhebliche manuelle Arbeit. Darüber hinaus ist die Erstellung einer formalen Spezifikation eine komplexe Tätigkeit, die ein hohes Maß an Fähigkeiten erfordert.

Diese Faktoren (Aufwand und Fähigkeiten) machen die formale Verifikation anspruchsvoller und teurer im Vergleich zu den üblichen Methoden zur Beurteilung der Korrektheit von Verträgen, wie Tests und Audits. Dennoch ist es praktisch, die Kosten für ein vollständiges Verifikationsaudit zu tragen, wenn man die Kosten von Fehlern in Smart-Contract-Implementierungen bedenkt.

Falsch-negative Ergebnisse

Die formale Verifikation kann nur überprüfen, ob die Ausführung des Smart Contracts mit der formalen Spezifikation übereinstimmt. Daher ist es wichtig sicherzustellen, dass die Spezifikation die erwarteten Verhaltensweisen eines Smart Contracts richtig beschreibt.

Wenn Spezifikationen schlecht geschrieben sind, können Verletzungen von Eigenschaften – die auf anfällige Ausführungen hinweisen – durch das formale Verifikationsaudit nicht erkannt werden. In diesem Fall könnte ein Entwickler fälschlicherweise annehmen, dass der Vertrag fehlerfrei ist.

Leistungsprobleme

Die formale Verifikation stößt auf eine Reihe von Leistungsproblemen. Beispielsweise können Zustands- und Pfadexplosionsprobleme, die beim Model Checking bzw. bei der symbolischen Prüfung auftreten, Verifikationsverfahren beeinträchtigen. Außerdem verwenden Tools zur formalen Verifikation oft SMT-Solver und andere Constraint-Solver in ihrer zugrunde liegenden Schicht, und diese Solver stützen sich auf rechenintensive Verfahren.

Außerdem ist es für Programmverifizierer nicht immer möglich zu bestimmen, ob eine Eigenschaft (beschrieben als logische Formel) erfüllt werden kann oder nicht (das „Entscheidungsproblem (opens in a new tab)“), da ein Programm möglicherweise nie terminiert. Daher kann es unmöglich sein, einige Eigenschaften für einen Vertrag zu beweisen, selbst wenn er gut spezifiziert ist.

Tools zur formalen Verifikation für Ethereum-Smart-Contracts

Spezifikationssprachen zur Erstellung formaler Spezifikationen

Act: Act ermöglicht die Spezifikation von Speicheraktualisierungen, Vor-/Nachbedingungen und Vertragsinvarianten. Seine Tool-Suite verfügt auch über Beweis-Backends, die in der Lage sind, viele Eigenschaften über Coq, SMT-Solver oder hevm zu beweisen.

Scribble - Scribble transformiert Code-Annotationen in der Scribble-Spezifikationssprache in konkrete Zusicherungen, die die Spezifikation überprüfen.

Dafny - Dafny ist eine verifikationsbereite Programmiersprache, die sich auf High-Level-Annotationen stützt, um über die Korrektheit von Code nachzudenken und diese zu beweisen.

Programmverifizierer zur Überprüfung der Korrektheit

Certora Prover - Certora Prover ist ein automatisches Tool zur formalen Verifikation zur Überprüfung der Codekorrektheit in Smart Contracts. Spezifikationen werden in CVL (Certora Verification Language) geschrieben, wobei Eigenschaftsverletzungen mithilfe einer Kombination aus statischer Analyse und Constraint-Solving erkannt werden.

Solidity SMTChecker - Der SMTChecker von Solidity ist ein integrierter Model Checker, der auf SMT (Satisfiability Modulo Theories) und Horn-Solving basiert. Er bestätigt während der Kompilierung, ob der Quellcode eines Vertrags mit den Spezifikationen übereinstimmt, und prüft statisch auf Verletzungen von Sicherheitseigenschaften.

solc-verify - solc-verify ist eine erweiterte Version des Solidity-Compilers, die mithilfe von Annotationen und modularer Programmverifikation eine automatisierte formale Verifikation von Solidity-Code durchführen kann.

KEVM - Die KEVM ist eine formale Semantik der Ethereum Virtual Machine (EVM), die im K-Framework geschrieben ist. Die KEVM ist ausführbar und kann bestimmte eigenschaftsbezogene Zusicherungen mithilfe von Erreichbarkeitslogik beweisen.

Logische Frameworks für das Theorembeweisen

Isabelle - Isabelle/HOL ist ein Beweisassistent, der es ermöglicht, mathematische Formeln in einer formalen Sprache auszudrücken, und Tools zum Beweisen dieser Formeln bereitstellt. Die Hauptanwendung ist die Formalisierung mathematischer Beweise und insbesondere die formale Verifikation, die den Beweis der Korrektheit von Computerhardware oder -software sowie den Beweis von Eigenschaften von Computersprachen und -protokollen umfasst.

Rocq - Rocq ist ein interaktiver Theorembeweiser, mit dem Sie Programme mithilfe von Theoremen definieren und interaktiv maschinell geprüfte Korrektheitsbeweise generieren können.

Auf symbolischer Ausführung basierende Tools zur Erkennung anfälliger Muster in Smart Contracts

Manticore - Ein Tool zur Analyse von EVM-Bytecode, das auf symbolischer Ausführung basiert.

hevm - hevm ist eine Engine für symbolische Ausführung und ein Äquivalenzprüfer für EVM-Bytecode.

Mythril - Ein Tool zur symbolischen Ausführung zur Erkennung von Schwachstellen in Ethereum-Smart-Contracts

Weiterführende Literatur

Letzte Aktualisierung der Seite: 28. April 2026

Astronaut828A (opens in a new tab)
carmen1912c (opens in a new tab)
shalom-ezekiels (opens in a new tab)
+14