In dieser Artikelserie zur erweiterten formalen Verifizierung von Zero-Knowledge-Proofs haben wir die Verifizierung von ZK-Anweisungen und eine eingehende Analyse von zwei ZK-Schwachstellen besprochen.

Wie im öffentlichen Bericht (https://skynet.certik.com/projects/zkwasm) und im Code-Repository (https://github.com/CertiKProject/zkwasm-fv) gezeigt wird, ist jede zkWasm-Anweisung formal verifiziert, fanden wir und jede Schwachstelle 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 demonstriert 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) vs. ZK Virtual Machine (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 basierend auf der operativen Semantik der Sprache. Wie in der folgenden Abbildung dargestellt, gilt: Wenn der aktuelle Status einer Zeile der Datenstruktur in der Ausführungstabelle SR ist und dieser Status als Status SH in der High-Level-Spezifikation der Wasm-Maschine ausgedrückt wird, dann ist der Status SR' der Die nächste Zeile in der Ausführungstabelle 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 mit 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 Artikel festgestellt haben, im Wesentlichen eine Ganzzahloperation modulo einer großen Primzahl, 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 herkömmlichen 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 einen Speicherdatentyp, der als Byte-Array implementiert ist, das den physischen Speicher darstellt und in die Methoden Set32 und GetPtr geschrieben und gelesen wird. Um eine Speicheranweisung zu implementieren, ruft Geth Set32 auf, um den physischen Speicher zu ändern.

func opMstore(pc *uint64, interpreter *EVMInterpreter, scope *ScopeContext) ([]byte, error) { // Pop-Wert des Stacks mStart, val := scope.Stack.pop(), scope.Stack.pop() scope.Memory.Set32(mStart.Uint64(), &val) return nil, nil}

Beim Korrektheitsnachweis des obigen Interpreters haben wir bewiesen, dass sein High-Level-Status und sein Low-Level-Status 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 Spalten für Daten fester Größe in der Ausführungstabelle (ähnlich den Registern in CPUs), sie können jedoch nicht zur Verarbeitung von Datenstrukturen 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. Aufrufstapeln verwendet werden.

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

int balance, amount;void main () {balance = 100; amount = 10;balance -= amount; // abheben}

Der Inhalt und die Struktur der Ausführungstabelle sind recht einfach. Es verfügt über 6 Ausführungsschritte (EID1 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 die Daten an diese Adresse schreibt, und die End-EID ist die EID des nächsten Ausführungsschritts, der die Daten an 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 regulären VM-Interpretern: Die Speichertabelle ist kein veränderlicher Speicher, der nach und nach aktualisiert wird, sondern enthält einen Verlauf aller Speicherzugriffe während des gesamten Ausführungs-Trace. Um die Arbeit des Programmierers zu vereinfachen, 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 Write-Alloc-Funktion:

let memory_table_lookup_heap_write1 = allocator .alloc_memory_table_lookup_write_cell_with_value( "store write res1", constraint_builder, eid, move |____| constant_from!(LocationType::Heap as u64), move |meta| load_block_index.expr(meta), // Adresse move |____| constant_from!(0), // ist 32-Bit move |____| constant_from!(1), // (immer) aktiviert );letstore_value_in_heap1=memory_table_lookup_heap_write1.value_cell;

Die Alloc-Funktion ist für die Handhabung von Sucheinschränkungen zwischen Tabellen und arithmetischen Einschränkungen verantwortlich, die die aktuelle EID mit Speichertabelleneinträgen verknüpfen. 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.

In ähnlicher Weise werden Speicherleseanweisungen mithilfe 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.

Die Struktur der formalen Verifizierung sollte den in der zu verifizierenden Software verwendeten Abstraktionen entsprechen, damit der Beweis der gleichen 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 des Variablentyps 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 der Set- und Get-Funktionen entsprechen Legen Sie die entsprechenden Adressen fest, die durch Datenzuordnung vorgenommen wurden. Wir können beweisen:

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

Speichertabellen-Lookup_Read_CelleIDTypeOffsetValue

Aber

get(memory_ateidtype)offset=EinigerWert

• Und wenn die folgenden Einschränkungen gelten

memory_table_lookup_write_cell EID Typ Offset Wert

Aber

memory_at (eid+1) Typ = setze (memory_at eid Typ) Offsetwert

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 leicht manipuliert werden, indem sie eine Datenzeile einfügen und beliebige Werte zurückgeben.

Am Beispiel des Auszahlungsprogramms hat der Angreifer die Möglichkeit, falsche Daten in den Kontostand einzuschleusen, indem er vor dem Auszahlungsvorgang einen Speicherschreibvorgang 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 bei 100 $ bleibt.

Um sicherzustellen, dass die Speichertabelle (und Sprungtabelle) nur gültige Einträge enthält, die durch die tatsächlich ausgeführten Speicherschreibbefehle (und Aufruf- und Rückgabebefehle) 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 Typ 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

(Speichertabellensuche_Schreiben_Zellen-ID-Typ-Offsetwert)

Und die folgenden neuen Einschränkungen werden festgelegt

(mops_ateidtyp)=1

Aber

(Speicher_bei(EID+1)Typ)=Setze(Speicher_bei(EIDTyp)Offsetwert

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 weglässt und einen böswilligen neuen Speichertabelleneintrag für eine andere, nicht verwandte Anweisung erstellt.

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 die 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 Sucheinschränkungen jeder Anweisung können wir nachweisen, dass sie nicht weniger Einträge als erwartet erstellt, was zu der Schlussfolgerung führt, dass jedes verfolgte Segment [i ... numRows] nicht weniger Einträge als erwartet erstellt:

Lemma cum_mops_bound': für alle n i, 0 ≤ i -> i + Z.of_nat n = etable_numRow ->MTable.cum_mops(etable_valueseid_celli)(max_eid+1)≥instructions_mops'in.

Zweitens: Wenn Sie zeigen 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.of_nat n = etable_numRow -> MTable.cum_mops (etable_values ​​eid_cell i) (max_eid+1) ≤ instructions_mops' i n ->MTable.cum_mops(etable_valueseid_celli)(max_eid+1)=instructions_mops'in.

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_valueseid_cell(Z.of_natn))(max_eid+1)=instructions_mops(Z.of_natn)

Die Überprüfung erfolgt durch Zusammenfassung von n. 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:

cum_mopsn=Anleitung_mopsn

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

mopp_bei n + mit_mopp (n+1) = Anweisungsmopp n + Anweisungen_mopp (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.

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 ist es das wert? 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 muss ein weiterer Faktor berücksichtigt werden. Das zkWasm-Projekt ist ziemlich groß, 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 gibt es 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_cell i) > 1 -> nth_error xs (Z.to_nat (etable_values ​​offset_cell i - 1)) = Einige y ->state_rel(i+1)(update_stack(incr_iidst)(y::xs)).

Die erste Satzaussage

opcode_mops_correct LocalGet i

Wenn es erweitert wird, 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 aufgebaut wird, dass sie mit der in der Implementierung verwendeten Abstraktionsschicht übereinstimmt, sodass jede Anweisung als separates Modul basierend auf der Get-Set-Schnittstelle implementiert werden kann, wie bei einer regulären chemischen Verifizierung durch einen Interpreter .