In questa serie di articoli sulla verifica formale avanzata delle prove a conoscenza zero, abbiamo discusso come verificare le istruzioni ZK e un'analisi approfondita di due vulnerabilità ZK.

Come mostrato nel rapporto pubblico (https://skynet.certik.com/projects/zkwasm) e nel repository del codice (https://github.com/CertiKProject/zkwasm-fv), ogni istruzione zkWasm è formalmente verificata, abbiamo scoperto e risolto ogni vulnerabilità, permettendoci di verificare a pieno la sicurezza tecnica e la correttezza dell'intero circuito zkWasm.

Sebbene abbiamo dimostrato il processo di verifica di un'istruzione zkWasm e introdotto i concetti preliminari del relativo progetto, i lettori che hanno familiarità con la verifica formale potrebbero essere più interessati a comprendere la verifica di zkVM con altri sistemi ZK più piccoli o altri tipi di VM di bytecode SU. In questo articolo discuteremo in modo approfondito alcuni dei punti tecnici incontrati durante la convalida del sottosistema di memoria zkWasm. La memoria è la parte più unica di zkVM e gestirla è fondamentale per tutte le altre verifiche di zkVM.

Verifica formale: macchina virtuale (VM) e ZK Virtual Machine (zkVM)

Il nostro obiettivo finale è verificare la correttezza di zkWasm, che è simile al teorema di correttezza dei normali interpreti di bytecode (VM, come l'interprete EVM utilizzato dai nodi Ethereum). Cioè, ogni fase di esecuzione dell'interprete corrisponde a una fase legale basata sulla semantica operativa della lingua. Come mostrato nella figura seguente, se lo stato corrente della struttura dati dell'interprete bytecode è SL, e questo stato è contrassegnato come stato SH nelle specifiche di alto livello della macchina Wasm, allora quando l'interprete passa allo stato SL', c'è deve essere un Il corrispondente stato legale di alto livello SH', e la specifica Wasm stabilisce che SH deve passare a SH'.

Allo stesso modo, zkVM ha un teorema di correttezza simile: ogni nuova riga nella tabella di esecuzione zkWasm corrisponde a un passaggio legale basato sulla semantica operativa del linguaggio. Come mostrato nella figura seguente, se lo stato corrente di una riga della struttura dati nella tabella di esecuzione è SR, e questo stato è espresso come stato SH nelle specifiche di alto livello della macchina Wasm, allora lo stato SR' della la riga successiva della tabella di esecuzione deve corrispondere a uno stato di alto livello SH' e la specifica Wasm stabilisce che SH deve passare a SH'.

Si può vedere che la specifica degli stati di alto livello e dei passaggi Wasm è coerente sia in VM che in zkVM, quindi può attingere a precedenti esperienze di verifica con interpreti o compilatori di linguaggi di programmazione. La particolarità della verifica zkVM è il tipo di struttura dati che costituisce lo stato di basso livello del sistema.

Innanzitutto, come abbiamo affermato in un articolo precedente, il dimostratore zk è essenzialmente un'operazione su interi modulo un numero primo grande, mentre la specifica Wasm e l'interprete normale trattano interi a 32 o 64 bit. La maggior parte dell'implementazione zkVM prevede questo, pertanto, durante la verifica è necessario eseguire anche l'elaborazione corrispondente. Si tratta però di un problema "locale": ogni riga di codice diventa più complessa a causa delle operazioni aritmetiche che deve gestire, ma la struttura complessiva del codice e della dimostrazione non cambia.

Un'altra differenza importante è il modo in cui vengono gestite le strutture dati di dimensioni dinamiche. In un interprete di bytecode convenzionale, la memoria, lo stack di dati e lo stack di chiamate sono tutti implementati come strutture di dati mutabili. Allo stesso modo, la specifica Wasm rappresenta la memoria come un tipo di dati con metodi get/set. Ad esempio, l'interprete EVM di Geth ha un tipo di dati Memory, che viene implementato come un array di byte che rappresenta la memoria fisica e scritto e letto tramite i metodi Set32 e GetPtr. Per implementare un'istruzione di archiviazione della memoria, Geth chiama Set32 per modificare la memoria fisica.

func opMstore(pc *uint64, interprete *EVMInterpreter, scope *ScopeContext) ([]byte, errore) { // valore pop dello stack mStart, val := scope.Stack.pop(), scope.Stack.pop() scope.Memory.Set32(mStart.Uint64(), &val) return nil, nil}

Nella prova di correttezza dell'interprete di cui sopra, abbiamo dimostrato che il suo stato di alto livello e quello di basso livello corrispondono tra loro dopo aver assegnato valori alla memoria concreta nell'interprete e alla memoria astratta nelle specifiche. Ciò è relativamente semplice.

Tuttavia, con zkVM la situazione diventa più complicata.

La tabella di memoria di zkWasm e il livello di astrazione della memoria

In zkVM, ci sono colonne per dati a dimensione fissa sulla tabella di esecuzione (simili ai registri nelle CPU), ma non può essere utilizzata per gestire strutture di dati a dimensione dinamica, che vengono implementate cercando tabelle ausiliarie. La tabella di esecuzione di zkWasm ha una colonna EID, i cui valori sono 1, 2, 3..., e ha due tabelle ausiliarie, una tabella di memoria e una tabella di salto, che vengono utilizzate rispettivamente per rappresentare i dati di memoria e lo stack di chiamate.

Quello che segue è un esempio di come implementare un programma di prelievo:

int saldo, importo;void main () {saldo = 100; importo = 10;saldo -= importo; // ritirare}

Il contenuto e la struttura della tabella di esecuzione sono abbastanza semplici. Ha 6 passi di esecuzione (da EID1 a 6), ogni passo ha una riga che elenca il suo codice operativo (opcode) e, se l'istruzione è una lettura o scrittura in memoria, il suo indirizzo e i suoi dati:

Ogni riga nella tabella di memoria contiene indirizzo, dati, EID iniziale e EID finale. L'EID iniziale è l'EID della fase di esecuzione che scrive i dati su questo indirizzo e l'EID finale è l'EID della fase di esecuzione successiva che scriverà i dati su questo indirizzo. (Contiene anche un conteggio, di cui parleremo in dettaglio più avanti.) Per il circuito dell'istruzione di lettura della memoria Wasm, utilizza un vincolo di ricerca per garantire che ci sia una voce appropriata nella tabella in modo tale che l'EID dell'istruzione di lettura sia nel vanno dall'inizio alla fine all'interno. (Allo stesso modo, ogni riga della tabella di salto corrisponde a un frame dello stack di chiamate e ogni riga è etichettata con l'EID del passaggio dell'istruzione di chiamata che l'ha creata.)

Questo sistema di memoria differisce notevolmente da un normale interprete VM: invece di una memoria mutabile che viene gradualmente aggiornata, la tabella di memoria contiene una cronologia di tutti gli accessi alla memoria durante la traccia di esecuzione. Per semplificare il lavoro dei programmatori, zkWasm prevede un livello di astrazione, implementato attraverso due comode funzioni di immissione. Sono:

alloc_memory_table_lookup_write_cell

E

Alloc_memory_table_lookup_read_cell

I suoi parametri sono i seguenti:

Ad esempio, il codice che implementa le istruzioni di archiviazione della memoria in zkWasm contiene una chiamata alla funzione write alloc:

let memory_table_lookup_heap_write1 = allocatore .alloc_memory_table_lookup_write_cell_with_value( "store write res1", vincoli_builder, eid, move |____| Constant_from!(LocationType::Heap as u64), move |meta| load_block_index.expr(meta), // indirizzo move |____| costante_da!(0), // è uno spostamento a 32 bit |____|. costante_da!(1), // (sempre) abilitato );letstore_value_in_heap1=memory_table_lookup_heap_write1.value_cell;

La funzione alloc è responsabile della gestione dei vincoli di ricerca tra tabelle e dei vincoli aritmetici che associano l'eid corrente alle voci della tabella di memoria. Da ciò, i programmatori possono trattare queste tabelle come memoria ordinaria e il valore di store_value_in_heap1 è stato assegnato all'indirizzo load_block_index dopo l'esecuzione del codice.

Allo stesso modo, le istruzioni di lettura della memoria vengono implementate utilizzando la funzione read_alloc. Nella sequenza di esecuzione dell'esempio precedente, esiste un vincolo di lettura per ciascuna istruzione di caricamento e un vincolo di scrittura per ciascuna istruzione di memorizzazione e ciascun vincolo è soddisfatto da una voce nella tabella di memoria.

La struttura della verifica formale dovrebbe corrispondere alle astrazioni utilizzate nel software da verificare, in modo che la dimostrazione possa seguire la stessa logica del codice. Per zkWasm, ciò significa che dobbiamo verificare il circuito della tabella di memoria e le funzioni "alloc read/write cell" come un modulo, che si interfaccia come una memoria variabile. Data una tale interfaccia, la verifica di ciascun circuito di istruzione può essere eseguita in modo simile a un normale interprete, mentre la complessità ZK aggiuntiva è incapsulata nel modulo del sottosistema di memoria.

Nella verifica abbiamo implementato l'idea che "la tabella di memoria può effettivamente essere considerata come una struttura dati mutabile". Cioè, scrivi la funzione di tipo memory_at, che scansiona completamente la tabella di memoria e costruisce la corrispondente mappatura dei dati dell'indirizzo. (L'intervallo di valori del tipo di variabile qui è costituito da tre diversi tipi di dati di memoria Wasm: heap, stack di dati e variabili globali.) Quindi, dimostriamo che i vincoli di memoria generati dalla funzione alloc equivalgono all'utilizzo delle funzioni set e get per impostare gli indirizzi corrispondenti. Modifiche dei dati apportate dalla mappatura dei dati. Possiamo dimostrare:

• Per ciascun eid, se valgono i seguenti vincoli

memory_table_lookup_read_celleidtypeoffsetvalue

Ma

get(memory_ateidtype)offset=Un valore

• E, se valgono i seguenti vincoli

memory_table_lookup_write_cell valore di offset del tipo eid

Ma

tipo memory_at (eid+1) = imposta il valore di offset (tipo eid memory_at).

Successivamente, la verifica di ciascuna istruzione può essere basata su operazioni get e set sulla mappa dei dati dell'indirizzo, simili agli interpreti di bytecode non ZK.

Il meccanismo di conteggio delle scritture in memoria di zkWasm

Tuttavia, la descrizione semplificata di cui sopra non rivela tutto il contenuto della tabella di memoria e della tabella di salto. Nell'ambito di zkVM, queste tabelle possono essere manipolate dagli aggressori che possono facilmente manipolare le istruzioni di caricamento della memoria e restituire valori arbitrari inserendo una riga di dati.

Prendendo come esempio il programma di prelievo, l’aggressore ha la possibilità di inserire dati falsi nel saldo del conto falsificando un’operazione di scrittura in memoria di 110 dollari prima dell’operazione di prelievo. Questo processo può essere ottenuto aggiungendo una riga di dati alla tabella di memoria e modificando i valori delle celle esistenti nella tabella di memoria e nella tabella di esecuzione. Ciò comporterà prelievi "gratuiti" poiché il saldo del conto rimarrà a $ 100 dopo l'operazione.

Per garantire che la tabella di memoria (e la tabella di salto) contenga solo voci valide generate dalle istruzioni di scrittura in memoria (e chiamata e ritorno) effettivamente eseguite, zkWasm utilizza uno speciale meccanismo di conteggio per monitorare il numero di voci. Nello specifico, la tabella di memoria ha una colonna dedicata che tiene traccia del numero totale di voci scritte in memoria. Allo stesso tempo, la tabella di esecuzione contiene anche un contatore per contare il numero di operazioni di scrittura in memoria previste per ciascuna istruzione. Assicurati che i due conteggi siano coerenti impostando un vincolo di uguaglianza. La logica di questo metodo è molto intuitiva: ogni volta che viene eseguita un'operazione di scrittura nella memoria, verrà conteggiata una volta e dovrebbe esserci un record corrispondente nella tabella di memoria. Pertanto l'aggressore non può inserire ulteriori voci nella tabella di memoria.

L’affermazione logica di cui sopra è un po’ vaga e, nel processo di dimostrazione meccanizzata, deve essere resa più precisa. Per prima cosa dobbiamo rivedere l’enunciato del lemma memory write menzionato sopra. Definiamo la funzione mops_at eid type per contare le voci della tabella di memoria con un dato eid e tipo (la maggior parte delle istruzioni creerà 0 o 1 voci per un eid). L'enunciazione completa del teorema ha un prerequisito aggiuntivo che afferma che non ci sono voci spurie nella tabella di memoria:

Se valgono i seguenti vincoli

(memory_table_lookup_write_celleidtypeoffsetvalue)

E vengono stabiliti i seguenti nuovi vincoli

(mops_ateidtype)=1

Ma

(memory_at(eid+1)type)=set(memory_ateidtype)valoreoffset

Ciò richiede che la nostra verifica sia più precisa rispetto al caso precedente. Derivare semplicemente dal vincolo di uguaglianza secondo cui il numero totale di voci della tabella di memoria è uguale al numero totale di scritture in memoria nell'esecuzione non è sufficiente per completare la verifica. Per dimostrare la correttezza di un'istruzione, dobbiamo sapere che ciascuna istruzione corrisponde al numero corretto di voci della tabella di memoria. Ad esempio, dobbiamo escludere se un utente malintenzionato possa omettere una voce della tabella di memoria per un'istruzione nella sequenza di esecuzione e creare una nuova voce dannosa della tabella di memoria per un'altra istruzione non correlata.

Per dimostrarlo, utilizziamo un approccio top-down per limitare il numero di voci della tabella di memoria corrispondenti a una determinata istruzione, che prevede tre passaggi. Innanzitutto stimiamo il numero di voci che dovrebbero essere create per le istruzioni nella sequenza di esecuzione in base al tipo di istruzione. Chiamiamo istruzioni_mops i il numero previsto di scritture dall'i-esimo passo alla fine dell'esecuzione, e il numero corrispondente di voci nella tabella di memoria dall'i-esima istruzione alla fine dell'esecuzione cum_mops (eid i). Analizzando i vincoli di ricerca di ciascuna istruzione, possiamo dimostrare che non crea meno voci del previsto, il che porta alla conclusione che ogni segmento [i ... numRows] tracciato crea non meno voci del previsto:

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

In secondo luogo, se è possibile dimostrare che la tabella non contiene più voci del previsto, allora avrà esattamente il numero esatto di voci, il che è ovvio.

Lemma cum_mops_equal' : forall 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)=istruzioni_mops'in.

Ora procedi al passaggio tre. Il nostro teorema di correttezza afferma che per ogni n, cum_mops e instructions_mops sono sempre coerenti dalla riga n fino alla fine della tabella:

Lemma cum_mops_equal : forall 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)

La verifica si effettua riassumendo n. La prima riga nella tabella è il vincolo di uguaglianza di zkWasm, che indica che il numero totale di voci nella tabella di memoria è corretto, ovvero cum_mops 0 = instructions_mops 0. Per le righe seguenti l’ipotesi induttiva ci dice:

cum_mopsn=istruzioni_mopsn

e speriamo di dimostrarlo

cum_mops (n+1) = istruzioni_mops (n+1)

Presta attenzione qui

cum_mops n = mop_at n + cum_mops (n+1)

E

istruzioni_mops n = istruzioni_mops n + istruzioni_mops (n+1)

Pertanto, possiamo ottenere

mops_at n + cum_mops (n+1) = istruzioni_mops n + istruzioni_mops (n+1)

In precedenza, abbiamo dimostrato che ciascuna istruzione creerà non meno del numero previsto di voci, ad es.

mops_at n ≥ istruzione_mops n.

Quindi si può concludere

cum_mops (n+1) ≤ istruzioni_mops (n+1)

Qui dobbiamo applicare il secondo lemma sopra.

Descrivere il processo di prova in modo così dettagliato è tipico della verifica formale ed è il motivo per cui verificare una parte specifica di codice spesso richiede più tempo che scriverla. Ma ne vale la pena? In questo caso ne è valsa la pena perché durante la dimostrazione abbiamo riscontrato un bug critico nel meccanismo di conteggio della tabella di salto. Questo bug è stato descritto in dettaglio in un articolo precedente: in sintesi, le versioni precedenti del codice tenevano conto sia delle istruzioni di chiamata che di quelle di ritorno e un utente malintenzionato poteva creare un salto falso aggiungendo ulteriori istruzioni di ritorno alla sequenza di esecuzione per fare spazio . Sebbene un meccanismo di conteggio errato possa soddisfare l'intuizione che ogni istruzione di chiamata e di ritorno conta, i problemi sorgono quando proviamo a perfezionare questa intuizione in un'enunciazione di teorema più precisa.

Rendi modulare il processo di prova

Dalla discussione sopra, possiamo vedere che esiste una dipendenza circolare tra la dimostrazione relativa al circuito di ciascuna istruzione e la dimostrazione relativa alla colonna count della tabella di esecuzione. Per dimostrare la correttezza del circuito di istruzioni, dobbiamo ragionare sulle scritture in memoria al suo interno, ovvero dobbiamo conoscere il numero di voci della tabella di memoria in un EID specifico e dobbiamo dimostrare che l'operazione di scrittura in memoria conta; la tabella di esecuzione è corretta; e per questo è necessario anche dimostrare che ogni istruzione esegua almeno un numero minimo di scritture in memoria.

Inoltre, c’è un altro fattore che deve essere considerato. Il progetto zkWasm è piuttosto grande, quindi il lavoro di verifica deve essere modularizzato in modo che più ingegneri di verifica possano dividere il lavoro. Pertanto, è necessario prestare particolare attenzione alla sua complessità quando si decostruisce la dimostrazione del meccanismo di conteggio. Ad esempio, per l'istruzione LocalGet, ci sono due teoremi come segue:

Teorema opcode_mops_correct_local_get : forall i, 0 <= i -> etable_values ​​eid_cell i > 0 -> opcode_mops_correct LocalGet i.

Teorema LocalGetOp_correct: forall i st y xs, 0 <= i -> etable_values ​​aware_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)) = Some y ->state_rel(i+1)(update_stack(incr_iidst)(y::xs)).

La prima enunciazione del teorema

opcode_mops_correct LocalGet i

Quando espanso, significa che l'istruzione crea almeno una voce della tabella di memoria sulla riga i (il numero 1 è specificato nella specifica del codice operativo LocalGet di zkWasm).

Il secondo teorema è il teorema di correttezza completa per l'istruzione, che cita

mops_at_correct i

Come ipotesi, ciò significa che l'istruzione crea esattamente una voce nella tabella di memoria.

Un ingegnere verificatore può dimostrare questi due teoremi in modo indipendente e poi combinarli con una dimostrazione sulla tabella di esecuzione per dimostrare la correttezza dell'intero sistema. Vale la pena notare che tutte le dimostrazioni per le singole istruzioni possono essere eseguite a livello di vincoli di lettura/scrittura senza conoscere l'implementazione specifica della tabella di memoria. Pertanto, il progetto è diviso in tre parti che possono essere gestite indipendentemente.

Riassumere

La verifica dei circuiti di zkVM linea per linea non è fondamentalmente diversa dalla verifica delle applicazioni ZK in altri campi, perché entrambi richiedono un ragionamento simile sui vincoli aritmetici. Da una prospettiva di alto livello, la verifica di zkVM richiede molti degli stessi metodi di verifica formale utilizzati negli interpreti e nei compilatori dei linguaggi di programmazione. La differenza principale qui è lo stato della macchina virtuale con dimensioni dinamiche. Tuttavia, l'impatto di queste differenze può essere ridotto al minimo strutturando attentamente la struttura di verifica in modo che corrisponda al livello di astrazione utilizzato nell'implementazione, consentendo a ciascuna istruzione di essere implementata come un modulo indipendente basato sull'interfaccia get-set come per un normale interprete chimico verifica.