Erweiterte formale Verifizierung von Zero-Knowledge-Beweisen: So beweisen Sie Zero-Knowledge-Gedächtnis

In dieser Blogreihe über die erweiterte formale Verifizierung von Zero-Knowledge-Proofs haben wir die Verifizierung von ZK-Anweisungen und eine eingehende Analyse von zwei ZK-Schwachstellen besprochen. Wie aus öffentlichen Berichten und Codebasen hervorgeht, haben wir durch die formelle Überprüfung jeder zkWasm-Anweisung jede Schwachstelle gefunden und behoben, sodass wir die technische Sicherheit und Korrektheit der gesamten zkWasm-Schaltung vollständig überprüfen konnten.

Obwohl wir den Prozess der Verifizierung einer zkWasm-Anweisung gezeigt und die vorläufigen Konzepte des zugehörigen Projekts vorgestellt haben, sind Leser, die mit der formalen Verifizierung vertraut sind, möglicherweise mehr daran interessiert, die Verifizierung von zkVM mit anderen kleineren ZK-Systemen oder anderen Arten von Bytecode-VMs zu verstehen An. In diesem Artikel werden wir einige der technischen Punkte, die bei der Validierung des zkWasm-Speichersubsystems auftreten, ausführlich besprechen. Der Speicher ist der einzigartigste Teil von zkVM, und seine Handhabung ist für alle anderen zkVM-Überprüfungen von entscheidender Bedeutung.

Formale Verifizierung: virtuelle Maschine (VM) versus virtuelle ZK-Maschine (zkVM)

Unser ultimatives Ziel ist es, die Korrektheit von zkWasm zu überprüfen, was dem Korrektheitssatz gewöhnlicher Bytecode-Interpreter (VMs, wie z. B. dem von Ethereum-Knoten verwendeten EVM-Interpreter) ähnelt. Das heißt, jeder Ausführungsschritt des Dolmetschers entspricht einem rechtlichen Schritt, der auf der operativen Semantik der Sprache basiert. Wie in der Abbildung unten gezeigt, gilt Folgendes: Wenn der aktuelle Status der Datenstruktur des Bytecode-Interpreters SL ist und dieser Status in der High-Level-Spezifikation der Wasm-Maschine als Status SH markiert ist, dann tritt der Interpreter dort in den Status SL' über muss ein sein Der entsprechende legale High-Level-Zustand SH', und die Wasm-Spezifikation legt fest, dass SH zu SH' wechseln muss.

Ebenso verfügt zkVM über einen ähnlichen Korrektheitssatz: Jede neue Zeile in der zkWasm-Ausführungstabelle entspricht einem rechtlichen Schritt, der auf der operativen Semantik der Sprache basiert. Wie in der folgenden Abbildung dargestellt, gilt: Wenn der aktuelle Status einer Zeile der Datenstruktur in der Ausführungstabelle SR ist und dieser Status in der High-Level-Spezifikation der Wasm-Maschine als Status SH ausgedrückt wird, dann der Status der nächsten Zeile der Ausführungstabelle SR' muss einem High-Level-Zustand SH' entsprechen, und die Wasm-Spezifikation schreibt vor, dass SH zu SH' wechseln muss.

Es ist ersichtlich, dass die Spezifikation von High-Level-Zuständen und Wasm-Schritten sowohl in VM als auch in zkVM konsistent ist, sodass auf frühere Verifizierungserfahrungen von Programmierspracheninterpretern oder -compilern zurückgegriffen werden kann. Das Besondere an der zkVM-Verifizierung ist die Art der Datenstruktur, die den Low-Level-Status des Systems darstellt.

