Was ist die formale Verifizierung von Smart Contracts?
Startseite
Artikel
Was ist die formale Verifizierung von Smart Contracts?

Was ist die formale Verifizierung von Smart Contracts?

Fortgeschritten
Veröffentlicht Mar 2, 2023Aktualisiert Jul 12, 2023
5m

Dieser Artikel ist ein Beitrag der Community. Der Autor ist David Tarditi, VP of Engineering bei CertiK, einem Pr√ľfungsunternehmen f√ľr Web3-Smart-Contracts.

TL;DR

Die formale Verifizierung von Smart Contracts gew√§hrleistet, dass diese frei von Fehlern, Schwachstellen und anderem unbeabsichtigten Verhalten sind. Dabei stellt ein menschlicher Experte die Logik des Smart Contracts in Form von mathematischen Aussagen dar und l√§sst sie dann einen automatisierten Prozess durchlaufen, der die tats√§chliche Logik mit Modellen des erwarteten Verhaltens des Contracts vergleicht. Die Kombination aus formaler Verifizierung und manueller Pr√ľfung erm√∂glicht eine umfassende Bewertung der Sicherheit eines Smart Contracts.

Einf√ľhrung

Smart Contracts sind Computerprogramme, die auf einer Blockchain implementiert sind und automatisch ausgef√ľhrt werden, wenn bestimmte Bedingungen erf√ľllt sind. Sie k√∂nnen einfach oder extrem komplex sein und Assets im Wert von Millionen oder sogar Milliarden USD enthalten.¬†¬†

Sicherheitsl√ľcken im Code eines Smart Contracts k√∂nnen gravierende Folgen haben, bis hin zum Diebstahl aller Assets, die darin enthalten sind. Im Jahr 2021 wurde der automatisierte Market-Maker (AMM) Uranium Finance aufgrund eines einzigen Tippfehlers in einem Smart Contract um 50 Mio. USD beraubt.

Ebenfalls im Jahr 2021 zahlte Compound Finance aufgrund eines einzigen Buchstabenfehlers fälschlicherweise 80 Mio. USD an Belohnungen aus. Und 2022 wurden der Blockchain-Bridge Wormhole aufgrund eines fehlerhaften Smart Contract 320 Mio. USD gestohlen.

Es ist wichtig, dass das Smart-Contract-Programm gleich von Anfang an richtig funktioniert. Smart Contracts sind quelloffen, d.h. der Code ist √∂ffentlich zug√§nglich, sobald der Smart Contract implementiert wurde. Wenn ein Hacker einen Fehler findet, kann er ihn sofort ausnutzen. Au√üerdem ist es nicht m√∂glich, Sicherheitsschwachstellen im Laufe der Zeit zu beheben, da der Smart-Contract-Code nach der Einf√ľhrung in der Regel nicht mehr ge√§ndert werden kann.

Wie die Verifizierung von Smart Contracts funktioniert  

Bei der formalen Verifizierung von Smart Contracts werden deren Logik und gew√ľnschtes Verhalten als mathematische Aussagen dargestellt. Die Pr√ľfer verwenden dann automatisierte Tools, um zu untersuchen, ob diese Aussagen korrekt sind.

Der Prozess umfasst folgende Schritte:

  1. Definition der Spezifikationen und gew√ľnschten Eigenschaften eines Smart Contracts in formaler Sprache.

  2. √úbersetzung des Smart-Contract-Codes in eine formale Darstellung, z.B. in mathematische Modelle oder mathematische Logik.

  3. Anwendung automatischer Theorembeweiser (ATP) oder Modellpr√ľfprogramme zur Validierung der Spezifikationen und Eigenschaften des Smart Contracts.

  4. Wiederholung des Verifizierungsprozesses, um allf√§llige Fehler oder Abweichungen von den gew√ľnschten Eigenschaften zu finden und zu beheben.

Warum die Verifizierung von Smart Contracts wichtig ist

Der Einsatz mathematischer Logik hilft sicherzustellen, dass formal verifizierte Smart Contracts frei von Fehlern, Schwachstellen und anderem unbeabsichtigten Verhalten sind. Auf diese Weise kann das Vertrauen in einen Smart Contract erhöht werden, da seine Eigenschaften als eindeutig korrekt erwiesen sind. 

Im Folgenden sind einige Beispiele aufgef√ľhrt, bei denen durch die Verifizierung von Smart Contracts erhebliche finanzielle Verluste und andere schwerwiegende Folgen vermieden werden konnten.¬†¬†

Uniswap

