Dieser Artikel wurde von einem Community-Mitglied gepostet. Der Autor ist David Tarditi, Vice President of Engineering bei CertiK, einem Web3-Smart-Contract-Audit-Unternehmen.

Zusammenfassung

Die formelle Überprüfung intelligenter Verträge schützt sie vor Fehlern, Schwachstellen und anderen ungünstigen Bedingungen. Dabei wandeln menschliche Experten die Logik des Smart Contracts in mathematische Aussagen um und prüfen dann mithilfe eines automatisierten Prozesses die tatsächliche Logik anhand eines Modells des erwarteten Verhaltens des Vertrags. Durch die Kombination von formaler Verifizierung und manueller Prüfung können wir eine umfassende Bewertung der Sicherheit intelligenter Verträge durchführen.

Einführung

Intelligente Verträge sind Computerprogramme, die auf der Blockchain bereitgestellt werden und automatisch ausgeführt werden, wenn bestimmte Bedingungen erfüllt sind. Intelligente Verträge können sehr einfach oder äußerst komplex sein und Vermögenswerte im Wert von Millionen oder sogar Milliarden Dollar enthalten.

Wenn der Smart-Contract-Code Sicherheitslücken aufweist, kann dies verheerende Folgen haben, beispielsweise den Diebstahl aller Vermögenswerte, die sich im Besitz von Kriminellen befinden. Im Jahr 2021 wurden dem Automated Market Maker (AMM) Uranium Finance aufgrund eines Tippfehlers in einem Smart Contract 50 Millionen US-Dollar gestohlen.

Ebenfalls im Jahr 2021 gab Compound Finance aufgrund eines einzelnen Codierungsfehlers fälschlicherweise Prämien in Höhe von 80 Millionen US-Dollar aus. Im Jahr 2022 wurden aufgrund eines Fehlers im Smart Contract 320 Millionen US-Dollar von der Wormhole Bridge gestohlen.

Daher ist es wichtig, Ihr Smart-Contract-Programm von Anfang an richtig einzurichten. Intelligente Verträge nutzen ein Open-Source-Modell, was bedeutet, dass der Code veröffentlicht wird, sobald der Vertrag bereitgestellt wird. Wenn ein Hacker einen Fehler entdeckt, kann er ihn sofort ausnutzen. Darüber hinaus ist die übliche Praxis, Sicherheitslücken im Laufe der Zeit zu schließen, wirkungslos, da der Code von Smart Contracts nach der Bereitstellung oft 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 erwarteten Verhaltens des Smart Contracts als mathematische Aussagen. Anschließend überprüfen Prüfer mithilfe automatisierter Tools, ob diese Aussagen korrekt sind.

Der Prozess umfasst:

  1. Definieren Sie die Spezifikationen und erwarteten Merkmale des Vertrags in einer formellen Sprache.

  2. Wandeln Sie den Code eines Vertrags in eine formale Aussage um, beispielsweise ein mathematisches Modell oder eine Logik.

  3. Überprüfen Sie Vertragsspezifikationen und -eigenschaften mithilfe automatisierter Theorembeweise oder Modellprüfungen.

  4. Wiederholen Sie den Validierungsprozess, um etwaige Fehler oder Abweichungen von den erwarteten Merkmalen zu finden und zu beheben.

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

Durch die Anwendung mathematischer Überlegungen trägt es dazu bei, sicherzustellen, dass formal verifizierte Smart Contracts frei von Fehlern, Schwachstellen und anderen nachteiligen Situationen sind. Die Verifizierung trägt auch dazu bei, das Vertrauen in den Vertrag zu stärken, da seine Eigenschaften eingehend geprüft wurden und korrekt und zuverlässig sind.

Die folgenden Beispiele zeigen, wie eine intelligente Vertragsverifizierung dazu beitragen kann, erhebliche finanzielle Verluste und andere katastrophale Folgen zu verhindern.

Uniswap

