En esta serie de artículos sobre verificación formal avanzada de pruebas de conocimiento cero, analizamos cómo verificar las instrucciones ZK y un análisis en profundidad de dos vulnerabilidades de ZK.
Como se muestra en el informe público (https://skynet.certik.com/projects/zkwasm) y el repositorio de código (https://github.com/CertiKProject/zkwasm-fv), cada instrucción zkWasm se verifica formalmente, encontramos y solucionó todas las vulnerabilidades, lo que nos permitió verificar completamente la seguridad técnica y la corrección de todo el circuito zkWasm.
Aunque hemos demostrado el proceso de verificación de una instrucción zkWasm e introducido los conceptos preliminares del proyecto relacionado, los lectores familiarizados con la verificación formal pueden estar más interesados en comprender la verificación de zkVM con otros sistemas ZK más pequeños u otros tipos de máquinas virtuales de código de bytes únicos. en. En este artículo, analizaremos en profundidad algunos de los puntos técnicos encontrados al validar el subsistema de memoria zkWasm. La memoria es la parte más exclusiva de zkVM y su manejo es fundamental para todas las demás verificaciones de zkVM.
Verificación formal: máquina virtual (VM) frente a máquina virtual ZK (zkVM)
Nuestro objetivo final es verificar la corrección de zkWasm, que es similar al teorema de corrección de los intérpretes de códigos de bytes ordinarios (VM, como el intérprete EVM utilizado por los nodos Ethereum). Es decir, cada paso de ejecución del intérprete corresponde a un paso legal basado en la semántica operativa del lenguaje. Como se muestra en la figura siguiente, si el estado actual de la estructura de datos del intérprete de código de bytes es SL, y este estado está marcado como estado SH en la especificación de alto nivel de la máquina Wasm, entonces cuando el intérprete pasa al estado SL', hay debe ser un SH' del estado legal de alto nivel correspondiente, y la especificación Wasm estipula que SH debe pasar a SH'.
Asimismo, zkVM tiene un teorema de corrección similar: cada nueva fila en la tabla de ejecución de zkWasm corresponde a un paso legal basado en la semántica operativa del lenguaje. Como se muestra en la figura siguiente, si el estado actual de una fila de estructura de datos en la tabla de ejecución es SR, y este estado se expresa como estado SH en la especificación de alto nivel de la máquina Wasm, entonces el estado SR' de la La siguiente fila en la tabla de ejecución debe corresponder a un estado de alto nivel SH', y la especificación Wasm estipula que SH debe pasar a SH'.
Se puede ver que la especificación de estados de alto nivel y pasos de Wasm es consistente ya sea en VM o zkVM, por lo que puede aprovechar la experiencia de verificación previa con intérpretes o compiladores de lenguajes de programación. Lo especial de la verificación zkVM es el tipo de estructura de datos que constituye el estado de bajo nivel del sistema.
Primero, como dijimos en un artículo anterior, el prover zk es esencialmente una operación de número entero módulo un primo grande, mientras que la especificación Wasm y el intérprete normal tratan con números enteros de 32 o 64 bits. La mayor parte de la implementación de zkVM implica esto, por lo que también es necesario realizar el procesamiento correspondiente durante la verificación. Sin embargo, este es un problema "local": cada línea de código se vuelve más compleja debido a las operaciones aritméticas que necesita manejar, pero la estructura general del código y la prueba no cambia.
Otra diferencia importante es cómo se manejan las estructuras de datos de tamaño dinámico. En un intérprete de código de bytes convencional, la memoria, la pila de datos y la pila de llamadas se implementan como estructuras de datos mutables. De manera similar, la especificación Wasm representa la memoria como un tipo de datos con métodos get/set. Por ejemplo, el intérprete EVM de Geth tiene un tipo de datos de Memoria, que se implementa como una matriz de bytes que representa la memoria física y se escribe y lee a través de los métodos Set32 y GetPtr. Para implementar una instrucción de almacenamiento de memoria, Geth llama a Set32 para modificar la memoria física.
func opMstore(pc *uint64, interpreter *EVMInterpreter, alcance *ScopeContext) ([]byte, error) { // valor emergente de la pila mStart, val := alcance.Stack.pop(), alcance.Stack.pop() alcance.Memoria.Set32(mStart.Uint64(), &val) devuelve nulo, nulo}
En la prueba de corrección del intérprete anterior, demostramos que su estado de alto nivel y su estado de bajo nivel coinciden después de asignar valores a la memoria concreta en el intérprete y a la memoria abstracta en la especificación. Esto es relativamente fácil.
Sin embargo, con zkVM la situación se vuelve más complicada.
Tabla de memoria de zkWasm y capa de abstracción de memoria
En zkVM, hay columnas para datos de tamaño fijo en la tabla de ejecución (similar a los registros en las CPU), pero no se pueden usar para manejar estructuras de datos de tamaño dinámico, que se implementan buscando tablas auxiliares. La tabla de ejecución de zkWasm tiene una columna EID, cuyos valores son 1, 2, 3..., y tiene dos tablas auxiliares, una tabla de memoria y una tabla de salto, que se utilizan para representar los datos de la memoria y la pila de llamadas respectivamente.
El siguiente es un ejemplo de cómo implementar un programa de retiro:
int saldo, monto;void main () {saldo = 100; monto = 10;saldo -= monto; // retirar}
El contenido y la estructura de la tabla de ejecución son bastante simples. Tiene 6 pasos de ejecución (EID1 a 6), cada paso tiene una línea listando su código de operación (opcode) y, si la instrucción es de lectura o escritura en memoria, su dirección y datos:
Cada fila de la tabla de memoria contiene dirección, datos, EID inicial y EID final. El EID inicial es el EID del paso de ejecución que escribe los datos en esta dirección y el EID final es el EID del siguiente paso de ejecución que escribirá los datos en esta dirección. (También contiene un recuento, que analizaremos en detalle más adelante). Para el circuito de instrucciones de lectura de memoria Wasm, utiliza una restricción de búsqueda para garantizar que haya una entrada adecuada en la tabla, de modo que el EID de la instrucción de lectura esté en el van de principio a fin en el interior. (De manera similar, cada fila de la tabla de salto corresponde a un marco de la pila de llamadas y cada fila está etiquetada con el EID del paso de instrucción de llamada que la creó).
Este sistema de memoria difiere mucho de un intérprete de VM normal: en lugar de una memoria mutable que se actualiza gradualmente, la tabla de memoria contiene un historial de todos los accesos a la memoria a lo largo del seguimiento de ejecución. Para simplificar el trabajo del programador, zkWasm proporciona una capa de abstracción, implementada a través de dos funciones de entrada convenientes. Ellos son:
alloc_memory_table_lookup_write_cell
y
Alloc_memory_table_lookup_read_cell
Sus parámetros son los siguientes:
Por ejemplo, el código que implementa las instrucciones de almacenamiento de memoria en zkWasm contiene una llamada a la función de asignación de escritura:
let Memory_table_lookup_heap_write1 = asignador .alloc_memory_table_lookup_write_cell_with_value( "almacenar escritura res1", constraint_builder, eid, mover |____| constante_from!(LocationType::Heap as u64), mover |meta| load_block_index.expr(meta), // mover dirección |____| constante_from!(0), // es un movimiento de 32 bits |____| constante_from!(1), // (siempre) habilitado );letstore_value_in_heap1=memory_table_lookup_heap_write1.value_cell;
La función alloc es responsable de manejar las restricciones de búsqueda entre tablas y las restricciones aritméticas que asocian el eid actual con las entradas de la tabla de memoria. A partir de esto, los programadores pueden tratar estas tablas como memoria ordinaria, y el valor de store_value_in_heap1 se ha asignado a la dirección load_block_index después de ejecutar el código.
De manera similar, las instrucciones de lectura de memoria se implementan utilizando la función read_alloc. En la secuencia de ejecución de ejemplo anterior, hay una restricción de lectura para cada instrucción de carga y una restricción de escritura para cada instrucción de almacenamiento, y cada restricción se satisface mediante una entrada en la tabla de memoria.
La estructura de la verificación formal debe corresponder a las abstracciones utilizadas en el software que se verifica, de modo que la prueba pueda seguir la misma lógica que el código. Para zkWasm, esto significa que necesitamos verificar el circuito de la tabla de memoria y las funciones de "celda de lectura/escritura de asignación" como un módulo, que interactúa como una memoria variable. Dada dicha interfaz, la verificación de cada circuito de instrucción se puede realizar de manera similar a un intérprete normal, mientras que la complejidad adicional de ZK se encapsula en el módulo del subsistema de memoria.
En la verificación, implementamos la idea de que "la tabla de memoria en realidad puede considerarse como una estructura de datos mutable". Es decir, escriba la función tipo memoria_at, que escanea completamente la tabla de memoria y construye la asignación de datos de dirección correspondiente. (El rango de valores del tipo de variable aquí es de tres tipos diferentes de datos de memoria Wasm: montón, pila de datos y variables globales). Luego, demostramos que las restricciones de memoria generadas por la función alloc son equivalentes a usar las funciones set y get para establezca las direcciones correspondientes. Los cambios de datos realizados mediante el mapeo de datos. Podemos probar:
Para cada eid, si se cumplen las siguientes restricciones
memoria_table_lookup_read_celleidtypeoffsetvalue
pero
get(memory_ateidtype)offset=Algún valor
Y, si se cumplen las siguientes restricciones
valor de compensación del tipo eid de memoria_table_lookup_write_cell
pero
tipo de memoria_at (eid+1) = establecer valor de compensación (tipo de eid de memoria_at)
Después de esto, la verificación de cada instrucción se puede basar en operaciones de obtención y configuración en el mapa de datos de direcciones, similar a los intérpretes de códigos de bytes que no son ZK.
Mecanismo de conteo de escritura en memoria de zkWasm
Sin embargo, la descripción simplificada anterior no revela todo el contenido de la tabla de memoria y de la tabla de salto. En el marco de zkVM, estas tablas pueden ser manipuladas por atacantes. Los atacantes pueden manipular fácilmente las instrucciones de carga de memoria y devolver valores arbitrarios insertando una fila de datos.
Tomando el programa de retiro como ejemplo, el atacante tiene la oportunidad de inyectar datos falsos en el saldo de la cuenta falsificando una operación de escritura en memoria de $110 antes de la operación de retiro. Este proceso se puede lograr agregando una fila de datos a la tabla de memoria y modificando los valores de las celdas existentes en la tabla de memoria y la tabla de ejecución. Esto resultará en retiros "gratuitos" ya que el saldo de la cuenta permanecerá en $100 después de la operación.
Para garantizar que la tabla de memoria (y la tabla de salto) solo contenga entradas válidas generadas por las instrucciones de escritura en memoria (y llamadas y retornos) realmente ejecutadas, zkWasm emplea un mecanismo de conteo especial para monitorear el número de entradas. Específicamente, la tabla de memoria tiene una columna dedicada que realiza un seguimiento del número total de entradas escritas en la memoria. Al mismo tiempo, la tabla de ejecución también contiene un contador para contar el número de operaciones de escritura en memoria esperadas para cada instrucción. Asegúrese de que los dos recuentos sean consistentes estableciendo una restricción de igualdad. La lógica de este método es muy intuitiva: cada vez que se realiza una operación de escritura en la memoria, se contará una vez y debería haber un registro correspondiente en la tabla de memoria. Por lo tanto, el atacante no puede insertar entradas adicionales en la tabla de memoria.
La afirmación lógica anterior es un poco vaga y, en el proceso de prueba mecanizada, es necesario hacerla más precisa. Primero, necesitamos revisar la declaración del lema de escritura en memoria mencionado anteriormente. Definimos la función mops_at eid type para contar las entradas de la tabla de memoria con un eid y tipo determinados (la mayoría de las instrucciones crearán 0 o 1 entradas en un eid). El enunciado completo del teorema tiene un requisito previo adicional que establece que no hay entradas falsas en la tabla de memoria:
Si se cumplen las siguientes restricciones
(memory_table_lookup_write_celleidtypeoffsetvalue)
Y se establecen las siguientes nuevas restricciones
(mops_ateidtipo)=1
pero
(memory_at(eid+1)tipo)=set(memory_ateidtype)valor de compensación
Esto requiere que nuestra verificación sea más precisa que el caso anterior. Simplemente derivar de la restricción de igualdad de que el número total de entradas de la tabla de memoria sea igual al número total de escrituras de memoria en la ejecución no es suficiente para completar la verificación. Para demostrar la exactitud de una instrucción, necesitamos saber que cada instrucción corresponde al número correcto de entradas de la tabla de memoria. Por ejemplo, debemos descartar si un atacante podría omitir una entrada de la tabla de memoria para una instrucción en la secuencia de ejecución y crear una nueva entrada maliciosa en la tabla de memoria para otra instrucción no relacionada.
Para demostrar esto, utilizamos un enfoque de arriba hacia abajo para limitar el número de entradas de la tabla de memoria correspondientes a una instrucción determinada, que implica tres pasos. Primero, estimamos la cantidad de entradas que se deben crear para las instrucciones en la secuencia de ejecución según el tipo de instrucción. Llamamos al número esperado de escrituras desde el i-ésimo paso hasta el final de la ejecución instrucciones_mops i, y al número correspondiente de entradas en la tabla de memoria desde la i-ésima instrucción hasta el final de la ejecución cum_mops (eid i). Al analizar las restricciones de búsqueda de cada instrucción, podemos demostrar que no crea menos entradas de las esperadas y, por lo tanto, cada segmento rastreado [i ... numRows] no crea menos entradas de las esperadas:
Lema 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.
En segundo lugar, si puede demostrar que la tabla no tiene más entradas de las esperadas, entonces tiene exactamente el número correcto de entradas, lo cual es obvio.
Lema 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) ≤ instrucciones_mops' i n ->MTable.cum_mops(etable_valueseid_celli)(max_eid+ 1)=instrucciones_mops'in.
Ahora continúe con el paso tres. Nuestro teorema de corrección establece que para cualquier n, cum_mops e instrucciones_mops siempre son consistentes desde la fila n hasta el final de la tabla:
Lema cum_mops_equal: para todos 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 verificación se logra resumiendo n. La primera fila de la tabla es la restricción de igualdad de zkWasm, lo que indica que el número total de entradas en la tabla de memoria es correcto, es decir, cum_mops 0 = instrucciones_mops 0. Para las siguientes líneas, la hipótesis inductiva nos dice:
cum_mopsn=instrucciones_mopsn
y esperamos demostrar
cum_mops (n+1) = instrucciones_mops (n+1)
presta atención aquí
cum_mops n = trapeador_at n + cum_mops (n+1)
y
instrucciones_mops n = instrucciones_mops n + instrucciones_mops (n+1)
Por tanto, podemos conseguir
mops_at n + cum_mops (n+1) = instrucción_mops n + instrucciones_mops (n+1)
Anteriormente, hemos demostrado que cada instrucción creará no menos del número esperado de entradas, p.e.
mops_at n ≥ instrucción_mops n.
Así se puede concluir
cum_mops (n+1) ≤ instrucciones_mops (n+1)
Aquí debemos aplicar el segundo lema anterior.
Describir el proceso de prueba con tanto detalle es típico de la verificación formal y es la razón por la que verificar un fragmento de código específico suele llevar más tiempo que escribirlo. Pero ¿vale la pena? En este caso valió la pena porque encontramos un error crítico en el mecanismo de conteo de la tabla de salto durante la prueba. Este error se describió en detalle en un artículo anterior; en resumen, las versiones anteriores del código tenían en cuenta tanto las instrucciones de llamada como las de devolución, y un atacante podría crear un salto falso agregando instrucciones de devolución adicionales a la secuencia de ejecución para hacer espacio en las entradas de la tabla. . Aunque un mecanismo de conteo incorrecto puede satisfacer la intuición de que cada instrucción de llamada y devolución se cuenta, surgen problemas cuando intentamos refinar esta intuición en un enunciado de teorema más preciso.
Haga que el proceso de prueba sea modular
De la discusión anterior, podemos ver que existe una dependencia circular entre la prueba sobre el circuito de cada instrucción y la prueba sobre la columna de conteo de la tabla de ejecución. Para probar la exactitud del circuito de instrucciones, necesitamos razonar sobre las escrituras en memoria en él; es decir, necesitamos saber el número de entradas de la tabla de memoria en un EID específico y debemos demostrar que la operación de escritura en memoria cuenta; la tabla de ejecución es correcta y esto también es necesario demostrar que cada instrucción realiza al menos un número mínimo de escrituras en memoria.
Además, hay otro factor que debe considerarse: el proyecto zkWasm es bastante grande, por lo que el trabajo de verificación debe modularizarse para que varios ingenieros de verificación puedan dividir el trabajo. Por lo tanto, se debe prestar especial atención a su complejidad al deconstruir la prueba del mecanismo de conteo. Por ejemplo, para la instrucción LocalGet, existen dos teoremas:
Teorema opcode_mops_correct_local_get: para todos 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 enable_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)).
El primer enunciado del teorema.
opcode_mops_correct LocalGet i
Cuando se expande, significa que la instrucción crea al menos una entrada de la tabla de memoria en la línea i (el número 1 se especifica en la especificación del código de operación LocalGet de zkWasm).
El segundo teorema es el teorema de corrección total de la instrucción, que cita
mops_at_correct yo
Como hipótesis, esto significa que la instrucción crea exactamente una entrada en la tabla de memoria.
Un ingeniero de verificación puede probar estos dos teoremas de forma independiente y luego combinarlos con una demostración sobre la tabla de ejecución para demostrar la exactitud de todo el sistema. Vale la pena señalar que todas las pruebas de instrucciones individuales se pueden realizar en el nivel de restricciones de lectura/escritura sin conocer la implementación específica de la tabla de memoria. Por tanto, el proyecto se divide en tres partes que pueden abordarse de forma independiente.
Resumir
Verificar los circuitos de zkVM línea por línea no es fundamentalmente diferente de verificar aplicaciones ZK en otros campos, porque ambos requieren razonamientos similares sobre restricciones aritméticas. Desde una perspectiva de alto nivel, la verificación de zkVM requiere muchos de los mismos métodos de verificación formales utilizados en los intérpretes y compiladores de lenguajes de programación. La principal diferencia aquí es el estado de la máquina virtual de tamaño dinámico. Sin embargo, el impacto de estas diferencias se puede minimizar estructurando cuidadosamente la estructura de verificación para que coincida con la capa de abstracción utilizada en la implementación, permitiendo que cada instrucción se implemente como un módulo independiente basado en la interfaz get-set como para un intérprete químico normal. verificación.
