Einführung

Da der Wert von Vermögenswerten auf der Blockchain mit mehreren Projekten, die abwechselnd verschiedene Anwendungsfälle innerhalb der Kryptoökonomie starten, rapid wächst, ist es wichtiger denn je, möglichen Schlupflöchern und Bedrohungen einen Schritt voraus zu sein.

Bitcoin wurde erfunden, um Banken zu ersetzen, aber die zugrunde liegende Technologie, die Blockchain, hat gezeigt, dass sie fast jeden Vermittler ersetzen kann. In der Zukunft hörte es dort nicht auf, sondern sah das massive Potenzial, das digitales Geld besaß, das Papiergeld nie besitzen konnte, und das beinhaltet die Möglichkeit, Geld zu programmieren. Plötzlich könnten Anwälte und Verträge in Finanztransaktionen ersetzt werden. Diese Form digitaler Währung hat die Dezentralisierung vorangetrieben, indem sie die automatische Ausführung von Verträgen mit vollständiger Transparenz und ohne menschliches Eingreifen ermöglichte. Aber wie funktionieren Smart Contracts genau? Kann man diesen Systemen, die auf Vertrauen verzichten, wirklich vertrauen?

In diesem Artikel werden wir die umfangreichen Fragen zur formalen Verifizierung von Smart Contracts erkunden und dabei ihre Vor- und Nachteile, Auswirkungen auf das Krypto-Ökosystem und mehr unter besonderer Betonung auf Ethereum diskutieren.

Kurze Geschichte der Smart Contracts

Quelle: CryptoSlate

Nick Szabo, ein amerikanischer Informatiker und Kryptograph, der oft als Satoshi Nakamoto vermutet wird, war der Pionier der Smart Contracts und führte das Konzept erstmals 1994 ein. Szabo beschrieb Smart Contracts als digitale Transaktionsprotokolle, die entworfen wurden, um die Bedingungen einer Vereinbarung automatisch durchzusetzen. Sein Ziel war es, elektronische Transaktionsmethoden, wie zum Beispiel Point-of-Sale-Systeme, zu verbessern und ihre Funktionalität in die digitale Welt zu erweitern.

Szabo stellte sich eine Zukunft vor, in der Vereinbarungen wie Verkaufsautomaten funktionieren könnten - automatisiert, zuverlässig und manipulationssicher. Obwohl die Technologie seiner Zeit nicht fortschrittlich genug war, um seine Vision vollständig zu verwirklichen, legten Szabos Ideen den Grundstein für das, was später die Blockchain-Industrie revolutionieren würde. Wenn Ethereum gestartetIm Jahr 2015 brachte es Smart Contracts in die praktische Anwendung und machte Szabos theoretische Konzepte zu wesentlichen Bestandteilen von dezentralen Anwendungen.

Seine Vision war, Verträge zu entwickeln, die Beziehungen mit präzisen, automatisierten Bedingungen regeln können, um den Bedarf an menschlichem Eingreifen und Überwachung zu reduzieren. Dieser Ansatz zielte darauf ab, einen sichereren und effizienteren Weg zur Abwicklung von Vereinbarungen zu schaffen und ebnete den Weg für die Entwicklung von Smart Contracts zu leistungsstarken Werkzeugen im Blockchain-Ökosystem. Szabos frühe Erkenntnisse prägen auch heute noch die Landschaft digitaler Transaktionen und der Entwicklung von Smart Contracts.

Was ist Formale Verifizierung?

Quelle: Mittel

Formale Verifizierung ist der Prozess der rigorosen Bewertung, ob ein System, wie ein Smart Contract, gemäß einem definierten Satz von Regeln oder Spezifikationen funktioniert. Im Wesentlichen überprüft es, ob das System wie erwartet funktioniert, stellt sicher, dass es die erforderlichen Bedingungen erfüllt und die beabsichtigten Funktionen ohne Fehler ausführt.

