In einem früheren Artikel haben wir die erweiterte formale Verifikation von Zero-Knowledge Proof (ZKP)-Systemen besprochen: Wie man eine ZK-Anweisung verifiziert. Durch die formale Überprüfung jeder zkWasm-Anweisung können wir die technische Sicherheit und Korrektheit der gesamten zkWasm-Schaltung vollständig gewährleisten. In diesem Artikel konzentrieren wir uns auf die Perspektive der Schwachstellenerkennung, analysieren spezifische Schwachstellen, die während der Auditing- und Verifizierungsprozesse identifiziert wurden, und die daraus gewonnenen Erkenntnisse. Eine allgemeine Diskussion über die erweiterte formale Verifizierung von ZKP-Blockchains finden Sie im Artikel über die erweiterte formale Verifizierung von ZKP-Blockchains.

Bevor wir auf ZK-Schwachstellen eingehen, wollen wir zunächst verstehen, wie CertiK die formale ZK-Verifizierung durchführt. Bei komplexen Systemen wie der ZK Virtual Machine (zkVM) besteht der erste Schritt bei der formalen Verifikation (FV) darin, klar zu definieren, was verifiziert werden muss und welche Eigenschaften es hat. Dies erfordert eine umfassende Überprüfung des Designs, der Codeimplementierung und des Testaufbaus des ZK-Systems. Dieser Prozess überschneidet sich mit regulären Audits, unterscheidet sich jedoch dadurch, dass nach der Überprüfung die Verifizierungsziele und -eigenschaften festgelegt werden müssen. Bei CertiK bezeichnen wir dies als revisionsorientierte Verifizierung. Auditierungs- und Verifizierungsarbeiten sind in der Regel integriert. Für zkWasm haben wir sowohl Audits als auch formale Verifizierungen gleichzeitig durchgeführt.

Was ist eine ZK-Schwachstelle?

Das Kernmerkmal von Zero-Knowledge-Proof-Systemen (ZKP) besteht darin, dass sie die Übertragung eines kurzen verschlüsselten Nachweises von Berechnungen, die offline oder privat ausgeführt wurden (z. B. Blockchain-Transaktionen), an einen ZKP-Verifizierer ermöglichen. Die Prüfstelle prüft und bestätigt den Nachweis, um sicherzustellen, dass die Berechnung wie behauptet erfolgt ist. In diesem Zusammenhang würde eine ZK-Schwachstelle es einem Hacker ermöglichen, gefälschte ZK-Beweise für falsche Transaktionen einzureichen und diese vom ZKP-Verifizierer akzeptieren zu lassen.

Für einen zkVM-Prüfer umfasst der ZK-Beweisprozess das Ausführen eines Programms, das Generieren von Ausführungsdatensätzen für jeden Schritt und das Konvertieren dieser Ausführungsdatensätze in eine Reihe numerischer Tabellen (ein Prozess, der als "Arithmetisierung" bezeichnet wird). Diese Zahlen müssen eine Reihe von Einschränkungen (die "Schaltung") erfüllen, zu denen die Beziehungen zwischen bestimmten Tabellenzellen, feste Konstanten, Datenbanksuchbedingungen zwischen Tabellen und Polynomgleichungen (oder "Gatter") gehören, die jedes Paar benachbarter Tabellenzeilen erfüllen muss. Die On-Chain-Verifizierung kann das Vorhandensein einer Tabelle bestätigen, die alle Einschränkungen erfüllt, ohne die spezifischen Zahlen in der Tabelle preiszugeben.

Rechentabelle in zkWasm

Die Genauigkeit jeder Einschränkung ist entscheidend. Jeder Fehler in einer Einschränkung, ob sie zu schwach ist oder fehlt, könnte es einem Hacker ermöglichen, irreführende Beweise vorzulegen. Diese Tabellen scheinen eine gültige Ausführung eines Smart Contracts darzustellen, sind es aber in Wirklichkeit nicht. Im Vergleich zu herkömmlichen VMs verstärkt die Undurchsichtigkeit von zkVM-Transaktionen diese Schwachstellen. In Nicht-ZK-Chains werden die Details der Transaktionsberechnungen öffentlich in der Blockchain aufgezeichnet; zkVMs speichern diese Details jedoch nicht in der Kette. Dieser Mangel an Transparenz macht es schwierig, die Einzelheiten eines Angriffs zu bestimmen oder sogar, ob ein Angriff stattgefunden hat.

