Verificación formal de zk-SNARKs: método de prueba de memoria

Al llevar a cabo la Verificación formal de un sistema de zk-SNARKs, el manejo del subsistema de memoria es un desafío clave. A diferencia de las máquinas virtuales tradicionales, zkVM utiliza tablas de ejecución y tablas auxiliares para representar el estado de la memoria, lo que requiere métodos de verificación especiales.

El sistema de memoria de zkWasm está compuesto por una tabla de ejecución y una tabla de memoria. La tabla de ejecución registra el proceso de ejecución de instrucciones, mientras que la tabla de memoria guarda el historial de todos los accesos a la memoria. Para simplificar el desarrollo, zkWasm proporciona una capa de abstracción, que permite operar la memoria a través de las funciones alloc_memory_table_lookup_write_cell y alloc_memory_table_lookup_read_cell.

Durante el proceso de verificación, consideramos la tabla de memoria como una estructura de datos mutable, construyendo un mapeo de datos de dirección a través de la función memory_at. Esto permite demostrar que las restricciones generadas por la función alloc son equivalentes a las operaciones de set y get realizadas sobre el mapeo, simplificando así la verificación de instrucciones a una forma similar a un intérprete no ZK.

Para evitar que los atacantes manipulen la tabla de memoria, zkWasm utiliza un mecanismo de conteo para rastrear la cantidad de entradas válidas. La tabla de ejecución y la tabla de memoria mantienen contadores por separado, asegurando la coherencia entre ambas a través de restricciones. Esto requiere una mayor precisión durante la verificación, ya que se necesita demostrar que cada instrucción corresponde a la cantidad correcta de entradas en la tabla de memoria.

El proceso de verificación se realiza de arriba hacia abajo e incluye tres pasos:

1. Se debe estimar el número de entradas que debe crear la instrucción.
2. El número de entradas en la tabla de pruebas no debe ser mayor de lo esperado
3. Demostrar por inducción que cum_mops e instructions_mops son siempre consistentes en la tabla.

Este método de verificación detallado ayuda a identificar errores potenciales, como un problema clave en el mecanismo de conteo de saltos.

Para lograr la verificación modular, hemos dividido el sistema en tres partes independientes: verificación del circuito de instrucciones, verificación de la tabla de ejecución e implementación de la tabla de memoria. Esta estructura permite que varios ingenieros trabajen en paralelo, mejorando la eficiencia de la verificación.

En general, aunque la verificación de zkVM presenta diferencias al manejar estados dinámicos, aún se puede adoptar un enfoque modular similar al de la verificación de intérpretes tradicionales mediante la coincidencia de la capa de abstracción en la implementación. Este enfoque minimiza el impacto de las diferencias, permitiendo que cada instrucción sea verificada de forma independiente a través de la interfaz get-set.