Um dies zu erreichen, werden die erwarteten Verhaltensweisen des Systems mithilfe formaler Modelle skizziert, während Spezifikationssprachen verwendet werden, um die genauen Eigenschaften zu definieren, die der Vertrag erfüllen muss, und wir werden im Laufe des Artikels weitere praktische Szenarien sehen. Formale Verifikationstechniken gleichen dann die Umsetzung des Vertrags mit seinen Spezifikationen ab und liefern so den mathematischen Beweis für seine Richtigkeit. Wenn ein Vertrag diese Spezifikationen erfüllt, gilt er als "funktional korrekt" oder "korrekt durch Design", was seine Zuverlässigkeit und Sicherheit in der Blockchain-Umgebung bestätigt.

Arten von formalen Spezifikationen für Smart Contracts

Quelle: Ever Scale

Formale Spezifikationen bieten eine strukturierte Möglichkeit, mathematische Argumentation zu verwenden, um die Genauigkeit der Programmausführung zu überprüfen. Diese Spezifikationen können entweder hochrangige Eigenschaften beschreiben, die sich auf das Gesamtverhalten konzentrieren, oder Detailinformationen zur internen Funktionsweise eines Vertrags. Indem diese Verhaltensweisen mathematisch definiert werden, stellen formale Spezifikationen sicher, dass der Vertrag wie beabsichtigt funktioniert.

Hochrangige Spezifikationen

Hochrangige Spezifikationen, auch bekannt als modellorientierte Spezifikationen, beschreiben das Gesamtverhalten eines Smart Contracts und behandeln ihn als endlichen Automaten (FSM), der durch spezifische Operationen zwischen verschiedenen Zuständen wechselt. Temporale Logik wird häufig verwendet, um die formalen Regeln zu definieren, die diese Übergänge regeln und detaillieren, wie der Vertrag im Laufe der Zeit zwischen den Zuständen wechselt und die Bedingungen erfüllen muss, um dies korrekt zu tun.

Diese Spezifikationen erfassen zwei wesentliche Eigenschaften: Sicherheit und Lebendigkeit. Sicherheit stellt sicher, dass unerwünschte Ereignisse nicht eintreten, wie z.B. das Verhindern, dass das Guthaben des Absenders unter den für eine Transaktion erforderlichen Betrag fällt. Lebendigkeit hingegen stellt sicher, dass der Vertrag weiterhin funktioniert und Fortschritte macht, wie z.B. die Aufrechterhaltung der Liquidität, damit Benutzer bei Bedarf Geld abheben können. Beide Eigenschaften gewährleisten, dass Smart Contracts sicher und zuverlässig funktionieren und Benutzerinteraktionen und Vermögenswerte schützen.

Niedrigstufige Spezifikationen

Niedrigstufige Spezifikationen, auch als eigenschaftsorientierte Spezifikationen bekannt, konzentrieren sich darauf, das korrekte Verhalten von Smart Contracts zu definieren, indem sie ihre internen Ausführungsprozesse analysieren. Im Gegensatz zu Hochstufenspezifikationen, die Verträge als endliche Automaten modellieren, betrachten niedrigstufige Spezifikationen Smart Contracts als Systeme mathematischer Funktionen und untersuchen die Sequenzen von Funktionsausführungen, die den Zustand des Vertrags ändern, bekannt als Traces.

Techniken zur Formalen Verifizierung von Smart Contracts

Quelle: Immer Maßstab

Model Checking

Model Checking ist eine Formale Verifizierungsmethode, die Algorithmen verwendet, um zu bewerten, ob das Modell eines Smart Contracts mit seinen Spezifikationen übereinstimmt. Smart Contracts werden in der Regel als Zustandsübergangssysteme dargestellt, und ihre Eigenschaften werden mithilfe von temporalenLogikDieser Prozess umfasst die Erstellung eines mathematischen Modells des Vertrags und die Ausdrückung seiner Eigenschaften durch logische Formeln, die es dem Algorithmus ermöglichen zu überprüfen, ob das Modell diesen Spezifikationen entspricht.

