Dieser Artikel ist ein Community-Beitrag. Der Autor ist David Tarditi, VP of Engineering bei Certik, einem Web3-Smart-Contract-Audit-Unternehmen.

Zusammenfassung

Durch die formelle Überprüfung von Smart Contracts wird sichergestellt, dass diese frei von Fehlern, Schwachstellen und anderem unerwünschten Verhalten sind. Sie wird von einem menschlichen Experten durchgeführt, der die Smart-Contract-Logik als mathematische Aussagen präsentiert und sie dann durch einen automatisierten Prozess führt, der die tatsächliche Logik mit den erwarteten Verhaltensmodellen des Smart 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 von einfach bis äußerst komplex reichen und Vermögenswerte im Wert von Millionen oder sogar Milliarden Dollar enthalten.

Sicherheitslücken im Smart-Contract-Code können schwerwiegende Folgen haben, einschließlich des Diebstahls aller Smart-Contract-Assets. Im Jahr 2021 kam es bei Automated Market Maker (AMM) Uranium Finance aufgrund eines Tippfehlers in einem Smart Contract zu einem Diebstahl von 50 Millionen US-Dollar.

Ebenfalls im Jahr 2021 verteilte Compound Finance allein aufgrund fehlerhafter Charaktere 80 Millionen US-Dollar an unverdienten Belohnungen. Im Jahr 2022 wurden Wormhole Bridge aufgrund eines Fehlers in einem seiner Smart Contracts 320 Millionen US-Dollar gestohlen.

Es ist wichtig, dass das Smart-Contract-Programm von Anfang an korrekt ist. Smart Contracts sind Open Source, das heißt, sobald der Vertrag bereitgestellt wird, ist der Code für die Öffentlichkeit verfügbar. Wenn ein Hacker einen Fehler findet, kann er ihn sofort ausnutzen. Darüber hinaus ist das Patchen von Sicherheitslücken keine nachhaltige Option, da der Vertragscode nach der Bereitstellung normalerweise nicht mehr geändert werden kann.

Wie funktioniert die intelligente Vertragsüberprüfung?

Die formale Verifizierung von Smart Contracts erfolgt durch die Darstellung der Logik und des gewünschten Verhaltens der Verträge als mathematische Aussagen. Mithilfe automatisierter Tools überprüfen Prüfer dann, ob die Aussagen korrekt sind.

Der Prozess umfasst:

  1. Definieren Sie die Spezifikationen und gewünschten Eigenschaften eines Vertrags in formaler Sprache.

  2. Übersetzen Sie intelligenten Vertragscode in eine formale Darstellung, z. B. mathematische Modelle und Logik.

  3. Verwenden Sie automatisierte Theorembeweiser oder Modellprüfer, um Vertragsspezifikationen und -eigenschaften zu validieren.

  4. Wiederholen Sie den Überprüfungsprozess, um etwaige Fehler oder Abweichungen von den gewünschten Eigenschaften zu finden und zu korrigieren.

Warum die Überprüfung intelligenter Verträge wichtig ist

Der Einsatz mathematischer Argumente trägt dazu bei, sicherzustellen, dass formal verifizierte Verträge frei von Fehlern, Schwachstellen und anderem unerwünschten Verhalten sind. Es trägt auch dazu bei, das Vertrauen in den Vertrag zu stärken, da seine Eigenschaften streng auf ihre Richtigkeit geprüft wurden.

Nachfolgend finden Sie einige Beispiele dafür, wie die intelligente Vertragsüberprüfung dazu beigetragen hat, erhebliche finanzielle Verluste und andere schwerwiegende Folgen zu verhindern.

Uniswap

Uniswap ist ein bekannter AMM. Als die erste Version des Uniswap-Smart-Vertrags entwickelt wurde, wurde sie offiziell verifiziert. Vor der Einführung wurden bei dieser formellen Überprüfung Rundungsfehler festgestellt und korrigiert, die möglicherweise dazu geführt haben, dass Gelder aus Uniswap V1 abgezogen wurden.

Balancer

