💻 computer science

Formally Verifying Noir Zero Knowledge Programs with NAVe

Este artículo presenta NAVe, un verificador formal de código abierto que utiliza SMT-LIB y el solver cvc5 para verificar formalmente la corrección y las restricciones adecuadas de los programas de conocimiento cero de Noir mediante la traducción de su representación intermedia ACIR en ecuaciones de polinomios de campos finitos.

Autores originales: Pedro Antonino, Namrata Jain

Publicado 2026-01-15

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Pedro Antonino, Namrata Jain

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que estás construyendo una bóveda de alta seguridad. Quieres demostrarle a un gerente de un banco que conoces la combinación de la bóveda sin decirle realmente cuál es la combinación. Esto es la magia de las pruebas de conocimiento cero (Zero-Knowledge o ZK).

Sin embargo, construir estas bóvedas es complicado. Los "planos" para estas pruebas son rompecabezas matemáticos complejos llamados circuitos aritméticos. Si una sola línea de los planos es incorrecta, la bóveda podría ser insegura o la prueba podría fallar.

Este artículo presenta una nueva herramienta llamada NAVe (Noir Acir Verifier) diseñada para revisar estos planos en busca de errores antes de que lleguen a utilizarse. Así es como funciona, explicado de forma sencilla:

1. El problema: La "Receta Secreta" frente al "Libro de Cocina"

Los autores se centran en un lenguaje de programación llamado Noir. Piensa en Noir como un libro de cocina de alto nivel que facilita la escritura de recetas para estas bóvedas.

El Cocinero (Desarrollador): Escribe una receta en un Noir fácil de leer.
El Traductor (Compilador): Convierte esa receta en un manual de instrucciones de bajo nivel llamado ACIR. Este manual es una lista de ecuaciones matemáticas que la computadora debe resolver para demostrar que la bóveda es segura.
El Peligro: A veces, el traductor comete un error, o el cocinero olvida incluir un paso crucial. En el mundo de ZK, esto se llama estar "sub-restringido" (under-constrained). Es como escribir una receta que dice "añadir sal" pero olvida decir cuánto. El resultado puede ser comestible, pero no es el plato que pretendías.

2. La solución: El "Detective Matemático" (NAVe)

Los autores crearon NAVe, un verificador formal. Piensa en NAVe como un detective matemático superinteligente que lee el manual de instrucciones de bajo nivel (ACIR) y comprueba si las matemáticas realmente coinciden con lo que el cocinero pretendía.

NAVe utiliza un potente motor de lógica (llamado solucionador SMT) para hacer preguntas como:

"¿Si introduzco un número secreto, la matemática siempre dará como resultado la prueba pública correcta?"
"¿Hay alguna forma de engañar al sistema con un número falso?"

Si la matemática está rota, NAVe no se limita a decir "Error". Actúa como un detective que encuentra una pista: le muestra al desarrollador exactamente qué número podría haber usado para romper el sistema. Esto les ayuda a corregir el plano de inmediato.

3. Dos formas de resolver el rompecabezas

El artículo describe dos formas diferentes en las que NAVe traduce los rompecabezas matemáticos para resolverlos:

La vía de los Enteros: Trata los números como números enteros regulares (1, 2, 3...) y comprueba las matemáticas utilizando reglas aritméticas estándar.
La vía del Campo Finito: Trata los números como si estuvieran en un reloj circular (donde, después de cierto número, vuelves a empezar desde cero). Así es como funcionan las pruebas ZK reales.

Los autores descubrieron que ninguno de los dos métodos es perfecto para todas las situaciones. A veces, el detective de "Enteros" es más rápido; otras veces, el detective de "Campo Finito" es mejor. Sugieren utilizar ambos detectives al mismo tiempo para obtener los mejores resultados.

4. La trampa de lo "No Restringido"

Una característica única de Noir es el "código no restringido" (unconstrained code). Imagina una parte de la receta donde se le permite al chef adivinar los ingredientes sin ser comprobado. Esto es útil para la velocidad, pero peligroso si el chef adivina mal.

El Riesco: Un desarrollador podría escribir código que parece que verifica los ingredientes, pero debido a que está en la sección "no restringida", la computadora no fuerza realmente la comprobación.
El Trabajo de NAVe: NAVe busca específicamente estas "comprobaciones fantasma". Verifica que, incluso si un desarrollador utiliza la sección de "adivinanza", haya añadido una regla estric de separación (un assert) para asegurarse de que la adivinación fue realmente correcta.