Beweisverfahren

Im Gegensatz zur Modellprüfung ist der Theorembeweis ein mathematischer Ansatz, der zur Feststellung der Korrektheit von Programmen, einschließlich Smart Contracts, verwendet wird. Diese Methode beinhaltet die Umwandlung des Modells und der Spezifikationen eines Vertrags in logische Formeln, um ihre logische Äquivalenz zu überprüfen, was bedeutet, dass eine Aussage wahr ist, wenn die andere wahr ist. Indem diese Beziehung als Theorem formuliert wird, kann ein automatischer Theorembeweiser die Korrektheit des Vertragsmodells gegenüber seinen Spezifikationen validieren.

Im scharfen Kontrast zur Modellprüfung, die auf endliche Zustandssysteme beschränkt ist, kann die Beweisführung unendliche Zustandssysteme analysieren, erfordert jedoch häufig menschliche Anleitung, um komplexe logische Probleme zu bewältigen. Folglich ist die Beweisführung in der Regel ressourcenintensiver als der vollautomatisierte Modellprüfungsprozess.

Symbolische Ausführung

Symbolische Ausführung ist eine leistungsstarke Analysemethode für Smart Contracts, die Funktionen mit symbolischen Werten anstelle von spezifischen Eingaben ausführt. Diese Formale Verifizierungstechnik ermöglicht es, auf Trace-Ebene Eigenschaften im Code eines Vertrags zu betrachten, indem Ausführungspfade als mathematische Formeln, sogenannte Pfadprädikate, dargestellt werden. Ein SMT-Löser wird dann eingesetzt, um zu bestimmen, ob diese Prädikate zufriedenstellend sind, d.h. ob eine Eingabe existiert, die den Bedingungen entspricht.

Wenn beispielsweise eine Vertragsfunktion zurückkehrt, wenn ein Wert zwischen 5 und 10 liegt, kann die symbolische Ausführung solche auslösenden Werte effizient identifizieren, indem sie die Bedingung als X > 5 ∧ X < 10 auswertet. Diese Methode ist oft effektiver als herkömmliche Tests, erzeugt weniger falsch positive Ergebnisse und generiert direkt konkrete Werte, die jeden SMT-Solver replizieren. Zur Bestimmung gefundener Fehler wird dann ein wertvolles Werkzeug zur Sicherstellung der Verlässlichkeit von Smart Contracts eingesetzt.

Was sind Smart Contracts?

Quelle: Zärtlich

Smart Contracts sind automatisierte Computerprogramme, die auf einer Blockchain operieren und Aktionen ausführen, wenn bestimmte Bedingungen erfüllt sind. Sie können von einfachen Vereinbarungen bis hin zu hochkomplexen Prozessen variieren und Vermögenswerte im Wert von Millionen oder sogar Milliarden von Dollar verwalten.

Während Smart Contracts das Potenzial haben, verschiedene Bereiche wie politische Abstimmungen, Supply Chain Management, Gesundheitswesen und Immobilien zu revolutionieren, behält dieser Artikel dennoch seinen Fokus auf ihre Auswirkungen im Kryptowährungsbereich bei. Ihr Design ermöglicht es mehreren Parteien, ohne Manipulationsrisiko zusammenzuarbeiten und bietet ein transparentes und sicheres Rahmenwerk, das Effizienz und Innovation verbessert. Es ist jedoch wichtig anzuerkennen, dass Smart Contracts auch mit Schwachstellen und Herausforderungen einhergehen.

Schwachstellen bei Smart Contracts

SicherheitsschwachstellenFehler im Smart-Vertragscode können zu katastrophalen Ergebnissen führen, wie zum Beispiel dem totalen Verlust von Vermögenswerten, die im Vertrag gespeichert sind, wie durch kürzliche Vorfälle demonstriert wurde.

