Vulnerabilidades ZK: Rocas afiladas escondidas en aguas profundas

Serie de publicaciones del blog Veridise: captura de vulnerabilidades en pruebas de conocimiento cero.

En esta entrada, hablaremos sobre las vulnerabilidades comunes en los programas Circom y la raiz de sus causas. Si no estás familiarizado con zkSNARKs, R1CS o el lenguaje de programación Circom, te recomendamos encarecidamente que, primero, leas nuestra entrada anterior, Una Introducción Suave a ZKPs y Circom, antes de continuar con esta.

Antecedentes

Como auditores de seguridad en Veridise, hemos examinado muchos circuitos ZK y hemos descubierto vulnerabilidades potencialmente desastrosas. (Por ejemplo, vea nuestro blog anterior: Circom-Pairing: Un error ZK de un millón de dólares detectado tempranamente.) Al reflexionar sobre nuestro tiempo auditando circuitos ZK, una de las cosas que notamos fue lo útil que era (especialmente al principio) tener el rastreador de vulnerabilidades comunes de 0xPARC. Cuando miramos el código en un marco nuevo o desconocido, especialmente en un nuevo paradigma como ZK, es fácil perderse, y tener un documento que detalle los tipos comunes de errores en el marco, te da una lista concreta de cosas para buscar. Sin embargo, rápidamente encontramos que muchos de los errores que estábamos descubriendo en estos circuitos, no estaban cubiertos por el rastreador. Por lo tanto, decidimos reexaminar los errores que encontramos, identificar los patrones comunes y compartirlos para ayudar a los implementadores de ZK a evitar (y ayudar a los auditores de ZK a encontrar 🙂) estas rocas afiladas, escondidas en aguas profundas.

Discrepancias de Cálculo y Restricción

Recordando nuestra entrada anterior, (Una Introducción Suave a ZKPs y Circom) muchos lenguajes ZKP, incluido Circom, compilan el programa en dos programas diferentes: (a) una función generadora de testigos (a la que de ahora en adelante nos referiremos como "cálculo"), y (b) un conjunto de restricciones. Intuitivamente, para que el circuito sea correcto, el cálculo P y las restricciones C deben tener la misma semántica con respecto a cada uno: Dado un input x, debería ser el caso que P(x) = y (donde y es la señal de salida) si y solo si C(x, y) evalúa a verdadero. Nos referimos a esta relación como la "invariante ZKP fundamental", y, si esta invariante no se cumple, es probable que el programa contenga un error. Nos referimos a tales problemas como "discrepancias de cálculo-restricción".

Pero, ¿cómo surgen estas discrepancias de cálculo-restricción en la práctica? Uno podría estar tentado a pensar que esto nunca debería suceder porque siempre se puede usar el operador <== en Circom. Recuerdando el blog anterior, este operador genera simultáneamente restricciones y realiza asignaciones para el generador de testigos. Entonces, si siempre usas <== en lugar de < — y ===, ¿por qué surgieron estos problemas?

Bueno, el problema es que muchos tipos de cálculo no se pueden expresar directamente como una restricción (particularmente debido al requisito de que las restricciones deben ser compilables hasta R1CS). Como resultado, hay muchas situaciones en las que uno no puede usar el operador <== y debe intentar expresar el cálculo y la restricción de manera diferente, mientras aún se asegura de que se cumpla nuestra invariante fundamental ZKP.

Para obtener más información sobre estas vulnerabilidades causadas por "discrepancias de cálculo-restricción", consideremos el circuito Edwards2Montgomery:

template Edwards2Montgomery() {
    signal input in[2];
    signal output out[2];
    out[0] <-- (1 + in[1]) / (1 - in[1]);
    out[1] <-- out[0] / in[0];
    out[0] * (1-in[1]) === (1 + in[1]);
    out[1] * in[0] === out[0];
}
component main = Edwards2Montgomery();

Este circuito está destinado a convertir un punto en una curva de Edwards a uno en la correspondiente curva de Montgomery. Consideremos primero las restricciones aquí: cuando out[0] = 0, out[1] = 0 y in[1] = -1, esas dos restricciones serán: 0 * 2 === 0 y 0 * in[0] === 0. ¡Nota que ambas ecuaciones se cumplirán (y se verificará la prueba) independientemente de lo que se proporcione para in[0]!

