Erweiterte formale Verifizierung von Zero-Knowledge-Beweisen: So verifizieren Sie eine ZK-Anweisung

Um genau zu verstehen, wie die formale Verifizierungstechnologie auf zkVM (Zero-Knowledge Virtual Machine) angewendet wird, konzentriert sich dieser Artikel auf die Verifizierung einer einzelnen Anweisung. Zur Gesamtsituation der fortgeschrittenen formalen Verifizierung von ZKP (Zero-Knowledge Proof) verweisen wir auf den Artikel „Advanced Formal Verification of Zero-Knowledge Proof Blockchain“, den wir zeitgleich veröffentlicht haben.

Was ist die Überprüfung von ZK-Anweisungen?

zkVM (Zero-Knowledge Virtual Machine) ist in der Lage, kurze Beweisobjekte als Beweis dafür zu erstellen, dass ein bestimmtes Programm auf bestimmten Eingaben ausgeführt und erfolgreich beendet werden kann. Im Web3.0-Bereich ermöglicht die Anwendung von zkVM einen hohen Durchsatz, da der L1-Knoten nur einen kurzen Beweis für den Übergang des Smart Contracts vom Eingabezustand in den Ausgabezustand verifizieren muss und die eigentliche Ausführung des Vertragscodes außerhalb der Kette abgeschlossen werden kann.

Der zkVM-Prüfer führt zunächst das Programm aus, um einen Ausführungsdatensatz für jeden Schritt zu generieren, und wandelt dann die Ausführungsdatensatzdaten in einen Satz numerischer Tabellen um (dieser Vorgang wird als „Arithmetik“ bezeichnet). Diese Zahlen müssen eine Reihe von Einschränkungen (d. h. Schaltkreisen) erfüllen, zu denen die Verbindungsgleichungen zwischen bestimmten Tabellenzellen, feste Konstanten, Datenbanksucheinschränkungen zwischen Tabellen und die Einschränkungen gehören, die zwischen jedem Paar benachbarter Tabellenzeilen erfüllt werden müssen Gleichungen (auch bekannt als „Tore“). Durch die On-Chain-Verifizierung kann bestätigt werden, dass tatsächlich eine Tabelle vorhanden ist, die alle Einschränkungen erfüllt, und gleichzeitig sichergestellt werden, dass die spezifischen Zahlen in der Tabelle nicht sichtbar sind.

Die Ausführung jeder VM-Anweisung unterliegt vielen solchen Einschränkungen. Hier bezeichnen wir diesen Satz von Einschränkungen der VM-Anweisung als ihre „ZK-Anweisung“. Unten finden Sie ein Beispiel für eine in Rust geschriebene zkWasm-Speicherladeanweisungsbeschränkung.

ZK Die formale Verifizierung von Anweisungen erfolgt durch die Durchführung formaler Überlegungen zu diesen Codes, die wir zunächst in eine formale Sprache übersetzen.

Auch wenn nur eine einzelne Einschränkung einen Fehler enthält, ist es für einen Angreifer möglich, einen böswilligen ZK-Beweis einzureichen. Die dem böswilligen Beweis entsprechende Datentabelle entspricht nicht der rechtlichen Funktionsweise des Smart Contracts. Im Gegensatz zu Nicht-ZK-Ketten wie Ethereum, bei denen viele Knoten unterschiedliche EVM-Implementierungen (Ethereum Virtual Machine) ausführen, wodurch es unwahrscheinlich ist, dass derselbe Fehler zur gleichen Zeit am selben Ort auftritt, verfügt eine zkVM-Kette nur über eine einzige VM-Implementierung . Allein aus dieser Perspektive ist die ZK-Kette fragiler als das traditionelle Web3.0-System.