• Im Jahr 2021 führte der automatisierte Market Maker Uranium Finance hat einen Diebstahl von 50 Millionen Dollar erlittenaufgrund eines einfachen Tippfehlers in seinem Smart Contract.
• Auch im Jahr 2021, Compound Finance verteilte versehentlich 80 Millionen Dollaraufgrund eines einzelnen Zeichenfehlers erneut in nicht verdiente Belohnungen.
• Eine bedeutendere Verletzung ereignete sich im Jahr 2022als $320 Millionen von der Wormhole-Brücke gestohlen wurdenaufgrund eines Fehlers in einem seiner Smart Contracts.

Angesichts dieser Beispiele ist es entscheidend sicherzustellen, dass Smart Contracts von Anfang an genau codiert werden. Sobald sie bereitgestellt sind, sind Smart Contracts Open Source, was bedeutet, dass ihr Code öffentlich zugänglich ist und es Hackern leicht macht, entdeckte Schwachstellen auszunutzen. Darüber hinaus bedeutet die unveränderliche Natur von Smart Contracts, dass ihr Code in der Regel nach dem Start nicht geändert werden kann, um Sicherheitslücken zu beheben, sodass sie dauerhaft gefährdet sind, wenn sie nicht mit größter Präzision entwickelt werden.

Wie funktioniert die Verifizierung von Smart Contracts?

Quelle: Certik

Der Prozess umfasst:

• Die Spezifikationen und gewünschten Eigenschaften des Vertrags mithilfe einer formalen Sprache definieren.
• Die Übersetzung des Vertragscodes in eine formale Darstellung, wie mathematische Modelle oder logische Ausdrücke.
• Automatisierte Theorembeweiser oder Modellprüfer werden eingesetzt, um die Gültigkeit der Vertragsspezifikationen und -eigenschaften zu bestätigen.
• Wiederholen Sie iterativ den Verifizierungsprozess, um Fehler oder Abweichungen von den beabsichtigten Eigenschaften zu identifizieren und zu korrigieren.

Schlüsselfunktionen von Smart Contracts

Quelle: Certik

Smart Contracts können als Vereinbarungen betrachtet werden, die einmal erstellt wurden und nicht geändert werden können. Sie funktionieren auf der unveränderlichen Buchführung einer Blockchain, und diese Verträge setzen automatisch Bedingungen durch, ohne dass Vermittler erforderlich sind, was Transaktionen beschleunigt und Kosten senkt. Diese feste Natur erhöht die Sicherheit und dezentralisiert die Kontrolle, was die Wahrscheinlichkeit von Betrug und Korruption erheblich reduziert.

Warum die Verifizierung von Smart Contracts wichtig ist

Mathematisches Denken spielt eine entscheidende Rolle dafür, dass formale verifizierte Smart Contracts frei von Fehlern, Schwachstellen und unerwartetem Verhalten sind. Dieser strenge Prozess stärkt das Vertrauen in den Vertrag, da seine Eigenschaften gründlich validiert wurden.

Erfolgreiche Beispiele für die formale Verifizierung von Smart Contracts unterstreichen deren Bedeutung bei der Verhinderung erheblicher finanzieller Verluste.

Uniswap

Beispielsweise wurde Uniswap, ein bekannter automatisierter Marktgestalter (AMM), während der Entwicklung seines V1-Smart-Vertrags einer formalen Verifizierung unterzogen, die Rundungsfehler identifizierte und korrigierte.das hätte Geld abfließen lassen können.

Balancer

Ebenso profitierte Balancer V2, ein weiteres AMM, von der formalen Verifizierung, die feststellte eine falsche Gebührenberechnungim Zusammenhang mit Flash-Krediten, um potenzielle Diebstähle zu verhindern.

SafeMoon

SafeMoon V1 hatte einen subtilen Fehleridentifiziert durch formale Verifizierung nach der Bereitstellung. Dieser Fehler ermöglichte es dem Besitzer, den Besitz abzulehnen und unter bestimmten Bedingungen wiederzuerlangen, ein Detail, das die meisten manuellen Prüfungen aufgrund seiner Komplexität übersehen haben. Die Fähigkeit der formalen Verifizierung, spezifische Kombinationen von Variablenwerten zu analysieren, macht sie zu einem effektiven Werkzeug, um Probleme zu erkennen, die menschliche Prüfer möglicherweise übersehen.