Erstens ist der zk-Beweiser, wie wir in einem früheren Blogbeitrag erwähnt haben, im Wesentlichen eine Ganzzahloperation modulo großer Primzahlen, während die Wasm-Spezifikation und der normale Interpreter 32-Bit- oder 64-Bit-Ganzzahlen verarbeiten. Der größte Teil der zkVM-Implementierung beinhaltet dies, daher muss während der Überprüfung auch eine entsprechende Verarbeitung durchgeführt werden. Dabei handelt es sich jedoch um ein „lokales“ Problem: Jede Codezeile wird aufgrund der arithmetischen Operationen, die sie verarbeiten muss, komplexer, die Gesamtstruktur des Codes und des Beweises ändert sich jedoch nicht.

Ein weiterer wesentlicher Unterschied besteht darin, wie Datenstrukturen mit dynamischer Größe gehandhabt werden. In einem regulären Bytecode-Interpreter werden Speicher, Datenstapel und Aufrufstapel alle als veränderbare Datenstrukturen implementiert. In ähnlicher Weise stellt die Wasm-Spezifikation Speicher als Datentyp mit Get/Set-Methoden dar. Beispielsweise verfügt der EVM-Interpreter von Geth über den Datentyp „Memory“, der als Byte-Array implementiert ist, das den physischen Speicher darstellt und über die Methoden „Set 32“ und „GetPtr“ geschrieben und gelesen wird. Um eine Speicheranweisung zu implementieren, ruft Geth „Set 32“ auf, um den physischen Speicher zu ändern.

Funktion opMstore(pc *uint 64, Interpreter *EVMInterpreter, Bereich *ScopeContext) ([]Byte, Fehler) {

// Pop-Wert des Stapels

mStart, Wert := Umfang.Stack.pop(), Umfang.Stack.pop()

Umfang.Speicher.Set 32(mStart.Uint 64(), Wert)

Rückgabe Null, Null

}

Beim Korrektheitsnachweis des obigen Interpreters haben wir bewiesen, dass sein High-Level-Zustand und sein Low-Level-Zustand miteinander übereinstimmen, nachdem wir dem konkreten Speicher im Interpreter und dem abstrakten Speicher in der Spezifikation Werte zugewiesen haben. Dies ist relativ einfach.

Bei zkVM wird die Situation jedoch komplizierter.

Speichertabelle und Speicherabstraktionsschicht von zkWasm

In zkVM gibt es in der Ausführungstabelle Spalten für Daten fester Größe (ähnlich den Registern in der CPU), sie können jedoch nicht für die Verarbeitung von Datenstrukturen mit dynamischer Größe verwendet werden, die durch das Nachschlagen von Hilfstabellen implementiert werden. Die Ausführungstabelle von zkWasm verfügt über eine EID-Spalte mit den Werten 1, 2, 3 ... und zwei Hilfstabellen, eine Speichertabelle und eine Sprungtabelle, die zur Darstellung von Speicherdaten bzw. Aufrufstapel verwendet werden.

Im Folgenden finden Sie ein Beispiel für die Implementierung eines Auszahlungsprogramms:

int Guthaben, Betrag;

Leere Haupt () {

Saldo = 100;

  Betrag = 10;

Guthaben -= Betrag; // abheben

}

Der Inhalt und die Struktur der Ausführungstabelle sind recht einfach. Es verfügt über 6 Ausführungsschritte (EID 1 bis 6), jeder Schritt hat eine Zeile, in der sein Opcode (Opcode) und, wenn es sich bei der Anweisung um einen Speicherlese- oder -schreibbefehl handelt, seine Adresse und Daten aufgeführt sind:

Jede Zeile in der Speichertabelle enthält Adresse, Daten, Start-EID und End-EID. Die Start-EID ist die EID des Ausführungsschritts, der diese Daten an diese Adresse schreibt, und die End-EID ist die EID des nächsten Ausführungsschritts, der diese Adresse schreibt. (Es enthält auch eine Zählung, die wir später ausführlich besprechen.) Für die Wasm-Speicherlesebefehlsschaltung verwendet sie eine Suchbeschränkung, um sicherzustellen, dass es einen geeigneten Eintrag in der Tabelle gibt, sodass die EID des Lesebefehls darin enthalten ist reichen vom Anfang bis zum Ende im Inneren. (In ähnlicher Weise entspricht jede Zeile der Sprungtabelle einem Frame des Aufrufstapels, und jede Zeile ist mit der EID des Aufrufanweisungsschritts gekennzeichnet, der sie erstellt hat.)