Die ZK-Schaltung, die die Ausführungsregeln von zkVM-Anweisungen erzwingt, ist äußerst komplex. Für zkWasm umfasst die Implementierung seiner ZK-Schaltung über 6.000 Zeilen Rust-Code und Hunderte von Einschränkungen. Diese Komplexität bedeutet oft, dass es mehrere Schwachstellen geben kann, die darauf warten, entdeckt zu werden.

zkWasm-Schaltungsarchitektur

Tatsächlich haben wir durch die Prüfung und formale Überprüfung von zkWasm mehrere solcher Schwachstellen entdeckt. Im Folgenden werden wir zwei repräsentative Beispiele diskutieren und die Unterschiede zwischen ihnen untersuchen.

Code-Schwachstelle: Load8-Dateninjektionsangriff

Die erste Schwachstelle betrifft die Load8-Anweisung in zkWasm. In zkWasm werden Heap-Speicherlesevorgänge mithilfe einer Reihe von LoadN-Anweisungen durchgeführt, wobei N die Größe der zu ladenden Daten ist. Beispielsweise sollte Load64 64-Bit-Daten aus einer zkWasm-Speicheradresse lesen. Load8 sollte 8-Bit-Daten (d. h. ein Byte) aus dem Speicher lesen und mit Nullen auffüllen, um einen 64-Bit-Wert zu erzeugen. Intern stellt zkWasm Speicher als ein Array von 64-Bit-Bytes dar, daher muss es einen Teil des Speicherarrays "auswählen". Dies geschieht über vier Zwischenvariablen (u16_cells), die zusammen den vollständigen 64-Bit-Lastwert bilden.

Die Einschränkungen für diese LoadN-Anweisungen sind wie folgt definiert:

Diese Einschränkung ist in drei Fälle unterteilt: Load32, Load16 und Load8. Load64 hat keine Einschränkungen, da die Speichereinheiten genau 64 Bit groß sind. Für den Fall Load32 stellt der Code sicher, dass die hohen 4 Byte (32 Bit) in der Speichereinheit Null sein müssen.

Für den Fall Load16 stellt der Code sicher, dass die hohen 6 Byte (48 Bit) in der Speichereinheit Null sein müssen.

Für den Fall Load8 sollte es erforderlich sein, dass die hohen 7 Byte (56 Bit) in der Speichereinheit Null sind. Leider ist dies im Code nicht der Fall.

Wie Sie sehen können, sind nur die hohen 9 bis 16 Bit auf Null beschränkt. Die anderen hohen 48 Bit können einen beliebigen Wert haben und trotzdem als "Aus dem Speicher gelesen" durchgehen.

Durch Ausnutzen dieser Schwachstelle kann ein Hacker den ZK-Beweis einer legitimen Ausführungssequenz manipulieren, wodurch die Load8-Anweisung diese unerwarteten Bytes lädt, was zu einer Datenbeschädigung führt. Darüber hinaus kann es durch sorgfältige Anordnung von umgebendem Code und Daten zu falschen Ausführungen und Übertragungen kommen, was zu Daten- und Asset-Diebstahl führt. Diese gefälschten Transaktionen könnten die Prüfungen der zkWasm-Prüfer bestehen und von der Blockchain fälschlicherweise als legitime Transaktionen erkannt werden.

Die Behebung dieser Schwachstelle ist eigentlich ganz einfach.

Diese Schwachstelle stellt eine Klasse von ZK-Schwachstellen dar, die als "Code-Schwachstellen" bezeichnet werden, da sie aus der Implementierung des Codes stammen und durch geringfügige lokale Codeänderungen leicht behoben werden können. Wie Sie vielleicht zustimmen, sind diese Schwachstellen für die Menschen auch relativ einfacher zu identifizieren.