Was noch schlimmer ist, ist, dass es im Gegensatz zu Nicht-ZK-Ketten nicht nur sehr schwierig ist, die spezifischen Details des Angriffs zu ermitteln, sondern auch, da die Berechnungsdetails von zkVM-Transaktionen nicht in der Kette übermittelt und gespeichert werden Es kann auch eine große Herausforderung sein, den Angriff überhaupt zu erkennen.

Das zkVM-System erfordert eine äußerst strenge Prüfung. Leider ist die Korrektheit der zkVM-Schaltung schwer zu garantieren.

Warum ist es schwierig, ZK-Anweisungen zu überprüfen?

VM (Virtual Machine) ist einer der komplexesten Teile der Web3.0-Systemarchitektur. Die leistungsstarken Funktionen intelligenter Verträge sind der Kern der Unterstützung von Web3.0-Funktionen. Ihre Leistung beruht auf den zugrunde liegenden VMs, die sowohl flexibel als auch komplex sind: Um allgemeine Rechen- und Speicheraufgaben zu erfüllen, müssen diese VMs in der Lage sein, zahlreiche Anweisungen zu unterstützen und Staaten. Beispielsweise erfordert die Geth-Implementierung des EVM mehr als 7.500 Zeilen Go-Sprachcode. Ebenso groß und komplex ist die ZK-Schaltung, die die Ausführung dieser Befehle einschränkt. Wie im zkWasm-Projekt erfordert die Implementierung der ZK-Schaltung mehr als 6000 Zeilen Rust-Code.

zkWasm-Schaltungsarchitektur

Im Vergleich zu dedizierten ZK-Schaltungen, die in ZK-Systemen verwendet werden, die für bestimmte Anwendungen (z. B. private Zahlungen) entwickelt wurden, sind zkVM-Schaltungen viel größer: ihre verbindlichen Regeln. Die Anzahl kann eins sein oder zwei Größenordnungen größer, und die arithmetische Tabelle kann Hunderte von Spalten mit Millionen von numerischen Zellen umfassen.

Was bedeutet die Verifizierung von ZK-Anweisungen?

Wir möchten hier die Richtigkeit der XOR-Anweisung in zkWasm überprüfen. Technisch gesehen entspricht die Ausführungstabelle von zkWasm einer legalen Wasm-VM-Ausführungssequenz. Aus Makroperspektive möchten wir also überprüfen, dass jede Ausführung dieser Anweisung immer einen neuen legalen zkVM-Status generiert: Jede Zeile in der Tabelle entspricht einem legalen Status der VM und die folgende Zeile wird immer von generiert Ausführen der entsprechenden VM-Anweisungen. Die folgende Abbildung zeigt den formalen Satz für die Korrektheit der XOR-Anweisung.

Hier gibt „state_rel i st“ an, dass Status „st“ der legale zkVM-Status des Smart-Vertrags in Schritt „i“ ist. Wie Sie vielleicht erraten haben, ist der Beweis von „state_rel (i+1) ...“ nicht trivial.

Wie überprüfe ich den ZK-Befehl?

Obwohl die rechnerische Semantik einer Ganzzahl zutrifft, führen Sie eine XOR-Berechnung durch und speichern Sie dann die berechnete neue Ganzzahl wieder im selben Stapel. Darüber hinaus sollten die Ausführungsschritte dieser Anweisung in den gesamten Smart-Contract-Ausführungsprozess integriert werden und die Reihenfolge und der Zeitpunkt der Ausführung müssen korrekt sein.

Daher sollte der Ausführungseffekt des XOR-Befehls darin bestehen, zwei Zahlen aus dem Datenstapel zu entfernen, ihre XOR-Ergebnisse zu übertragen und gleichzeitig den Programmzähler zu erhöhen, um auf den nächsten Befehl des Smart Contracts zu zeigen.

Es ist nicht schwer zu erkennen, dass die Definition der Korrektheitseigenschaften hier im Allgemeinen der Situation sehr ähnlich ist, mit der wir bei der Überprüfung herkömmlicher Bytecode-VMs (wie dem EVM-Interpreter in Ethereum L1-Knoten) konfrontiert sind. Es basiert auf einer abstrakten Definition des Maschinenzustands auf hoher Ebene (hier Stapelspeicher und Ausführungsfluss) und einer Definition des erwarteten Verhaltens jeder Anweisung (hier arithmetische Logik).

