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:
Definition der Spezifikationen und gewünschten Eigenschaften eines Smart Contracts in formaler Sprache.
Übersetzung des Smart-Contract-Codes in eine formale Darstellung, z.B. in mathematische Modelle oder mathematische Logik.
Anwendung automatischer Theorembeweiser (ATP) oder Modellprüfprogramme zur Validierung der Spezifikationen und Eigenschaften des Smart Contracts.
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.