Resumen Técnico: ZKFUZZ: Fundamento y Marco para la Eficaz Fuzzing de Circuitos de Conocimiento Cero

1. Declaración del Problema

Los circuitos de conocimiento cero (ZK) son fundamentales para los cálculos que preservan la privacidad, permitiendo pruebas concisas y verificación eficiente en aplicaciones que van desde criptomonedas anónimas hasta aprendizaje automático verificable. Sin embargo, desarrollar circuitos ZK correctos es notoriamente difícil debido a la desalineación entre la lógica de computación de propósito general y las restricciones polinómicas de campos finitos.

Existen dos clases principales de vulnerabilidades:

• Circuitos subrestringidos: Las restricciones son demasiado laxas, permitiendo que probadores maliciosos generen pruebas válidas para testigos inválidos (violando la solidez).
• Circuitos sobre-restringidos: Las restricciones son demasiado estrictas, causando que el sistema rechace testigos válidos de probadores honestos (violando la completitud).

Los métodos de detección existentes enfrentan limitaciones significativas:

• Análisis Estático: Herramientas como Circomspect y ZKAP a menudo sufren altas tasas de falsos positivos y no logran capturar problemas semánticos profundos, particularmente aquellos que involucran cálculos intermedios o terminación anormal del programa.
• Métodos Formales: Las herramientas que dependen de solucionadores SMT (por ejemplo, Picus, ConsCS) luchan por escalar a tamaños de circuitos del mundo real y a menudo se basan en definiciones incompletas de vulnerabilidades, centrándose únicamente en la no determinismo en las restricciones mientras ignoran casos donde la computación se aborta o donde los valores intermedios no coinciden.
• Brechas en la Definición: Las definiciones formales anteriores de errores ZK son incompletas. A menudo ignoran la "terminación anormal" (donde una computación falla pero las restricciones aún se satisfacen) y no tienen en cuenta el conjunto completo de trazas de ejecución, incluidos los valores intermedios.

2. Metodología

2.1 Fundamento Teórico: Prueba de Consistencia Traza-Restricción (TCCT)

Los autores introducen TCCT, un marco formal independiente del lenguaje que define las vulnerabilidades ZK como discrepancias entre dos conjuntos:

1. Conjunto de Trazas $T(P)$: El conjunto de todas las trazas de ejecución posibles (entrada, valores intermedios, salida) producidas por el programa de computación de testigo $P$.
2. Conjunto de Satisfacción de Restricciones $S(C)$: El conjunto de todas las tuplas (entrada, valores intermedios, salida) que satisfacen las restricciones del circuito $C$.

TCCT define un circuito como bien restringido si y solo si:

• Sin Subrestricción: La proyección de $S(C)$ sobre pares entrada-salida es un subconjunto de la proyección de $T(P)$. Esto asegura que no se acepten trazas inválidas.
• Sin Sobre-restricción: $T(P)$ es un subconjunto de $S(C)$. Esto asegura que todas las trazas válidas (incluidos valores intermedios específicos) sean aceptadas.

Esta formulación captura vulnerabilidades causadas por abortos de computación (donde $P$ falla pero $C$ acepta la entrada) y desajustes en valores intermedios, los cuales las definiciones anteriores pasaron por alto. Los autores demuestran que decidir la subrestricción o sobre-restricción es NP-completo, y el TCCT completo es co-NP-completo.

2.2 Diseño del Sistema: ZKFUZZ

ZKFUZZ es un marco de análisis dinámico que detecta violaciones de TCCT utilizando un enfoque de mutación conjunta de programas y generación de entradas. A diferencia del fuzzing tradicional que solo muta entradas, ZKFUZZ muta tanto la lógica del programa como las entradas.

Flujo de Trabajo Principal:

1. Mutación: El sistema genera mutantes ($P'$) del programa de computación original ($P$). Las mutaciones incluyen eliminar aserciones, transformar asignaciones (por ejemplo, reemplazar operadores o valores) y modificar asignaciones débiles.
2. Ejecución: Tanto el programa original ($P$) como el mutante ($P'$) se ejecutan en entradas muestreadas ($x$).
3. Verificación:
   • Detección de Sobre-restricción: Si $P(x)$ produce una traza válida que falla $C$, el circuito está sobre-restringido.
   • Detección de Subrestricción: Si $P'(x)$ produce una traza con una salida diferente ($y' \neq y$) que aún satisface $C$, el circuito está subrestringido (ya que la lógica mutante es semánticamente diferente, la salida no debería ser aceptada).
4. Búsqueda Guiada: Para navegar el vasto espacio de búsqueda de grandes campos primos y posibilidades infinitas de mutación, ZKFUZZ emplea un algoritmo genético:
   • Función de Aptitud: Una nueva función de aptitud de suma mínima calcula la suma de errores de restricción a través de todas las restricciones para una traza dada. El mutante se puntúa por la suma mínima de errores a través de las entradas muestreadas. Esto difiere de los métodos anteriores que solo usaban máximos y es más adecuado para la mutación conjunta.
   • Selectores de Objetivo: El sistema utiliza análisis estático para guiar la mutación y la generación de entradas hacia patrones de alto riesgo, como:
     • División por Cero: Generar entradas donde el numerador y el denominador son ambos cero.
     • Verificación de Hash: Forzar entradas a satisfacer restricciones de igualdad de hash.
     • Distribución Sesgada: Sesgar la generación de entradas hacia casos extremos (0, 1 y valores cercanos al módulo del campo $q$).
     • Lista Blanca: Saltar plantillas conocidas como seguras (por ejemplo, IsZero, Num2Bits) para centrarse en código propenso a errores.

3. Contribuciones Clave

1. Marco TCCT: Un modelo formal unificado e independiente del lenguaje que subsume definiciones anteriores y captura el espacio completo de errores ZK, incluidos aquellos que surgen de terminación anormal y desajustes de valores intermedios.
2. Sistema ZKFUZZ: Un marco de fuzzing novedoso que muta conjuntamente programas e entradas para detectar violaciones de TCCT, utilizando una función de aptitud de suma mínima y heurísticas de búsqueda guiada.
3. Validación Empírica: Evaluación en 452 circuitos Circom del mundo real, demostrando un rendimiento superior sobre herramientas de última generación.
4. Prototipo Noir: Una implementación preliminar para Noir, un DSL ZK diferente, que demuestra el potencial del marco para la independencia del lenguaje.

4. Resultados

Los autores evaluaron ZKFUZZ en 452 circuitos Circom del mundo real, comparándolo con cuatro herramientas de última generación: Circomspect, ZKAP, Picus y ConsCS.

• Detección de Errores: ZKFUZZ identificó 85 errores únicos, incluidos 59 vulnerabilidades cero-día previamente desconocidas. De estos, 39 fueron confirmados por desarrolladores y 14 fueron corregidos.
• Comparación: ZKFUZZ encontró entre un 30% y un 300% más de errores que las herramientas existentes en varios tamaños de circuitos.
• Precisión: ZKFUZZ logró 100% de precisión (cero falsos positivos), mientras que los analizadores estáticos como Circomspect y ZKAP tenían altas tasas de falsos positivos (precisión que oscilaba entre 0.06 y 0.75).
• Velocidad: ZKFUZZ++ (con selectores de objetivo) identificó más del 90% de los errores en 100 segundos, superando significativamente a los métodos formales y analizadores estáticos.
• Impacto: Los errores descubiertos incluyeron vulnerabilidades críticas de subrestricción en proyectos como zk-regex y passport-zk-circuits, que podrían permitir a los atacantes forjar pruebas o extraer fondos.

5. Significado y Afirmaciones

El artículo afirma que ZKFUZZ representa un avance significativo en la seguridad de circuitos ZK al abordar la incompletitud fundamental de las definiciones anteriores de vulnerabilidades. Al formalizar los errores como inconsistencias traza-restricción (TCCT), los autores exponen una gran clase de vulnerabilidades (casi el 50% de los errores del mundo real en su evaluación) que anteriormente eran indetectables por herramientas centradas únicamente en el no determinismo de restricciones.

La capacidad del sistema para detectar errores sin falsos positivos lo convierte en una herramienta práctica para desarrolladores, quienes a menudo ignoran las alertas de analizadores estáticos con altos falsos positivos. Además, la detección exitosa de errores en circuitos Noir sugiere que el marco TCCT y la arquitectura ZKFUZZ no están limitados a Circom, sino que pueden generalizarse a otros lenguajes ZK que se compilan a formatos de restricción estandarizados.

Los autores enfatizan que su trabajo se centra en vulnerabilidades que surgen de la desalineación entre computación y restricciones (solidez y completitud), excluyendo explícitamente errores en los sistemas de prueba subyacentes, errores de lógica pura (como entradas no utilizadas) o fugas de conocimiento cero a nivel de protocolo.