Uniswap ist ein bekannter AMM. Der Uniswap V1-Smart-Vertrag wurde während des Entwicklungsprozesses einer formellen Überprüfung unterzogen. Vor der Veröffentlichung wurden bei dieser formellen Überprüfung einige Rundungsfehler festgestellt und behoben, wodurch verhindert wurde, dass Uniswap V1 Gelder entzogen wurden.

Balancer

Balancer V2 ist ebenfalls ein bewährtes AMM. Bei der formellen Überprüfung wurde ein Gebührenberechnungsfehler in der Flash-Darlehensfunktion im Smart Contract entdeckt und behoben, der die Handelsplattform anfällig für Diebstahl machte.

Sicherer Mond

Nach der Bereitstellung von SafeMoon V1 wurde durch eine formelle Überprüfung ein sehr kleiner Fehler entdeckt. Wenn der Vertragseigentümer bestimmte Vorgänge vor der Aufgabe des Vertrags durchgeführt hat, kann es sein, dass er ihn nach der Aufgabe des Vertrags wiedererlangt.

Bei den meisten manuellen Audits des SafeMoon V1-Forks wird dieser Fehler übersehen, da bestimmte Kombinationen von Programmvariablenwerten analysiert werden müssen, um ihn zu finden. Menschen können dieses Problem leicht übersehen, aber Maschinen können es rechtzeitig erkennen.

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 anhand seiner erwarteten Merkmale zu überprüfen. Dies erleichtert die Identifizierung und Behebung potenzieller Fehler oder Schwachstellen. Dies ist besonders nützlich bei komplexen, subtilen Problemen, die durch manuelle Inspektion schwer zu erkennen wären.

Bei der manuellen Prüfung überprüfen Experten den Code, das Design und die Bereitstellung des Vertrags. Prüfer nutzen ihre Erfahrung und ihr Fachwissen, um Sicherheitsrisiken zu identifizieren und die allgemeine Sicherheitslage des Vertrags zu bewerten. Sie können auch bestätigen, dass der formelle Verifizierungsprozess korrekt durchgeführt wurde, und nach Problemen suchen, die automatisierte Tools möglicherweise nicht erkennen.

Durch die Kombination von formaler Verifizierung und manueller Prüfung können wir eine umfassende Bewertung der Sicherheit intelligenter Verträge durchführen. Dies erhöht die Chancen, Schwachstellen zu finden und zu beheben. Dabei verfolgen wir einen Defense-in-Depth-Sicherheitsansatz, der die Expertise von Mensch und Maschine vereint.

Abschluss

Um die Sicherheit von Smart Contracts zu gewährleisten, müssen formale Verifizierung und manuelle Prüfung kombiniert werden, um eine umfassende und gründliche Bewertung der Sicherheitslage von Smart Contracts zu gewährleisten.

Obwohl die formelle Verifizierung ressourcenintensiver ist, ist sie eine lohnende Investition für Verträge mit hohem Wert oder hohen Risikofaktoren. Letztendlich ist Sicherheit wichtiger als alles andere. Stellen Sie sicher, dass die Sicherheit Priorität hat und dass intelligente Verträge frei von Fehlern, Schwachstellen und unerwünschtem unerwartetem Verhalten sind.

Weiterführende Literatur

  • Was ist ein Smart Contract?

  • Was ist ein Smart-Contract-Sicherheitsaudit?

Haftungsausschluss und Risikowarnung: Die Inhalte dieses Artikels sind Fakten und dienen ausschließlich allgemeinen Informations- und Bildungszwecken und stellen keine Zusicherung oder Gewährleistung dar. Dieser Artikel ist nicht als Finanzberatung zu verstehen und empfiehlt Ihnen nicht den Kauf eines bestimmten Produkts oder einer bestimmten Dienstleistung. Die Preise digitaler Vermögenswerte können schwanken. Der Wert Ihrer Anlage kann sowohl fallen als auch steigen und Sie erhalten möglicherweise nicht den investierten Kapitalbetrag zurück. Sie sind allein für Ihre eigenen Anlageentscheidungen verantwortlich und Binance Academy ist nicht verantwortlich für etwaige Verluste, die Sie erleiden. Dieses Material stellt keine Finanzberatung dar.