Wie wir jedoch weiter unten sehen werden, unterscheidet sich der Überprüfungsprozess für ihre Korrektheit aufgrund der besonderen Natur von ZKP und zkVM oft stark von dem bei regulären VMs. Nur um die einzelne Anweisung zu überprüfen, die wir hier haben, hängt die Richtigkeit vieler Tabellen in zkWASM ab: Darunter befindet sich eine Bereichstabelle, die zur Begrenzung der Wertgröße verwendet wird, und eine Bittabelle (Bittabelle), die für das Zwischenergebnis der binären Bitberechnung verwendet wird , Eine Ausführungstabelle, die VM-Status mit konstanter Größe pro Zeile speichert (ähnlich den Daten in Registern und Latches in einer physischen CPU) und Speicher, der Tabellen und Sprünge für VM-Status (Speicher, Datenstapel und Aufrufstapel) dynamisch variabler Größe darstellt Tische.

Schritt eins: Stapelspeicher

Ähnlich wie bei einer herkömmlichen VM müssen wir sicherstellen, dass die beiden ganzzahligen Parameter der Anweisung vom Stapel gelesen werden können und dass ihre XOR-Ergebniswerte korrekt in den Stapel zurückgeschrieben werden. Auch die formale Darstellung des Stapels kommt mir ziemlich bekannt vor (es gibt auch globalen Speicher und Heap-Speicher, aber der XOR-Befehl verwendet sie nicht).

zkVM verwendet ein komplexes Schema zur Darstellung dynamischer Daten, da der ZK-Prover Datenstrukturen wie Stacks oder Arrays nicht nativ unterstützt. Im Gegensatz dazu zeichnet die Speichertabelle für jeden auf den Stapel verschobenen Wert eine separate Zeile auf, und einige der Spalten werden verwendet, um die effektive Zeit des Eintrags anzugeben. Natürlich können die Daten in diesen Tabellen von Angreifern kontrolliert werden, daher müssen einige Einschränkungen auferlegt werden, um sicherzustellen, dass die Tabelleneinträge tatsächlich den tatsächlichen Stapelanweisungen bei der Vertragsausführung entsprechen. Dies wird durch sorgfältige Berechnung der Anzahl der Stack-Pushes während der Programmausführung erreicht. Bei der Überprüfung jeder Anweisung müssen wir sicherstellen, dass diese Zählung immer korrekt ist. Darüber hinaus verfügen wir über eine Reihe von Lemmata, die die von einer einzelnen Anweisung generierten Einschränkungen mit den Tabellensuchen und Zeitbereichsprüfungen in Beziehung setzen, die Stapeloperationen implementieren. Auf der obersten Ebene werden die Zählbeschränkungen für Speicheroperationen wie folgt definiert.

Schritt 2: Arithmetische Operationen

Ähnlich wie bei herkömmlichen VMs möchten wir sicherstellen, dass die bitweise XOR-Operation korrekt ist. Das scheint einfach zu sein, schließlich sind unsere physischen Computer-CPUs dazu in der Lage, dies auf einmal zu tun.

Aber für zkVM ist das eigentlich nicht einfach. Die einzigen arithmetischen Anweisungen, die vom ZK-Beweiser nativ unterstützt werden, sind Addition und Multiplikation. Um binäre Bitoperationen durchzuführen, verwendet VM ein ziemlich komplexes Schema, bei dem eine Tabelle die Operationsergebnisse auf fester Byteebene speichert und die andere Tabelle als „Notizblock“ fungiert, um zu zeigen, wie Operationen an mehreren Tabellenzeilen ausgeführt werden. Die 64-Bit-Zahl wird in 8 Bytes zerlegt und anschließend wieder zusammengesetzt, um das Ergebnis zu ergeben.