Uniswap ist ein bekannter AMM. Der Smart Contract von Uniswap V1 wurde bei seiner Entwicklung formal verifiziert. Dank dieser formalen Verifizierung wurden noch vor seiner Einf√ľhrung Rundungsfehler gefunden und behoben, die dazu h√§tten f√ľhren k√∂nnen, dass Mittel von Uniswap V1 ungewollt abgezogen werden.¬†

Balancer

Balancer V2 ist ebenfalls ein AMM, der formal verifiziert wurde. Bei der formalen Verifizierung wurde eine falsche Geb√ľhrenberechnung im Zusammenhang mit der Flashkredit-Funktion des Smart Contracts festgestellt und korrigiert, die die B√∂rse m√∂glicherweise anf√§llig f√ľr Diebstahl gemacht h√§tte.

SafeMoon

SafeMoon V1 enthielt einen unauff√§lligen Fehler, der bei der formalen Verifizierung nach der Einf√ľhrung der Kryptow√§hrung gefunden wurde. Wegen dieses Fehlers war es m√∂glich, dass ein Inhaber eines Contracts sein Eigentum aufgibt und es dann wieder erwirbt, wenn vor dem Aufgeben des Eigentums bestimmte Operationen durchgef√ľhrt wurden.

Dieser Fehler wurde bei den meisten manuellen Pr√ľfungen von SafeMoon V1-Forks √ľbersehen, da die Identifizierung die Analyse bestimmter Kombinationen von Variablenwerten des Programms erforderte. Das ist etwas, das f√ľr Menschen leicht zu √ľbersehen und f√ľr eine Maschine leicht zu erkennen ist.

Kombination von formaler Verifizierung und manueller Pr√ľfung

Die formale Verifizierung bietet die M√∂glichkeit, die Logik und das Verhalten eines Smart Contracts im Hinblick auf seine gew√ľnschten Eigenschaften in systematischer und automatisierter Weise zu √ľberpr√ľfen. So lassen sich potenzielle Fehler oder Bugs leichter erkennen und beheben. Dies ist besonders n√ľtzlich, wenn es darum geht, komplexe und versteckte Probleme zu finden, die bei einer manuellen Pr√ľfung nur schwer zu identifizieren sind.

Bei der manuellen Pr√ľfung werden der Code, das Design und die Implementierung eines Smart Contracts von Experten gepr√ľft. Gest√ľtzt auf seine Erfahrung und sein Fachwissen sucht der Pr√ľfer nach Sicherheitsrisiken und bewertet die Gesamtsicherheit des Smart Contracts. Er kann auch best√§tigen, dass der formale Verifizierungsprozess korrekt durchgef√ľhrt wurde, und den Smart Contract auf m√∂gliche Probleme pr√ľfen, die mit automatisierten Tools nicht erkannt werden k√∂nnen.¬†

Die Kombination aus formaler Verifizierung und manueller Pr√ľfung erm√∂glicht eine umfassende und gr√ľndliche Bewertung der Sicherheit eines Smart Contracts. Dadurch erh√∂hen sich die Chancen, Schwachstellen zu identifizieren und zu beheben. Das Ergebnis ist ein ‚ÄěDefense-in-Depth‚Äú-Ansatz, der die einzigartigen F√§higkeiten von Mensch und Maschine nutzt.¬†

Fazit

Zur Gew√§hrleistung der Sicherheit eines Smart Contracts ist es wichtig, sowohl eine formale Verifizierung als auch eine manuelle Pr√ľfung vorzunehmen, um eine umfassende und gr√ľndliche Sicherheitsbewertung zu erhalten.

Die formale Verifizierung kann zwar aufw√§ndig sein, ist aber eine lohnende Investition f√ľr Smart Contracts, die f√ľr Assets mit hohem Wert entwickelt wurden oder die hohe Risikofaktoren aufweisen. Letztlich ist es von entscheidender Bedeutung, der Sicherheit h√∂chste Priorit√§t beizumessen und sicherzustellen, dass Smart Contracts frei von Fehlern, Schwachstellen und unbeabsichtigtem Verhalten sind.

Weiterf√ľhrende Lekt√ľre

Disclaimer und Risikohinweis: Dieser Inhalt wird dir zu allgemeinen Informations- und Bildungszwecken pr√§sentiert, ohne jegliche Zusicherung oder Garantie. Er ist weder als Finanzberatung zu verstehen, noch soll er den Kauf bestimmter Produkte oder Dienstleistungen empfehlen. Die Preise von digitalen Assets sind volatil. Der Wert deiner Anlage kann fallen oder steigen, und es kann sein, dass du den angelegten Betrag nicht zur√ľckerh√§ltst. Du bist allein f√ľr deine Anlageentscheidungen verantwortlich, und die Binance Academy haftet nicht f√ľr etwaige Verluste, die du erleidest. Dieser Inhalt stellt keine Finanzberatung dar.