5. Lo que encontraron

Los autores probaron NAVe en una variedad de programas Noir existentes:

Funciona: NAVe detectó con éxito errores en programas donde la matemática no coincidía con la intención.
El Cuello de Botella: Descubrieron que comprobar las "restricciones de rango" (asegurarse de que un número quepa dentro de un número específico de bits, como comprobar si un número está entre 0 y 255) es muy difícil para el detective matemático. A veces tarda mucho tiempo o se queda bloqueado.
El Futuro: Planean construir mejores "atajos" (abstracciones) para ayudar al detective a resolver estos complicados rompecabezas de rango de forma más rápida.

Resumen

En resumen, NAVe es una red de seguridad para los desarrolladores que construyen aplicaciones que preservan la privacidad. Traduce su código a un lenguaje matemático estricto y utiliza un potente solucionador para asegurar que el código hace exactamente lo que afirma hacer, detectando errores sutiles que de otro modo podrían conducir a fallos de seguridad. Es como tener un inspector riguroso que comprueba la integridad estructural de un puente antes de que se permita a nadie cruzarlo.

Resumen Técnico: Verificación Formal de Programas de Conocimiento Cero de Noir con NAVe

Planteamiento del Problema
Los sistemas de prueba de Conocimiento Cero (ZK) dependen de circuitos aritméticos —conjuntos de ecuaciones polinómicas sobre campos finitos— para verificar que una entrada privada $W$ satisface una relación $R(X, W)$ sin revelar $W$ . Los lenguajes de dominio específico (DSL) de alto nivel como Noir simplifican la creación de estos circuitos compilando el código en una representación intermedia llamada ACIR (Representación de Circuito Intermedio Abstracto). Sin embargo, esta abstracción introduce vulnerabilidades sutiles. Específicamente, Noir soporta "código no restringido" (mediante funciones unconstrained y bloques unsafe) diseñado para mejorar la eficiencia de la prueba al delegar computaciones complejas al probador. Si los desarrolladores no añaden manualmente las correspondientes restricciones (por ejemplo, mediante sentencias assert) para los resultados del código no restringido, el circuito aritmético generado puede no capturar con precisión la relación pretendida. Este error de "sub-restricción" (under-constrained) puede derivar en vulnerabilidades de seguridad graves, como permitir que un probador genere pruebas válidas para enunciados falsos. Las herramientas de verificación formal existentes se dirigen mayoritariamente a DSL de circuitos de nivel inferior (como Circom) o requieren la demostración de teoremas interactiva, careciendo de una verificación automatizada y escalable para programas de Noir de alto nivel y sus características específicas como la manipulación de memoria y las funciones de caja negra.

Metodología
Los autores proponen NAVe (Noir Acir Verifier), un marco de verificación formal de código abierto que opera sobre la representación intermedia ACIR en lugar del código fuente de alto nivel de Noir. Esta elección garantiza la estabilidad frente a la evolución del lenguaje y permite que la herramienta soporte potencialmente otros lenguajes que tengan como objetivo ACIR.

Formalización mediante SMT-LIB: El núcleo de NAVe es una formalización de un subconjunto de opcodes de ACIR en fórmulas de Satisfacibilidad de Teorías (SMT):
- Codificación de Campo Finito: Utiliza una teoría no estándar de campos finitos de orden primo implementada en el solver cvc5. Este enfoque utiliza operadores específicos como ff.add, ff.mul y ff.bitsum para modelar directamente la aritmética de campos.
- Codificación de Aritmética de Enteros: Aprovecha la teoría estándar de enteros en SMT-LIB. Se basa en el isomorfismo entre campos finitos de orden primo $p$ y enteros módulo $p$ , codificando las operaciones de campo como aritmética modular de enteros (por ejemplo, (mod (+ ...) p)).
Semántica de los Opcodes: La formalización cubre opcodes clave de ACIR:
- AssertZero: Codificado como una restricción de ecuación polinómica igual a cero.
- BlackBoxFuncCall: Formalizado específicamente para el opcode de comprobación de rango (Range). En la codificación de campo finito, esto se modela mediante una descomposición binaria (bitsum) y restricciones que aseguran que los bits sean 0 o 1. En la codificación de enteros, se modela utilizando restricciones de orden de enteros estándar ( $x < 2^n$ ).
- MemoryOp y MemoryInit: Formalizados para rastrear mutaciones de arreglos utilizando un mapa de índices a valores de testigo (witness), manejando tanto las operaciones de lectura como de escritura de forma secuencial.
- BrilligCall: Representando el código no restringido, estos se traducen como la restricción siempre satisfecha true (o se ignoran), ya que el objetivo del verificador es comprobar las restricciones fuera de los bloques no restringidos.
Flujo de Trabajo de Verificación:
- La herramienta se integra con Nargo, el gestor de paquetes de Noir, como un comando formal-verify.
- Los desarrolladores anotan los programas de Noir con sentencias verify_assert(b: bool). A diferencia de las sentencias assert estándar que generan restricciones de circuito, verify_assert crea una obligación de prueba.
- NAVe compila el programa de Noir a ACIR, traduce los opcodes de ACIR en fórmulas SMT y construye una fórmula de verificación $F = \text{ACIR}_{\text{constraints}} \land \neg \text{verify\_assert}_{\text{condition}}$ .
- El solver cvc5 comprueba la satisfacibilidad de $F$ . Si $F$ es insatisfacible, la condición de verificación se cumple (el programa está correctamente restringido). Si $F$ es satisfacible, el solver devuelve un modelo (contraejemplo) que muestra una asignación de testigo que viola la condición, lo cual ayuda en la depuración.