Dieses Speichersystem unterscheidet sich stark von einem normalen VM-Interpreter: Die Speichertabelle ist kein veränderlicher Speicher, der nach und nach aktualisiert wird, sondern enthält einen Verlauf aller Speicherzugriffe während der gesamten Ausführungsverfolgung. Um Programmierern die Arbeit zu erleichtern, stellt zkWasm eine Abstraktionsschicht bereit, die durch zwei praktische Eingabefunktionen implementiert wird. Sie sind:

alloc_memory_table_lookup_write_cell

Und

Speichertabellen-Lookup-Lesezelle zuweisen

Seine Parameter sind wie folgt:

Beispielsweise enthält der Code, der die Speicheranweisungen in zkWasm implementiert, einen Aufruf der Funktion „Write Alloc“:

let memory_table_lookup_heap_write1 = Allocator

.alloc_memory_table_lookup_schreibe_Zelle_mit_Wert(

"Speichern Sie Schreibres. 1",

Einschränkungsersteller,

Fest,

Verschiebe |____| konstant_von!(Standorttyp::Heap als u 64),

verschieben |meta| load_block_index.expr(meta),   // Adresse

Verschiebe |____| constant_from!( 0),             // ist 32-Bit

Verschieben |____| constant_from!( 1),             // (immer) aktiviert

    );

Lassen Sie store_value_in_heap1 = memory_table_lookup_heap_write1.value_cell;

Die Funktion „alloc“ ist für die Handhabung von Sucheinschränkungen zwischen Tabellen und arithmetischen Einschränkungen verantwortlich, die die aktuelle „eid“ mit Speichertabelleneinträgen in Beziehung setzen. Daher können Programmierer diese Tabellen als gewöhnlichen Speicher behandeln, und der Wert von „store_value_in_heap1“ wurde der Adresse „load_block_index“ zugewiesen, nachdem der Code ausgeführt wurde.

Ebenso werden Speicherleseanweisungen mit der Funktion „read_alloc“ implementiert. In der obigen beispielhaften Ausführungssequenz gibt es eine Lesebeschränkung für jeden Ladebefehl und eine Schreibbeschränkung für jeden Speicherbefehl, und jede Beschränkung wird durch einen Eintrag in der Speichertabelle erfüllt.

mtable_lookup_write(Zeile 1.eid, Zeile 1.store_addr, Zeile 1.store_value)

                       ⇐ (Zeile 1.eid= 1 ∧ Zeile 1.store_addr=balance ∧ Zeile 1.store_value= 100 ∧ ...)

mtable_lookup_write(Zeile 2.eid, Zeile 2.store_addr, Zeile 2.store_value)

                      ⇐ (Zeile 2.eid=2 ∧ Zeile 2.store_addr=Betrag ∧ Zeile 2.store_value=10 ∧ ...)