Design-Schwachstelle: Gefälschter Rückkehrangriff

Werfen wir einen Blick auf eine weitere Schwachstelle, diesmal in Bezug auf den Aufruf und die Rückgabe von zkWasm. Aufruf und Rückgabe sind grundlegende VM-Anweisungen, die es einem ausgeführten Kontext (z. B. einer Funktion) ermöglichen, einen anderen aufzurufen und die Ausführung des aufrufenden Kontexts fortzusetzen, nachdem der Aufgerufene seine Ausführung abgeschlossen hat. Jeder Aufruf erwartet später eine Rückgabe. Die dynamischen Daten, die von zkWasm während des Lebenszyklus von Aufruf und Rückgabe nachverfolgt werden, werden als "Anrufrahmen" bezeichnet. Da zkWasm Anweisungen sequentiell ausführt, können alle Aufrufrahmen basierend auf ihrem Auftreten während der Laufzeit sortiert werden. Nachfolgend finden Sie ein Beispiel für einen Aufruf-/Rückgabecode, der auf zkWasm ausgeführt wird.

Benutzer können die Funktion buy_token() aufrufen, um Token zu kaufen (möglicherweise durch Zahlung oder Übertragung anderer wertvoller Gegenstände). Einer der wichtigsten Schritte besteht darin, den Token-Kontostand durch Aufrufen der Funktion add_token() um 1 zu erhöhen. Da der ZK-Beweiser selbst die Datenstruktur des Aufrufrahmens nicht unterstützt, werden die Ausführungstabelle (E-Tabelle) und die Sprungtabelle (J-Tabelle) benötigt, um den vollständigen Verlauf dieser Aufrufrahmen aufzuzeichnen und zu verfolgen.

Die obige Abbildung veranschaulicht den Prozess des Aufrufs von add_token() durch buy_token() und die Rückkehr von add_token() zu buy_token(). Es ist zu sehen, dass der Token-Kontostand um 1 steigt. In der Ausführungstabelle belegt jeder Ausführungsschritt eine Zeile, einschließlich der aktuell ausgeführten Aufrufrahmennummer, des aktuellen Kontextfunktionsnamens (nur zur Veranschaulichung), der Nummer der aktuell ausgeführten Anweisung innerhalb der Funktion und der aktuellen Anweisung, die in der Tabelle gespeichert ist (nur zur Veranschaulichung). In der Sprungtabelle belegt jeder Aufrufrahmen eine Zeile, in der die Nummer seines Aufruferrahmens, der Kontextname der Aufruferfunktion (nur zur Veranschaulichung) und die nächste Anweisungsposition des Aufruferrahmens (damit der Frame zurückgegeben werden kann) gespeichert werden. In beiden Tabellen gibt es eine Spalte "jops", die nachverfolgt, ob es sich bei der aktuellen Anweisung um einen Call/Return handelt (in der Ausführungstabelle) und die Gesamtzahl der Call/Return-Anweisungen für diesen Frame (in der Jump-Tabelle).

Wie erwartet sollte jeder Aufruf eine entsprechende Rückgabe haben, und jeder Frame sollte nur einen Aufruf und eine Rückgabe haben. Wie in der obigen Abbildung gezeigt, ist der "jops"-Wert für den ersten Frame in der Sprungtabelle 2, entsprechend der ersten und dritten Zeile in der Ausführungstabelle, wobei der "jops"-Wert 1 ist. Im Moment sieht alles normal aus.

Hier gibt es jedoch ein Problem: Während ein Aufruf und eine Rückgabe die Anzahl der "Jops" für den Frame auf 2 erhöhen, führen zwei Aufrufe oder zwei Rückgaben ebenfalls zu einer Anzahl von 2. Zwei Aufrufe oder zwei Rückgaben pro Frame mögen absurd erscheinen, aber es ist wichtig, sich daran zu erinnern, dass ein Hacker genau das versuchen würde, indem er die Erwartungen bricht.

Sie sind jetzt vielleicht aufgeregt, aber haben wir das Problem wirklich gefunden?