ZkWasm-Bittabellenspezifikationsfragment

ist eine sehr einfache XOR-Operation in traditionellen Programmiersprachen, aber hier sind viele Lemmata erforderlich, um die Richtigkeit dieser Hilfstabellen zu überprüfen. Für unsere Anleitung haben wir:

Schritt drei: Ausführungsablauf

Ähnlich wie bei einer herkömmlichen VM müssen wir sicherstellen, dass der Wert des Programmzählers korrekt aktualisiert wird. Bei sequentiellen Anweisungen wie XOR muss der Programmzähler nach jedem Schritt um eins erhöht werden.

Da zkWasm für die Ausführung von Wasm-Code konzipiert ist, stellt es auch sicher, dass die Unveränderlichkeit des Wasm-Speichers während der gesamten Ausführung erhalten bleibt.

Traditionelle Programmiersprachen bieten native Unterstützung für Datentypen wie boolesche Werte, 8-Bit-Ganzzahlen und 64-Bit-Ganzzahlen, aber in ZK-Schaltkreisen ändern sich Variablen immer innerhalb des Bereichs von Ganzzahlen modulo großer Primzahlen (≈ 2254). . Da VMs typischerweise mit 64 Bit laufen, müssen Schaltungsentwickler ein System von Einschränkungen verwenden, um sicherzustellen, dass sie über die richtigen numerischen Bereiche verfügen, und formale Verifizierungsingenieure müssen invariante Eigenschaften dieser Bereiche während des gesamten Verifizierungsprozesses verfolgen. Überlegungen zu Ausführungsabläufen und Ausführungstabellen betreffen alle anderen Hilfstabellen. Daher müssen wir überprüfen, ob die Bereiche aller Tabellendaten korrekt sind.

Ähnlich wie bei der Verwaltung von Speicheroperationsnummern benötigt zkVM einen ähnlichen Satz von Lemmata, um den Kontrollfluss zu überprüfen. Insbesondere erfordert jede Aufruf- und Rückgabeanweisung die Verwendung eines Aufrufstapels. Der Aufrufstapel wird mithilfe eines Tabellenschemas implementiert, das dem Datenstapel ähnelt. Für den XOR-Befehl müssen wir den Aufrufstapel nicht ändern, aber bei der Überprüfung des gesamten Befehls müssen wir dennoch verfolgen und überprüfen, ob die Anzahl der Kontrollflussoperationen korrekt ist.

Überprüfen Sie diese Anweisung

Lassen Sie uns alle Schritte zusammenfassen und den End-to-End-Korrektheitssatz der zkWasm-XOR-Anweisung überprüfen. Die folgenden Überprüfungen werden in einer interaktiven Beweisumgebung durchgeführt, in der jeder Schritt der formalen Konstruktion und des logischen Denkens strengsten maschinellen Prüfungen unterzogen wird.

Wie oben gesehen, ist eine formale Überprüfung der zkVM-Schaltung möglich. Dies ist jedoch eine schwierige Aufgabe, die das Verständnis und die Verfolgung vieler komplexer invarianter Eigenschaften erfordert. Dies spiegelt die Komplexität der zu verifizierenden Software wider: Jedes an der Verifizierung beteiligte Lemma muss vom Schaltungsentwickler korrekt gehandhabt werden. Angesichts der hohen Risiken wäre es sinnvoll, sie durch ein formelles Verifizierungssystem maschinell prüfen zu lassen, anstatt sich ausschließlich auf eine sorgfältige menschliche Überprüfung zu verlassen.

Das obige ist der detaillierte Inhalt vonErweiterte formale Verifizierung von Zero-Knowledge-Beweisen: So verifizieren Sie eine ZK-Anweisung. Für weitere Informationen folgen Sie bitte anderen verwandten Artikeln auf der PHP chinesischen Website!