Contribuciones Clave

Formalización de ACIR: La primera formalización de un subconjunto del lenguaje ACIR utilizando SMT-LIB, cubriendo características complejas como operaciones de memoria, comprobaciones de rango y la distinción entre código restringido y no restringido.
Estrategia de Codificación Dual: La propuesta de dos codificaciones complementarias (teoría de campo finito y aritmética de enteros) para aprovechar las diferentes capacidades de los solvers.
Herramienta NAVe: Un verificador formal automatizado de código abierto integrado en el ecosistema de Noir (Nargo), diseñado para ser accesible a los desarrolladores sin requerir la demostración interactiva de teoremas.
Evaluación Empírica: Una evaluación exhaustiva de NAVe en un conjunto de programas de prueba de Noir, analizando el rendimiento a través de diferentes tipos de restricciones y configuraciones de solver.

Resultados
Los autores evaluaron NAVe en 4 conjuntos distintos de programas de Noir (condiciones verificadas, condiciones falsificadas, con y sin comprobaciones de rango) utilizando el solver cvc5.

Rendimiento del Solver: Ningún backend (codificación de enteros, campo finito --ff=gb, o campo finito --ff=split) superó consistentemente a los demás. Los resultados indican que las codificaciones son complementarias; algunos programas son resueltos más rápido por una codificación, mientras que otros agotan el tiempo de ejecución en esa misma codificación pero tienen éxito en otra.
Impacto de las Comprobaciones de Rango: Los programas que contienen comprobaciones de Range (opcodes BlackBoxFuncCall) aumentaron significamente el tiempo de verificación. La configuración --ff=split, que aproxima la teoría de campo finito, mostró un rendimiento superior en programas con comprobaciones de rango grandes en comparación con la configuración por defecto --ff=gb, aunque todavía ocurrieron tiempos de espera agotados en casos complejos.
Generación de Contraejemplos: La herramienta generó con éxito contraejemplos para condiciones falsificadas, demostrando su utilidad para identificar lógica sub-restringida.

Significancia y Reivindicaciones
El artículo afirma que NAVe aborda una brecha crítica en el ecosistema ZK al proporcionar un método automatizado y escalable para verificar programas de ZK de alto nivel ante errores de sub-restricción, una clase de errores que ha provocado vulnerabilidades en el mundo real. Al dirigirse a ACIR, la herramienta se mantiene robusta frente a cambios en la sintaxis de alto nivel de Noir y es potencialmente aplicable a otros lenguajes que tengan como objetivo la misma representación intermedia.

Los autores enmarcan modestamente su trabajo como un paso hacia capacidades de verificación más amplias. Reconocen que su formalización actual cubre solo un subconjunto de ACIR (excluyendo los opcodes Call recursivos y la mayoría de los BlackBoxFuncCalls excepto Range). Identifican el alto costo de verificar las comprobaciones de rango como una limitación primaria, sugiriendo que el trabajo futuro debe centrarse en desarrollar abstracciones o aproximaciones para manejar estas restricciones complejas de manera eficiente. El artículo posiciona a NAVe no como una solución completa para todas las necesidades de verificación de ZK, sino como una herramienta práctica e integrada que demuestra la viabilidad de la verificación formal automatizada para Noir y traza un camino para mejorar el manejo de los solvers de las restricciones complejas a nivel de bits.