Es stellt sich heraus, dass zwei Aufrufe kein Problem darstellen, da die Einschränkungen der Ausführungstabelle und der Sprungtabelle verhindern, dass zwei Aufrufe in dieselbe Zeile eines Frames codiert werden, da jeder Aufruf eine neue Frame-Nummer generiert, d. h. die aktuelle Aufruf-Frame-Nummer plus 1.

Bei zwei Rückgaben ist die Situation jedoch nicht so günstig: Da bei der Rückgabe kein neuer Frame erstellt wird, könnte ein Hacker tatsächlich die Ausführungstabelle und die Sprungtabelle einer legitimen Ausführungssequenz abrufen und gefälschte Rückgaben (und entsprechende Frames) injizieren. Beispielsweise könnte das vorherige Ausführungstabellen- und Sprungtabellenbeispiel von buy_token(), in dem add_token() aufgerufen wird, von einem Hacker für das folgende Szenario manipuliert werden:

Der Hacker hat zwei gefälschte Rückgaben zwischen dem ursprünglichen Aufruf und der Rückgabe in die Ausführungstabelle eingefügt und eine neue gefälschte Framezeile in der Sprungtabelle hinzugefügt (die ursprüngliche Rückgabe und die nachfolgenden Schritte zur Ausführung von Anweisungen in der Ausführungstabelle müssen um 4 erhöht werden). Da die Anzahl der "Jops" für jede Zeile in der Jump-Tabelle 2 beträgt, sind die Einschränkungen erfüllt, und der zkWasm-Proof-Checker würde den "Proof" dieser gefälschten Ausführungssequenz akzeptieren. Wie aus der Abbildung ersichtlich, erhöht sich der Token-Kontostand um das 3-fache statt um das 1-fache. Daher könnte der Hacker 3 Token zum Preis von 1 erhalten.

Es gibt verschiedene Möglichkeiten, dieses Problem anzugehen. Ein naheliegender Ansatz besteht darin, Aufrufe und Rückgaben getrennt zu verfolgen und sicherzustellen, dass jeder Frame genau einen Aufruf und eine Rückgabe hat.

Sie haben vielleicht bemerkt, dass wir bisher keine einzige Codezeile für diese Sicherheitsanfälligkeit angezeigt haben. Der Hauptgrund ist, dass es keine problematische Codezeile gibt; Die Codeimplementierung ist perfekt auf die Tabellen- und Einschränkungsentwürfe abgestimmt. Das Problem liegt im Design selbst, ebenso wie die Lösung.

Man könnte meinen, dass diese Schwachstelle offensichtlich sein sollte, aber in Wirklichkeit ist sie es nicht. Dies liegt daran, dass es eine Lücke gibt zwischen "zwei Calls oder zwei Returns führen auch zu einer 'Jops'-Anzahl von 2" und "zwei Returns sind tatsächlich möglich". Letzteres erfordert eine detaillierte und umfassende Analyse verschiedener Einschränkungen in der Ausführungstabelle und der Sprungtabelle, was es schwierig macht, vollständige informelle Schlussfolgerungen durchzuführen.

Vergleich zweier Schwachstellen

Die "Load8 Data Injection Vulnerability" und die "Forgery Return Vulnerability" haben beide das Potenzial, es Hackern zu ermöglichen, ZK-Proofs zu manipulieren, falsche Transaktionen zu erstellen, Proof-Prüfer zu täuschen und sich an Diebstahl oder Hijacking zu beteiligen. Ihre Natur und die Art und Weise, wie sie entdeckt wurden, sind jedoch ganz anders.

Die "Load8 Data Injection Vulnerability" wurde beim Audit von zkWasm entdeckt. Dies war keine leichte Aufgabe, da wir Hunderte von Einschränkungen in über 6.000 Zeilen Rust-Code und Dutzenden von zkWasm-Anweisungen überprüfen mussten. Trotzdem war die Schwachstelle relativ einfach zu erkennen und zu bestätigen. Da diese Schwachstelle vor Beginn der formellen Überprüfung behoben wurde, wurde sie während des Überprüfungsprozesses nicht festgestellt. Wenn diese Schwachstelle während des Audits nicht entdeckt worden wäre, könnten wir erwarten, dass sie bei der Überprüfung der Load8-Anweisung gefunden wird.