Balancer V2 wird auch als offiziell verifiziertes AMM bezeichnet. Die formelle Überprüfung ergab und korrigierte eine falsche Gebührenberechnung im Zusammenhang mit der Flash-Darlehensfunktion im Smart Contract, die die Börse anfällig für Diebstahl hätte machen können.

Sicherer Mond

SafeMoon V1 enthielt einen subtilen Fehler, der bei der formalen Überprüfung nach der Vertragsimplementierung entdeckt wurde. Wenn bestimmte Transaktionen vor dem Verzicht auf das Eigentum an dem Vertrag getätigt wurden, war es für den Eigentümer des Vertrags möglich, das Eigentum aufzugeben und es dann wieder zu erwerben.

Dieser Fehler blieb bei den meisten manuellen Prüfungen der SafeMoon V1-Forks unbemerkt, da für die Suche nach ihm bestimmte Kombinationen der Variablenwerte des Programms analysiert werden mussten. Dies ist etwas, das sich leicht der menschlichen Kontrolle entzieht, aber von einer Maschine leicht entdeckt werden kann.

Wie formale Verifizierung und manuelle Prüfung zusammenarbeiten

Die formale Verifizierung bietet eine systematische und automatisierte Möglichkeit, die Logik und das Verhalten eines Vertrags in Bezug auf seine gewünschten Eigenschaften zu bestätigen und so potenzielle Fehler und Bugs leichter zu erkennen und zu beheben. Es ist besonders nützlich, um komplexe und subtile Probleme zu finden, die bei der manuellen Inspektion möglicherweise unbemerkt bleiben.

Bei der manuellen Prüfung handelt es sich um eine Expertenprüfung des Codes, der Gestaltung und der Vertragsumsetzung. Der Prüfer nutzt seine Erfahrung und sein Fachwissen, um Sicherheitsrisiken zu identifizieren und die allgemeine Sicherheitslage des Vertrags zu bewerten. Sie können auch bestätigen, dass der formelle Verifizierungsprozess korrekt abgeschlossen wurde, und alle Probleme überprüfen, die von 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 des Smart Contracts und erhöht so die Wahrscheinlichkeit, etwaige darin enthaltene Schwachstellen zu finden und zu beheben. Das Ergebnis ist ein tiefgreifender Sicherheitsansatz, der die einzigartigen Fähigkeiten von Menschen und Maschinen nutzt.

Schlussfolgerungen

Um die Sicherheit von Smart Contracts zu gewährleisten, ist es unerlässlich, eine formelle Verifizierung und auch ein manuelles Audit durchzuführen, um so eine umfassende und gründliche Bewertung der Sicherheitslage des Smart Contracts zu gewährleisten.

Obwohl eine formelle Verifizierung ressourcenintensiv sein kann, lohnt sich die Investition bei Verträgen mit hohem Wert oder hohem Risiko. Schließlich ist es wichtig, der Sicherheit Priorität einzuräumen und sicherzustellen, dass Smart Contracts frei von Fehlern, Schwachstellen und unerwünschtem Verhalten sind.

Weiterführende Literatur

  • Was sind Smart Contracts?

  • Was ist ein Smart-Contract-Sicherheitsaudit?

Rechtlicher Hinweis und Risikowarnung: Dieser Inhalt wird „wie besehen“ nur zu allgemeinen Informations- und Bildungszwecken präsentiert, ohne Zusicherungen oder Gewährleistungen jeglicher Art. Es ist weder als Finanzberatung zu verstehen, noch ist es dazu gedacht, den Kauf eines bestimmten Produkts oder einer bestimmten Dienstleistung zu empfehlen. Die Preise digitaler Vermögenswerte sind volatil. Der Wert einer Anlage kann sowohl fallen als auch steigen, und es kann sein, dass Sie den investierten Betrag nicht zurückerhalten. Für Ihre Anlageentscheidungen sind allein Sie verantwortlich. Die Binance Academy übernimmt keine Haftung für etwaige Verluste, die Ihnen entstehen. Dieses Material sollte nicht als Finanzberatung ausgelegt werden.