Wie formale Verifizierung und manuelle Prüfung zusammenarbeiten

Formale Verifizierung bietet eine systematische und automatisierte Methode zur Überprüfung der Logik und des Verhaltens eines Smart Contracts auf seine beabsichtigten Eigenschaften. Dieser Ansatz vereinfacht die Identifizierung und Korrektur potenzieller Fehler oder Bugs, insbesondere bei komplexen Problemen, die manuelle Inspektionen möglicherweise übersehen.

Auf der anderen Seite beinhaltet die manuelle Prüfung eine gründliche Überprüfung des Vertragscodes, des Designs und der Bereitstellung durch einen Experten. Der Prüfer nutzt seine Erfahrung, um Sicherheitsrisiken zu lokalisieren und das allgemeine Sicherheitsniveau des Vertrags zu bewerten. Er kann auch die Korrektheit des Prozesses der formalen Verifizierung validieren und Probleme identifizieren, die automatisierte Tools möglicherweise übersehen. Die Kombination von formaler Verifizierung mit manueller Prüfung schafft eine umfassende Sicherheitsbewertung, die die Wahrscheinlichkeit erhöht, Schwachstellen aufzudecken und zu beheben, und eine robuste Verteidigungsstrategie etabliert, die die Stärken menschlicher Expertise und automatisierter Analyse nutzt.

Vor- und Nachteile von Smart Contracts

Quelle: Blockonomi

Smart Contracts sind nicht perfekt, aber ihre Vorteile überwiegen die Nachteile deutlich. Sie vereinfachen komplexe Transaktionen, sparen Zeit und Geld, fördern Transparenz und reduzieren Streitigkeiten. Da sie auf Code basieren, minimieren sie menschliche Fehler. Ihre Sicherheit ist robust, dank kryptographischer Schutzmechanismen. Allerdings können Smart Contracts unflexibel sein und Schwierigkeiten haben, sich an unerwartete Situationen anzupassen. Darüber hinaus erfordert die Einrichtung spezielle Codierungskenntnisse, was für einige ein Hindernis darstellen kann. Trotz dieser Herausforderungen transformieren Smart Contracts Branchen.

Vorteile von Smart Contracts

• Verbessern Sie die Effizienz, indem Sie Aufgaben automatisieren und Zeit und Geld sparen.
• Erhöhen Sie die Transparenz, indem Sie allen Parteien Zugriff auf die gleichen Informationen geben und Streitigkeiten reduzieren.
• Reduzieren Sie Fehler, indem Sie auf Code vertrauen, der menschliche Fehler eliminiert.
• Stärken Sie die Sicherheit durch kryptografischen Schutz, um das Manipulieren zu erschweren.

Nachteile von Smart Contracts

• Mangel an Flexibilität, um sich auf unvorhergesehene Situationen einzustellen, aufgrund ihrer starren Natur.
• Erfordert spezialisiertes Codierungswissen, was die weit verbreitete Einführung einschränkt.

Formale Verifizierungstools für Ethereum Smart Contracts

Quelle: Calibraint

Spezifikationssprachen zur Erstellung formaler Spezifikationen

• Act: Act ermöglicht es Benutzern, Speicheraktualisierungen, Vor- und Nachbedingungen sowie Vertragsinvarianten festzulegen. Der Tool-Satz umfasst Beweisbackends, die mithilfe von Coq, SMT-Solvern oder hevm verschiedene Eigenschaften validieren können.

GitHub

Dokumentation

• Scribble: Scribble wandelt in seiner Spezifikationssprache verfasste Code-Anmerkungen in spezifische Behauptungen um, die die Spezifikationen überprüfen.

Dokumentation