Die "Forgery Return Vulnerability" wurde bei der formellen Überprüfung nach dem Audit entdeckt. Ein Grund, warum wir es während des Audits nicht entdeckt haben, ist, dass zkWasm über einen Mechanismus verfügt, der "jops" ähnelt und "mops" genannt wird und Speicherzugriffsanweisungen verfolgt, die historischen Daten für jede Speichereinheit während der zkWasm-Laufzeit entsprechen. Die Einschränkungen für die Anzahl der Mops sind in der Tat korrekt, da nur eine Art von Speicheranweisung, Speicherschreibvorgänge, verfolgt werden und die historischen Daten jeder Speichereinheit unveränderlich sind und nur einmal geschrieben werden (die Anzahl der Mops-Einheiten beträgt 1). Aber selbst wenn wir diese potenzielle Schwachstelle während des Audits bemerkt hätten, wären wir immer noch nicht in der Lage gewesen, jedes mögliche Szenario ohne strenge formale Argumentation zu allen relevanten Einschränkungen einfach zu bestätigen oder auszuschließen, da es tatsächlich keine falsche Codezeile gibt.

Zusammenfassend lässt sich sagen, dass diese beiden Schwachstellen zu den Kategorien "Code-Schwachstellen" bzw. "Design-Schwachstellen" gehören. Code-Schwachstellen sind relativ einfach, leichter zu entdecken (fehlerhafter Code) und leichter zu begründen und zu bestätigen. Design-Schwachstellen können sehr subtil sein, schwieriger zu entdecken (kein "fehlerhafter" Code) und schwieriger zu begründen und zu bestätigen.

Best Practices zum Erkennen von ZK-Schwachstellen

Basierend auf unserer Erfahrung mit der Prüfung und formellen Überprüfung von zkVM und anderen ZK- und Nicht-ZK-Chains finden Sie hier einige Vorschläge, wie Sie ZK-Systeme am besten schützen können:

Überprüfung des Codes und des Designs

Wie bereits erwähnt, können sowohl der Code als auch das Design von ZK Schwachstellen enthalten. Beide Arten von Schwachstellen können die Integrität des ZK-Systems gefährden und müssen daher behoben werden, bevor das System in Betrieb genommen wird. Ein Problem bei ZK-Systemen im Vergleich zu Nicht-ZK-Systemen besteht darin, dass Angriffe schwieriger zu erkennen und zu analysieren sind, da ihre Rechendetails nicht öffentlich zugänglich sind oder in der Kette gespeichert werden. Infolgedessen wissen die Menschen möglicherweise, dass ein Hackerangriff stattgefunden hat, aber sie kennen möglicherweise nicht die technischen Details, wie es dazu gekommen ist. Dies macht die Kosten für jede ZK-Schwachstelle sehr hoch. Folglich ist auch der Wert der Gewährleistung der Sicherheit von ZK-Systemen im Vorfeld sehr hoch.

Durchführung von Audits und formalen Verifizierungen

Die beiden hier besprochenen Schwachstellen wurden durch Auditing und formale Überprüfung entdeckt. Einige mögen annehmen, dass die formale Verifizierung allein die Notwendigkeit einer Überwachung überflüssig macht, da alle Schwachstellen durch formale Verifizierung erkannt werden. Wir empfehlen jedoch, beides durchzuführen. Wie zu Beginn dieses Artikels erläutert, beginnt eine qualitativ hochwertige formale Verifizierungsarbeit mit einer gründlichen Überprüfung, Inspektion und informellen Begründung des Codes und des Designs, die sich mit der Prüfung überschneidet. Darüber hinaus kann das Auffinden und Beheben einfacherer Schwachstellen während der Prüfung den formalen Verifizierungsprozess vereinfachen und rationalisieren.

Wenn Sie sowohl ein Audit als auch eine formale Überprüfung für ein ZK-System durchführen, ist es optimal, beides gleichzeitig durchzuführen. Dies ermöglicht es Auditoren und formalen Verifizierungsingenieuren, effizient zusammenzuarbeiten und möglicherweise mehr Schwachstellen zu entdecken, da für die formale Verifizierung qualitativ hochwertige Audit-Eingaben erforderlich sind.