mtable_lookup_read(Zeile 3.eid, Zeile 3.load_addr, Zeile 3.load_value)

                      ⇐ ( 2

mtable_lookup_read(Zeile 4.eid, Zeile 4.load_addr, Zeile 4.load_value)

                      ⇐ ( 1

mtable_lookup_write(Zeile 6.eid, Zeile 6.store_addr, Zeile 6.store_value)

                      ⇐ (Zeile 6.eid= 6 ∧ Zeile 6.store_addr=balance ∧ Zeile 6.store_value= 90 ∧ ...)

Die Struktur der formalen Verifizierung sollte den in der zu verifizierenden Software verwendeten Abstraktionen entsprechen, damit der Beweis derselben Logik wie der Code folgen kann. Für zkWasm bedeutet dies, dass wir die Speichertabellenschaltung und die Funktion „Lese-/Schreibzelle zuweisen“ als Modul überprüfen müssen, das wie ein variabler Speicher fungiert. Bei einer solchen Schnittstelle kann die Überprüfung jeder Befehlsschaltung auf ähnliche Weise wie bei einem regulären Interpreter durchgeführt werden, während die zusätzliche ZK-Komplexität im Speichersubsystemmodul gekapselt ist.

Bei der Verifizierung haben wir die Idee umgesetzt, dass „die Speichertabelle tatsächlich als veränderliche Datenstruktur betrachtet werden kann“. Das heißt, schreiben Sie die Funktion „memory_at type“, die die Speichertabelle vollständig durchsucht und die entsprechende Adressdatenzuordnung erstellt. (Der Wertebereich der Variablen „Typ“ umfasst hier drei verschiedene Arten von Wasm-Speicherdaten: Heap, Datenstapel und globale Variablen.) Anschließend beweisen wir, dass die von der Alloc-Funktion generierten Speicherbeschränkungen der Verwendung von Set und Get entsprechen Datenänderungen, die durch die entsprechende Adressdatenzuordnung vorgenommen werden. Wir können beweisen:

• Für jede Eid, wenn die folgenden Einschränkungen gelten

memory_table_lookup_read_cell EID Typ Offset Wert

Aber

get (memory_at eid type) offset = Irgendein Wert

• Und wenn die folgenden Einschränkungen gelten

memory_table_lookup_write_cell EID Typ Offset Wert

Aber

memory_at (eid+ 1) Typ = Set (memory_at eid Typ) Offset-Wert

Danach kann die Überprüfung jeder Anweisung auf Get- und Set-Operationen auf der Adressdatenzuordnung basieren, ähnlich wie bei Nicht-ZK-Bytecode-Interpretern.

zkWasms Mechanismus zur Zählung von Speicherschreibvorgängen

Die obige vereinfachte Beschreibung offenbart jedoch nicht den gesamten Inhalt der Speichertabelle und der Sprungtabelle. Im Rahmen von zkVM können diese Tabellen von Angreifern manipuliert werden, die die Speicherladeanweisungen leicht manipulieren und durch Einfügen einer Datenzeile beliebige Werte zurückgeben können.

Am Beispiel des Auszahlungsprogramms hat der Angreifer die Möglichkeit, falsche Daten in den Kontostand einzuschleusen, indem er vor dem Auszahlungsvorgang einen Speicherschreibvorgang im Wert von 110 US-Dollar fälscht. Dieser Vorgang kann durch Hinzufügen einer Datenzeile zur Speichertabelle und Ändern der Werte vorhandener Zellen in der Speichertabelle und der Ausführungstabelle erreicht werden. Dies führt zu „kostenlosen“ Abhebungen, da der Kontostand nach dem Vorgang immer noch bei 100 $ bleibt.

Um sicherzustellen, dass die Speichertabelle (und Sprungtabelle) nur gültige Einträge enthält, die durch die tatsächlich ausgeführten Speicherschreibanweisungen (und Aufruf- und Rückgabeanweisungen) generiert wurden, verwendet zkWasm einen speziellen Zählmechanismus, um die Anzahl der Einträge zu überwachen. Insbesondere verfügt die Speichertabelle über eine eigene Spalte, die die Gesamtzahl der in den Speicher geschriebenen Einträge verfolgt. Gleichzeitig enthält die Ausführungstabelle auch einen Zähler, der die Anzahl der für jeden Befehl erwarteten Speicherschreibvorgänge zählt. Stellen Sie sicher, dass die beiden Zählwerte konsistent sind, indem Sie eine Gleichheitsbeschränkung festlegen. Die Logik dieser Methode ist sehr intuitiv: Jedes Mal, wenn ein Schreibvorgang im Speicher ausgeführt wird, wird dieser einmal gezählt und es sollte ein entsprechender Datensatz in der Speichertabelle vorhanden sein. Daher kann der Angreifer keine weiteren Einträge in die Speichertabelle einfügen.

Die obige logische Aussage ist etwas vage und muss im Prozess des maschinellen Beweises präzisiert werden. Zunächst müssen wir die oben erwähnte Aussage des Memory-Write-Lemmas überarbeiten. Wir definieren die Funktion „mops_at eid type“, um die Speichertabelleneinträge mit einer bestimmten „eid“ und einem bestimmten „type“ zu zählen (die meisten Anweisungen erstellen 0 oder 1 Einträge bei einer eid). Die vollständige Aussage des Theorems erfordert eine zusätzliche Voraussetzung, die besagt, dass keine falschen Speichertabelleneinträge vorhanden sind:

Wenn die folgenden Einschränkungen gelten

(memory_table_lookup_write_cell EID-Typ-Offset-Wert)

Und die folgenden neuen Einschränkungen werden festgelegt

 (mops_at eid-Typ) = 1 

Aber

(memory_at(eid+ 1) Typ) = setze (memory_at eid Typ) Offset-Wert

Dies erfordert, dass unsere Überprüfung präziser ist als im vorherigen Fall. Die bloße Ableitung aus der Gleichheitsbeschränkung, dass die Gesamtzahl der Speichertabelleneinträge der Gesamtzahl der Speicherschreibvorgänge in der Ausführung entspricht, reicht nicht aus, um die Überprüfung abzuschließen. Um die Richtigkeit einer Anweisung zu beweisen, müssen wir wissen, dass jede Anweisung der richtigen Anzahl von Speichertabelleneinträgen entspricht. Wir müssen beispielsweise ausschließen, dass ein Angreifer einen Speichertabelleneintrag für eine Anweisung in der Ausführungssequenz weglassen und einen böswilligen neuen Speichertabelleneintrag für eine andere, nicht verwandte Anweisung erstellen könnte.

Um dies zu beweisen, verwenden wir einen Top-Down-Ansatz, um die Anzahl der Speichertabelleneinträge zu begrenzen, die einer bestimmten Anweisung entsprechen. Dies umfasst drei Schritte. Zunächst schätzen wir die Anzahl der Einträge, die für Anweisungen in der Ausführungsreihenfolge erstellt werden sollten, basierend auf dem Befehlstyp. Wir nennen die erwartete Anzahl von Schreibvorgängen vom i-ten Schritt bis zum Ende der Ausführung „instructions_mops i“ und die entsprechende Anzahl von Einträgen in der Speichertabelle vom i-ten Schritt bis zum Ende der Ausführung „cum_mops (eid i)“ `. Durch die Analyse der Suchbeschränkungen jeder Anweisung können wir beweisen, dass sie nicht weniger Einträge als erwartet erstellt, was zu der Schlussfolgerung führt, dass jedes verfolgte Segment von [i... numRows] nicht weniger als erwartete Einträge erstellt:

Lemma cum_mops_bound': für alle n i,

  0 ≤ i ->

i + Z.von_nat n = etable_numRow ->

MTable.cum_mops (etable_values ​​eid_cell i) (max_eid+ 1) ≥ instructions_mops' i n.

Zweitens: Wenn Sie nachweisen können, dass die Tabelle nicht mehr Einträge als erwartet enthält, dann hat sie genau die richtige Anzahl an Einträgen, was offensichtlich ist.

Lemma cum_mops_equal' : für alle n i,

    0 ≤ i ->

i + Z.von_nat n = etable_numRow ->

    MTable.cum_mops (etable_values ​​eid_cell i) (max_eid+ 1) ≤ instructions_mops' i n ->

    MTable.cum_mops (etable_values ​​eid_cell i) (max_eid+ 1)  = instructions_mops' i n.

Fahren Sie nun mit Schritt drei fort. Unser Korrektheitssatz besagt, dass cum_mops und Instructions_mops für jedes n von Zeile n bis zum Ende der Tabelle immer konsistent sind:

Lemma cum_mops_equal : für alle n,

    0 <= Z.of_nat n < etable_numRow ->

MTable.cum_mops (etable_values ​​eid_cell (Z.of_nat n)) (max_eid+ 1) = instructions_mops (Z.of_nat n)

Die Überprüfung wird durch Zusammenfassen von n abgeschlossen. Die erste Zeile in der Tabelle ist die Gleichheitsbeschränkung von zkWasm, die angibt, dass die Gesamtzahl der Einträge in der Speichertabelle korrekt ist, d. h. cum_mops 0 = instruktionen_mops 0 . Für die folgenden Zeilen sagt uns die Induktionshypothese:

mit Wischmopp n = Wischmopp-Anleitung n

und wir hoffen, es zu beweisen

mit Wischmopp (n+1) = mit Wischmopp-Anweisungen (n+1)

Passen Sie hier auf

mit Wischmopp n = Wischmopp_bei n + mit Wischmopp (n+ 1)

Und

Wischmopp-Anleitung n = Wischmopp-Anleitung n + Wischmopp-Anleitung (n+ 1)

Deshalb können wir bekommen

Wischmopp_bei n + mit Wischmopp (n+ 1) = Wischmopp-Anweisung n + Wischmopp-Anweisungen (n+ 1)

Zuvor haben wir gezeigt, dass jede Anweisung nicht weniger als die erwartete Anzahl an Einträgen erstellt, z. B.

mops_at n ≥ Anweisung_mops n.

Daraus lässt sich schließen

mit Wischmopp (n+1) ≤ mit Wischmopp-Anweisungen (n+1)

Hier müssen wir das zweite Lemma oben anwenden.

(Unter Verwendung eines ähnlichen Lemmas zur Überprüfung der Sprungtabelle kann bewiesen werden, dass jede Aufrufanweisung einen Sprungtabelleneintrag genau erzeugen kann, sodass diese Beweistechnik allgemein anwendbar ist. Wir benötigen jedoch noch weitere Überprüfungsarbeiten, um zu beweisen, dass die Rückgabe korrekt ist Die zurückgegebene EID unterscheidet sich von der EID der aufrufenden Anweisung, die den Aufrufrahmen erstellt hat. Daher benötigen wir auch eine zusätzliche invariante Eigenschaft, um zu deklarieren, dass der EID-Wert während der Ausführungssequenz in eine Richtung erhöht wird.)

Die detaillierte Beschreibung des Beweisprozesses ist typisch für die formale Verifizierung und der Grund dafür, dass die Verifizierung eines bestimmten Codeabschnitts oft länger dauert als das Schreiben. Aber lohnt es sich? In diesem Fall hat es sich gelohnt, da wir beim Beweis einen kritischen Fehler im Zählmechanismus der Sprungtabelle gefunden haben. Dieser Fehler wurde in einem früheren Artikel ausführlich beschrieben. Zusammenfassend lässt sich sagen, dass ältere Versionen des Codes sowohl Aufruf- als auch Rückgabeanweisungen berücksichtigten und ein Angreifer einen falschen Sprung erstellen konnte, indem er der Ausführungssequenz zusätzliche Rückgabeanweisungen hinzufügte, um Platz zu schaffen . Obwohl ein falscher Zählmechanismus die Intuition erfüllen kann, dass jeder Aufruf- und Rückgabebefehl zählt, treten Probleme auf, wenn wir versuchen, diese Intuition in eine präzisere Theoremaussage zu verfeinern.

Gestalten Sie den Proofprozess modular

Aus der obigen Diskussion können wir erkennen, dass zwischen dem Beweis über die Schaltung jeder Anweisung und dem Beweis über die Zählspalte der Ausführungstabelle eine zirkuläre Abhängigkeit besteht. Um die Korrektheit der Befehlsschaltung zu beweisen, müssen wir über die darin enthaltenen Speicherschreibvorgänge nachdenken. Das heißt, wir müssen die Anzahl der Speichertabelleneinträge bei einer bestimmten EID kennen und nachweisen, dass die Speicherschreibvorgänge berücksichtigt werden Die Ausführungstabelle ist korrekt. Außerdem muss nachgewiesen werden, dass jeder Befehl mindestens eine Mindestanzahl an Speicherschreibvorgängen ausführt.

Darüber hinaus ist noch ein weiterer Faktor zu berücksichtigen, sodass die Verifizierungsarbeit modularisiert werden muss, damit mehrere Verifizierungsingenieure die Arbeit aufteilen können. Daher muss bei der Dekonstruktion des Beweises des Zählmechanismus besonderes Augenmerk auf seine Komplexität gelegt werden. Für die LocalGet-Anweisung lauten beispielsweise zwei Theoreme wie folgt:

Theorem opcode_mops_correct_local_get: für alle i,

  0 <= i ->

etable_values ​​eid_cell i > 0 ->

  opcode_mops_correct LocalGet i.

Theorem LocalGetOp_correct : für alle i st y xs,

  0 <= i ->

etable_values enabled_cell i = 1 ->

  mops_at_correct i ->

etable_values ​​(ops_cell LocalGet) i = 1 ->

  state_rel i st ->

wasm_stack st = xs ->

(etable_values Offset_Zelle i) > 1 ->

  n-ter_Fehler xs (Z.to_nat (etable_values offset_cell i - 1)) = Einige y ->

  state_rel (i+ 1) (update_stack (incr_iid st) (y :: xs)).

Die erste Satzaussage

opcode_mops_correct LocalGet i

Im erweiterten Zustand bedeutet dies, dass die Anweisung mindestens einen Speichertabelleneintrag in Zeile i erstellt (die Nummer 1 ist in der LocalGet-Opcode-Spezifikation von zkWasm angegeben).

Der zweite Satz ist der vollständige Korrektheitssatz für die Anweisung, die zitiert

mops_at_correct ich 

Als Hypothese bedeutet dies, dass die Anweisung genau einen Speichertabelleneintrag erstellt.

Ein Verifikationsingenieur kann diese beiden Theoreme unabhängig voneinander beweisen und sie dann mit einem Beweis über die Ausführungstabelle kombinieren, um die Korrektheit des gesamten Systems zu beweisen. Es ist erwähnenswert, dass alle Beweise für einzelne Anweisungen auf der Ebene von Lese-/Schreibeinschränkungen durchgeführt werden können, ohne die spezifische Implementierung der Speichertabelle zu kennen. Daher ist das Projekt in drei Teile gegliedert, die unabhängig voneinander bearbeitet werden können.

Zusammenfassen

Die zeilenweise Überprüfung der Schaltkreise von zkVM unterscheidet sich nicht grundlegend von der Überprüfung von ZK-Anwendungen in anderen Bereichen, da beide ähnliche Überlegungen zu arithmetischen Einschränkungen erfordern. Aus einer übergeordneten Perspektive erfordert die Verifizierung von zkVM viele der gleichen formalen Verifizierungsmethoden, die auch in Programmierspracheninterpretern und -compilern verwendet werden. Der Hauptunterschied besteht hier im dynamisch dimensionierten Status der virtuellen Maschine. Die Auswirkungen dieser Unterschiede können jedoch minimiert werden, indem die Verifizierungsstruktur sorgfältig so strukturiert wird, dass sie der in der Implementierung verwendeten Abstraktionsschicht entspricht, sodass jede Anweisung wie bei einem regulären chemischen Interpreter als unabhängiges Modul basierend auf der Get-Set-Schnittstelle implementiert werden kann Überprüfung.