• Dafny: Dafny ist eine Programmiersprache, die für die Verifikation entwickelt wurde. Sie verwendet hochrangige Annotationen, um das Nachvollziehen und die Bestätigung der Korrektheit des Codes zu erleichtern.

GitHub

Programmverifier zur Überprüfung der Korrektheit

• Certora Prover: Certora Prover ist ein automatisiertes Formale Verifizierungstool, das die Korrektheit von Smart Contract-Codes überprüft. Spezifikationen werden mithilfe der Certora Verification Language (CVL) erstellt, und es erkennt Eigenschaftsverletzungen durch eine Mischung aus statischer Analyse und Constraint-Lösungstechniken.

Website

Dokumentation

• Solidity SMTChecker: Solidity’s SMTChecker ist ein integrierter Modellchecker, der die Satisfiability Modulo Theories (SMT) und Horn solving verwendet. Es überprüft, ob der Quellcode eines Vertrags während der Kompilierung mit den Spezifikationen übereinstimmt und überprüft auf Verletzungen von Sicherheitseigenschaften.

GitHub

• Solc-verify: Solc-verify ist eine erweiterte Version des Solidity-Compilers, die automatisierte formale Verifizierung von Solidity-Code durch Annotationen und modulare Programmverifizierung ermöglicht.

GitHub

• KEVM: KEVM vertritt formal die Ethereum Virtual Machine(EVM)erstellt mit dem K-Framework. Es ist ausführbar und kann spezifische eigenschaftsbezogene Behauptungen durch Erreichbarkeitslogik überprüfen.

GitHub

Dokumentation

Logische Rahmenwerke für Beweisführung

• Isabelle: Isabelle/HOL ist ein Beweisassistent, der Benutzern dabei hilft, mathematische Formeln in einer formalen Sprache auszudrücken und Werkzeuge zum Beweisen bereitzustellen. Seine Hauptanwendung besteht darin, mathematische Beweise formal zu erfassen, insbesondere um die Korrektheit von Computerhardware und -software sowie die Eigenschaften von Programmiersprachen und Protokollen zu überprüfen.

GitHub

Dokumentation

• Coq - Coq ist ein interaktiver Theorembeweiser, mit dem Sie Programme mit Theoremen definieren und maschinell geprüfte Beweise für ihre Richtigkeit durch einen interaktiven Prozess erstellen können.

GitHub

Dokumentation

Symbolische Ausführungsbasierte Tools zum Erkennen von verwundbaren Mustern in Smart Contracts

• Manticore - Ein Tool, das EVM-Bytecode mithilfe der symbolischen Ausführung analysiert.

GitHub

Dokumentation

• Hevm - hevm ist eine symbolische Ausführungsmaschine, die die Äquivalenz von EVM-Bytecode überprüft.

GitHub

• Mythril - Ein symbolisches Ausführungswerkzeug zur Suche nach Schwachstellen in Ethereum Smart Contracts.

GitHub

Dokumentation

Fazit

Um Smart Contracts zu schützen, ist die Kombination aus formaler Verifizierung und manueller Prüfung entscheidend für eine umfassende Bewertung ihrer Sicherheit. Obwohl die formale Verifizierung ressourcenintensiv sein kann, ist sie eine wertvolle Investition für Verträge, bei denen viel auf dem Spiel steht oder ein erhebliches Risiko besteht. Smart Contracts sind mehr als ein trendiges Konzept. Sie transformieren globale Geschäftsabläufe, und obwohl sie Herausforderungen mit sich bringen, kann ihre beispiellose Fähigkeit, die Effizienz zu steigern, Fehler zu minimieren und die Sicherheit zu erhöhen, nicht ignoriert werden. Smart Contracts bergen ein enormes Potenzial, um Prozesse zu vereinfachen und das Vertrauen in digitale Transaktionen zu fördern. Zu diesem Zweck werden Unternehmen, die diese Technologie heute einsetzen, in einer Zukunft erfolgreich sein, in der Transparenz und Zuverlässigkeit im Vordergrund stehen.