Dieser Artikel ist ein Community-Beitrag. Autor: Dimitris Tsapis, Vice President of Engineering bei CertiK, einem Web3-Smart-Contract-Audit-Unternehmen.
TL;DR
Eine formelle Überprüfung stellt sicher, dass Smart Contracts frei von Fehlern, Schwachstellen und anderem unbeabsichtigtem Verhalten sind. Der Prozess beinhaltet, dass ein menschlicher Experte die Smart-Contract-Logik in Form von mathematischen Daten darstellt und sie dann durch einen Prozess führt, bei dem die tatsächliche Logik automatisch mit Modellen des erwarteten Verhaltens des Vertrags verglichen wird. Die Kombination aus formaler Verifizierung und manueller Prüfung ermöglicht eine umfassende Bewertung der Sicherheit intelligenter Verträge.
die Einleitung
Intelligente Verträge sind Computerprogramme, die auf einer Blockchain bereitgestellt werden und automatisch ausgeführt werden, wenn bestimmte Bedingungen erfüllt sind. Sie reichen von einfachen bis hin zu komplexen Programmen und können Vermögenswerte im Wert von mehreren Milliarden Dollar enthalten.
Sicherheitslücken im Smart-Contract-Code können verheerende Folgen haben, einschließlich des Diebstahls aller im Smart Contract enthaltenen Vermögenswerte. Im Jahr 2021 kam es beim automatisierten Market Maker Uranium Finance zu einem Diebstahl von 50 Millionen US-Dollar aufgrund eines einzigen Tippfehlers in einem Smart Contract.
Ebenfalls im Jahr 2021 lieferte das Compound Finance-Protokoll aufgrund eines einzelnen Token-Fehlers unverdiente Belohnungen in Höhe von 80 Millionen US-Dollar. Im Jahr 2022 wurden Wormhole Bridge aufgrund eines Programmierfehlers in einem seiner Smart Contracts 320 Millionen US-Dollar gestohlen.
Es ist wichtig, dass Sie Ihre Smart-Contract-Software gleich beim ersten Mal richtig einsetzen. Smart Contracts sind Open-Source-Verträge, was bedeutet, dass der Code nach der Veröffentlichung des Vertrags der Öffentlichkeit zugänglich ist. Wenn ein Hacker einen Fehler findet, kann er ihn sofort ausnutzen. Darüber hinaus ist der Umgang mit Sicherheitslücken im Laufe der Zeit keine Option, da Smart-Contract-Code nach seiner Bereitstellung in der Regel nicht mehr geändert werden kann.
Wie funktioniert die intelligente Vertragsüberprüfung?
Die formale Verifizierung von Smart Contracts funktioniert durch die Offenlegung der erforderlichen Logik und des Verhaltens von Smart Contracts in Form von Rechendaten. Prüfer können automatisierte Tools zur Validierung von Daten verwenden.
Der Prozess umfasst Folgendes:
Angabe der gewünschten Spezifikationen und Merkmale des Vertrags in der Amtssprache.
Übersetzen von Vertragscodes in eine formale Präsentation, z. B. Modelle oder mathematisch-logische Frameworks.
Verwendung von Theorembeweis- oder Modellprüfungstools zur Prüfung von Vertragsspezifikationen und -merkmalen.
Wiederholen Sie den Verifizierungsprozess, um eventuelle Fehler oder Abweichungen von den erforderlichen Merkmalen zu finden und zu korrigieren.
Warum ist die Überprüfung intelligenter Verträge wichtig?
Der Einsatz mathematischer Argumente trägt dazu bei, sicherzustellen, dass formal verifizierte Smart Contracts frei von Fehlern, Schwachstellen und anderem unbeabsichtigtem Verhalten sind. Es trägt auch dazu bei, das Vertrauen in den Vertrag zu stärken, da dessen Eigenschaften sorgfältig überprüft wurden.
Hier sind einige Beispiele dafür, wie eine intelligente Vertragsverifizierung dazu beitragen kann, erhebliche finanzielle Verluste und andere schlimme Folgen zu verhindern.
Uniswap
Uniswap ist ein bekannter automatisierter Market Maker. Als der Smart-Vertrag Uniswap V1 entwickelt wurde, wurde er offiziell verifiziert. Vor seiner Einführung konnte dieser offizielle Verifizierungsprozess Rundungsfehler finden und korrigieren, die zum Diebstahl von Uniswap V1-Geldern geführt hätten.
Balancer
Balancer V2 ist außerdem ein offiziell verifizierter automatisierter Market Maker. Durch den offiziellen Verifizierungsprozess konnten falsche Gebührenkonten gefunden und korrigiert werden, und es wurde eine Flash-Darlehensfunktion in den Smart Contract integriert, die die Handelsplattform einem Diebstahlsrisiko aussetzen könnte.
Sicherer Mond
SafeMoon V1 enthielt einen unbemerkten Fehler, der nach seiner Veröffentlichung durch offizielle Überprüfung entdeckt wurde. Dem Eigentümer war es möglich, das Eigentum an dem Vertrag aufzugeben und ihn erneut zu erwerben, wenn bestimmte Vorgänge vor der Eigentumsübertragung durchgeführt wurden.
Der Fehler bleibt bei den meisten manuellen Audits von SafeMoon V1-Forks unbemerkt, da für die Suche nach ihm die Analyse bestimmter Sätze von Programmvariablenwerten erforderlich ist. Dies ist etwas, das für Menschen leicht zu übersehen ist, für Maschinen jedoch leicht zu finden ist.
Wie formale Verifizierung und manuelle Prüfung zusammenarbeiten
Die formale Verifizierung bietet eine systematische und automatische Möglichkeit, die Logik und das Verhalten eines Vertrags anhand seiner gewünschten Eigenschaften zu überprüfen. Dies erleichtert das Erkennen und Beheben potenzieller Fehler oder Bugs. Dies ist besonders nützlich, um komplexe, unbemerkte Probleme zu finden, die bei einem manuellen Scan möglicherweise schwer zu erkennen sind.
Der manuelle Prüfungsprozess umfasst die fachkundige Prüfung des Vertragscodes und der Vertragsgestaltung sowie deren Veröffentlichung. Der Prüfer nutzt sein Fachwissen, um Sicherheitsrisiken zu identifizieren und den Sicherheitsstatus des Vertrags im Allgemeinen zu bewerten. Außerdem wird bestätigt, dass der formelle Verifizierungsprozess korrekt abgeschlossen wurde, und es wird geprüft, ob Probleme vorliegen, die von automatisierten Tools möglicherweise nicht erkannt werden.
Die Kombination aus formaler Verifizierung und manueller Prüfung ermöglicht eine umfassende Bewertung der Sicherheit intelligenter Verträge. Dies erhöht die Wahrscheinlichkeit, eventuelle Schwachstellen zu finden und zu beheben. Das Ergebnis ist ein defensiv ausgerichteter Sicherheitsansatz, der die einzigartigen Fähigkeiten von Menschen und Maschinen nutzt.
Abschließende Gedanken
Um die Sicherheit von Smart Contracts zu gewährleisten, ist es notwendig, sowohl einen formellen Verifizierungsprozess als auch eine manuelle Prüfung durchzuführen, um eine umfassende und genaue Bewertung des Sicherheitsstatus des Smart Contracts zu gewährleisten.
Obwohl die formale Verifizierung ressourcenintensiv sein kann, ist sie eine lohnende Investition für intelligente Verträge mit hohem Wert oder hohem Risiko. Schließlich ist es wichtig, der Sicherheit Priorität einzuräumen und sicherzustellen, dass intelligente Verträge frei von Fehlern, Schwachstellen und anderem unbeabsichtigtem Verhalten sind.
Verwandte Artikel
Was ist ein Smart Contract?
Was ist ein Sicherheitsaudit für Smart Contracts?
Haftungsausschluss und Risikowarnung: Dieser Inhalt wird Ihnen „wie besehen“ nur zu allgemeinen Informations- und Bildungszwecken und ohne jegliche Zusicherungen oder Gewährleistungen jeglicher Art zur Verfügung gestellt. Es ist weder als Finanzberatung zu verstehen, noch soll es den Kauf eines bestimmten Produkts oder einer bestimmten Dienstleistung empfehlen. Die Preise digitaler Vermögenswerte können volatil sein. Der Wert Ihrer Investition kann steigen oder fallen, und Sie erhalten möglicherweise nicht den investierten Betrag zurück. Sie allein sind für Ihre Anlageentscheidungen verantwortlich und Binance Academy ist nicht verantwortlich für etwaige Verluste, die Ihnen entstehen. Dies ist keine Finanzberatung.