En resumen, la semántica de out[1] ← out[0] / in[0] es diferente de su restricción correspondiente out[1] * in[0] === out[0] cuando out[1] yout[0]son0. Claramente, este código viola la invariante fundamental de ZKP porque, en la parte de restricción, ¡in[1]` puede tener un valor arbitrario y aún así satisfacer la restricción! Para solucionar el problema, el desarrollador necesita restringir a los divisores para que no sean cero.

Dependencias de Entrada-Salida Faltantes

Un segundo patrón de error que encontramos bastante durante nuestras auditorías se debe a las dependencias faltantes entre las entradas y salidas del circuito. Como ejemplo, considera el siguiente error que encontramos durante una de nuestras auditorías:


template ChunkedMul(m, n, base){
signal input in1[m];
signal input in2[n];
signal carry[m+n];
signal output out[m+n];
component lt[m+n];
...
// carry[m+n-1] es restringido antes por in1 y in2.
out[m+n-1] <-- carry[m+n-1];
for(i = 0; i< m+n; i++) {
lt[i] = LessThanPower(base);
lt[i].in <== out[i];
out[i] * lt[i].out === out[i];
}
}
component main = ChunkedMul(3, 3, 51);


Este fragmento de código del proyecto ed25519-circom, corresponde a la plantilla del circuito ChunkedMul, que implementa un algoritmo de multiplicación por partes para realizar la multiplicación en dos valores. Estos valores son representados como arrays (de tamaño m y tamaño n) de tal manera que cada elemento en el array debe ser menor que 2 ** base. La señal de salida out se declara como un array de tamaño m + n y debe representar el resultado de la multiplicación. Sin embargo, en realidad hay una vulnerabilidad aquí: (Supongamos que estamos en la iteración cuando i = m + n - 1, mostrado en el fragmento de código anterior.)


// carry[m+n-1] está restringido previamente por in1 e in2.
out[m+n-1] <-- carry[m+n-1];
lt[m+n-1] = LessThanPower(base);
lt[m+n-1].in <== out[m+n-1];
out[m+n-1] * lt[m+n-1].out === out[m+n-1];


La intención del desarrollador, aquí, es asignar el valor de carry[m+n-1] a out[m+n-1] y restringir out[m+n-1] para que sea menor que 2 ** base.

Veamos las restricciones aquí:

Primero, la señal intermedia carry[m+n-1] está restringida por las señales de entrada in1 e in2.

Segundo, out[m+n-1] y lt[m+n-1] están restringidos entre sí.

¿Y luego...?

Es obvio que out[m+n-1] no está restringido por carry[m+n-1] ni por ninguna otra señal que esté restringida por cualquier señal de entrada.

La relación entre las diferentes señales en este circuito.

¡Por lo tanto, un usuario malintencionado puede convencer al verificador que la señal out[m+n-1] es un valor arbitrario menor que 2 ** base! Según la documentación del proyecto, esta plantilla implementa un operador crucial que se aplica directamente a las entradas del algoritmo en general. Por lo tanto, la vulnerabilidad descubierta por nuestra auditoría expone una superficie de ataque sustancial para todo el sistema. Para solucionar este problema, el desarrollador necesita agregar restricciones adicionales que afirmen que out[m+n-1] es igual a carry[m+n-1].

Uso Inseguro de Componentes

Muchos lenguajes ZKP admiten los llamados "componentes", que son circuitos auxiliares utilizados en la definición del circuito de nivel superior. Esencialmente, podemos pensar en los "componentes" como llamar a una biblioteca de terceros en un lenguaje de programación regular. Pero, al igual que las API tradicionales hacen ciertas suposiciones sobre cómo se deben usar (por ejemplo, la entrada no debe ser cero o, "leer" no debe llamarse antes de "abrir"), ¡los componentes a menudo también hacen ciertas suposiciones sobre su uso! Por ejemplo, un componente puede suponer que los usuarios restringirán sus señales de entrada o salida de ciertas maneras. Por lo tanto, si el desarrollador desconoce tales suposiciones (implícitas o explícitas) hechas por el componente, puede terminar usándolo de una manera peligrosa e introducir errores sutiles en su aplicación. De hecho, el error descrito en Circom-Pairing: Un error de ZK de un millón de dólares detectado temprano es exactamente eso: ¡el error es causado por la salida de un componente que no está restringida en el circuito de nivel superior!

ZKAP: La herramienta protege tu circuito ZKP

Mientras que algunos errores en los programas Circom son bastante obvios y pueden detectarse utilizando simples controles sintácticos, otros son mucho más sutiles y requieren una comprensión profunda de la semántica del programa. Para ayudarnos (y a otros) a encontrar errores en los programas Circom de manera más confiable, hemos creado una nueva herramienta de análisis estático llamada ZKAP, que puede utilizarse para detectar una gran familia de errores en los circuitos ZK. Si estás interesado en aprender más, por favor revisa el preprint de una de nuestras publicaciones recientes: https://eprint.iacr.org/2023/190.pdf

Acerca de Veridise

Veridise es una empresa de seguridad blockchain que proporciona auditorías y herramientas de análisis de software para todas las capas del ecosistema blockchain, incluyendo contratos inteligentes, aplicaciones web3, circuitos de conocimiento cero e implementaciones de blockchain. Cofundada por un equipo de investigadores de verificación formal y seguridad de software, Veridise proporciona herramientas de última generación para endurecer la seguridad de blockchain. Nuestros clientes pueden trabajar con nosotros de diversas maneras, incluyendo contratarnos para auditorías de seguridad, utilizar nuestras herramientas de análisis de seguridad automatizadas (para pruebas, análisis estático, verificación formal), o una combinación de estas.

Si estás interesado en obtener más información, por favor considera seguirnos en las redes sociales o visitar nuestro sitio web:

Website | Twitter | Facebook | LinkedIn | Github | Request Audit

Este artículo es una traducción realizada por @bananlabs. Puedes encontrar el artículo original aquí