Wenn Ihr ZK-Projekt bereits einer Prüfung (Kudos) oder mehreren Audits (großes Lob) unterzogen wurde, empfehlen wir Ihnen, eine formale Überprüfung der Schaltung auf der Grundlage der vorherigen Auditergebnisse durchzuführen. Unsere Erfahrung mit Auditing und formaler Verifizierung in Projekten wie zkVM und anderen, sowohl ZK als auch Nicht-ZK, hat wiederholt gezeigt, dass die formale Verifizierung oft Schwachstellen erfasst, die während der Audits übersehen werden. Angesichts der Natur von ZKP sollten ZK-Systeme zwar eine bessere Blockchain-Sicherheit und Skalierbarkeit bieten als Nicht-ZK-Lösungen, aber die Kritikalität ihrer Sicherheit und Korrektheit ist viel höher als bei herkömmlichen Nicht-ZK-Systemen. Daher übersteigt der Wert einer qualitativ hochwertigen formalen Verifikation für ZK-Systeme den von Nicht-ZK-Systemen bei weitem.

Gewährleistung der Sicherheit von Schaltkreisen und Smart Contracts

ZK-Anwendungen bestehen in der Regel aus zwei Komponenten: Schaltkreise und Smart Contracts. Für Anwendungen, die auf zkVM basieren, gibt es universelle zkVM-Schaltungen und Smart-Contract-Anwendungen. Für Anwendungen, die nicht auf zkVM basieren, gibt es anwendungsspezifische ZK-Schaltungen zusammen mit entsprechenden Smart Contracts, die auf der L1-Chain oder am anderen Ende einer Bridge bereitgestellt werden.

Unsere Audit- und formalen Verifizierungsbemühungen für zkWasm beziehen sich nur auf die zkWasm-Schaltung. Aus Sicht der allgemeinen Sicherheit für ZK-Anwendungen ist es jedoch von entscheidender Bedeutung, auch ihre Smart Contracts zu prüfen und formell zu verifizieren. Schließlich wäre es bedauerlich, wenn nach erheblichen Anstrengungen in die Gewährleistung der Schaltkreissicherheit eine Nachlässigkeit bei der Prüfung von Smart Contracts zu einer Kompromittierung der Anwendung führen würde.

Zwei Arten von Smart Contracts verdienen besondere Aufmerksamkeit. Der erste Typ verarbeitet direkt ZK-Proofs. Obwohl sie möglicherweise nicht groß sind, ist ihr Risiko außergewöhnlich hoch. Der zweite Typ umfasst mittlere bis große Smart Contracts, die auf zkVM laufen. Wir wissen, dass diese Verträge manchmal sehr komplex sein können und die wertvollsten einer Prüfung und Verifizierung unterzogen werden sollten, zumal ihre Ausführungsdetails nicht in der Kette sichtbar sind. Glücklicherweise ist die formale Verifizierung für Smart Contracts nach jahrelanger Entwicklung jetzt praktikabel und für geeignete hochwertige Ziele vorbereitet.

Fassen wir die Auswirkungen der formalen Verifikation (FV) auf ZK-Systeme und deren Komponenten mit den folgenden Punkten zusammen.

Aussage:

1. Dieser Artikel wurde von [panewslab] reproduziert, das Urheberrecht liegt beim ursprünglichen Autor [CertiK], wenn Sie Einwände gegen den Nachdruck haben, wenden Sie sich bitte an das Gate Learn-Team, und das Team wird es so schnell wie möglich gemäß den entsprechenden Verfahren behandeln.

2. Haftungsausschluss: Die in diesem Artikel geäußerten Ansichten und Meinungen stellen nur die persönlichen Ansichten des Autors dar und stellen keine Anlageberatung dar.

3. Andere Sprachversionen des Artikels werden vom Gate Learn-Team übersetzt und nicht in Gate.io erwähnt, der übersetzte Artikel darf nicht vervielfältigt, verbreitet oder plagiiert werden.