Dieser Artikel ist eine Community-Einreichung. Der Autor ist David Tarditi, VP of Engineering bei CertiK, einem Web3-Smart-Contract-Audit-Unternehmen.
Die Ansichten in diesem Artikel stammen vom Mitwirkenden/Autor und spiegeln nicht unbedingt die Ansichten der Binance Academy wider.
TL;DR
Die formelle Verifizierung von Smart Contracts stellt sicher, dass sie frei von Fehlern, Schwachstellen und anderen unbeabsichtigten Verhaltensweisen sind. Dabei stellt ein menschlicher Experte die Logik des Smart Contracts als mathematische Aussagen dar und führt sie dann durch einen automatisierten Prozess, der die tatsächliche Logik mit Modellen des erwarteten Verhaltens des Vertrags vergleicht. Die Kombination aus formeller Verifizierung und manueller Prüfung bietet 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 extrem komplex reichen und Vermögenswerte im Wert von Millionen oder sogar Milliarden Dollar enthalten.
Sicherheitslücken im Smart-Contract-Code können verheerende Folgen haben, darunter den Diebstahl aller Vermögenswerte eines Smart Contracts. Im Jahr 2021 wurden dem Automated Market Maker (AMM) Uranium Finance aufgrund eines einzigen Tippfehlers in einem Smart Contract 50 Millionen US-Dollar gestohlen.
Außerdem gab Compound Finance im Jahr 2021 aufgrund eines einzigen Zeichenfehlers 80 Millionen US-Dollar an unverdienten Belohnungen aus. Im Jahr 2022 wurden aufgrund eines Fehlers in einem seiner Smart Contracts 320 Millionen US-Dollar von der Wormhole Bridge gestohlen.
Es ist wichtig, das Smart-Contract-Programm gleich beim ersten Mal richtig zu machen. Smart Contracts sind Open Source, d. h. der Code ist öffentlich verfügbar, sobald ein Vertrag bereitgestellt wird. Wenn ein Hacker einen Fehler findet, kann er ihn sofort ausnutzen. Darüber hinaus ist das Patchen von Sicherheitslücken im Laufe der Zeit keine Option, da der Code eines Smart Contracts nach der Bereitstellung normalerweise nicht mehr geändert werden kann.
Wie funktioniert die Smart Contract-Verifizierung?
Die formale Verifizierung von Smart Contracts erfolgt, indem die Logik und das gewünschte Verhalten von Smart Contracts als mathematische Aussagen dargestellt werden. Prüfer verwenden dann automatisierte Tools, um zu überprüfen, ob diese Aussagen korrekt sind.
Der Prozess umfasst:
Definieren der Spezifikationen und gewünschten Eigenschaften eines Vertrags in der formellen Sprache.
Übersetzen des Vertragscodes in eine formale Darstellung, beispielsweise mathematische Modelle oder Logik.
Verwenden Sie automatisierte Theorembeweiser oder Modellprüfer, um die Spezifikationen und Eigenschaften des Vertrags zu validieren.
Wiederholen Sie den Überprüfungsprozess, um eventuelle Fehler oder Abweichungen von den gewünschten Eigenschaften zu finden und zu beheben.
Warum die Überprüfung von Smart Contracts wichtig ist
Der Einsatz mathematischer Argumentation trägt dazu bei, sicherzustellen, dass formal überprüfte Smart Contracts frei von Fehlern, Schwachstellen und anderem unbeabsichtigten Verhalten sind. Es trägt auch dazu bei, das Vertrauen in den Vertrag zu stärken, da die Richtigkeit seiner Eigenschaften streng nachgewiesen wurde.
Nachfolgend finden Sie einige Beispiele, wie die Überprüfung intelligenter Verträge dazu beigetragen hat, erhebliche finanzielle Verluste und andere katastrophale Folgen zu verhindern.
Uniswap
Uniswap ist ein bekanntes AMM. Als der Smart Contract Uniswap V1 entwickelt wurde, wurde er formal verifiziert. Vor seiner Veröffentlichung wurden bei dieser formalen Verifizierung Rundungsfehler gefunden und behoben, die dazu hätten führen können, dass Uniswap V1 keine Mittel mehr hatte.
Balancer
Balancer V2 ist auch ein AMM, das formal verifiziert wurde. Bei der formellen Verifizierung wurde eine falsche Gebührenberechnung im Zusammenhang mit der Flash-Loan-Funktionalität im Smart Contract festgestellt und behoben, die die Börse für Diebstahl anfällig gemacht hätte.
Sicherer Mond
SafeMoon V1 enthielt einen subtilen Fehler, der nach der Bereitstellung durch eine formale Überprüfung entdeckt wurde. Es war einem Eigentümer möglich, das Eigentum an dem Vertrag aufzugeben und ihn dann wiederzuerlangen, wenn vor dem Verzicht auf das Eigentum bestimmte Vorgänge durchgeführt wurden.
Dieser Fehler wurde bei den meisten manuellen Prüfungen von SafeMoon V1-Forks übersehen, da zum Auffinden eine Analyse bestimmter Kombinationen von Programmvariablenwerten erforderlich war. Dies ist etwas, das Menschen leicht übersehen können, von Maschinen jedoch leicht erkannt werden kann.
Wie formale Verifizierung und manuelles Auditing zusammenarbeiten
Die formale Überprüfung bietet eine systematische und automatisierte Möglichkeit, die Logik und das Verhalten eines Vertrags anhand seiner gewünschten Eigenschaften zu überprüfen. Dadurch können potenzielle Fehler oder Bugs leichter identifiziert und behoben werden. Dies ist besonders nützlich, um komplexe und subtile Probleme zu finden, die bei einer manuellen Überprüfung möglicherweise nur schwer zu erkennen sind.
Bei der manuellen Prüfung werden Code, Design und Bereitstellung eines Vertrags von Experten geprüft. Der Prüfer nutzt seine Erfahrung und sein Fachwissen, um Sicherheitsrisiken zu identifizieren und die allgemeine Sicherheitslage des Vertrags zu bewerten. Er kann auch bestätigen, dass der formale Überprüfungsprozess korrekt durchgeführt wurde, und nach Problemen suchen, die von automatisierten Tools möglicherweise 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. Dies erhöht die Chancen, Schwachstellen zu finden und zu beheben. Das Ergebnis ist ein mehrstufiger Sicherheitsansatz, der die einzigartigen Fähigkeiten von Mensch und Maschine nutzt.
Abschließende Gedanken
Um die Sicherheit von Smart Contracts zu gewährleisten, ist es wichtig, sowohl eine formelle Überprüfung als auch eine manuelle Prüfung durchzuführen, um eine umfassende und gründliche Bewertung der Sicherheitslage eines Smart Contracts zu gewährleisten.
Obwohl die formelle Überprüfung ressourcenintensiv sein kann, ist sie eine lohnende Investition für Verträge mit hohem Wert oder hohen Risikofaktoren. Letztendlich ist es von entscheidender Bedeutung, der Sicherheit Priorität einzuräumen und sicherzustellen, dass Smart Contracts frei von Fehlern, Schwachstellen und unbeabsichtigtem Verhalten sind.
Weitere Informationen
Was sind Smart Contracts?
Was ist ein Smart Contract-Sicherheitsaudit?
Haftungsausschluss und Risikowarnung: Dieser Inhalt wird Ihnen „wie besehen“ nur zu allgemeinen Informations- und Bildungszwecken präsentiert, ohne Zusicherungen oder Gewährleistungen jeglicher Art. Er ist nicht als finanzielle, rechtliche oder sonstige professionelle Beratung zu verstehen und soll auch nicht den Kauf eines bestimmten Produkts oder einer bestimmten Dienstleistung empfehlen. Sie sollten sich von geeigneten professionellen Beratern beraten lassen. Wenn der Artikel von einem Drittanbieter stammt, beachten Sie bitte, dass die geäußerten Ansichten dem Drittanbieter gehören und nicht unbedingt denen von Binance Academy entsprechen. Weitere Einzelheiten finden Sie in unserem vollständigen Haftungsausschluss. Die Preise digitaler Vermögenswerte können volatil sein. Der Wert Ihrer Investition kann fallen oder steigen und Sie erhalten möglicherweise nicht den investierten Betrag zurück. Sie sind allein für Ihre Investitionsentscheidungen verantwortlich und Binance Academy haftet nicht für etwaige Verluste, die Ihnen entstehen können. Dieses Material ist nicht als finanzielle, rechtliche oder sonstige professionelle Beratung zu verstehen. Weitere Informationen finden Sie in unseren Nutzungsbedingungen und Risikowarnungen.
