En un artículo anterior, discutimos la verificación formal avanzada de los sistemas de prueba de conocimiento cero (ZKP): cómo verificar una instrucción ZK. Al verificar formalmente cada instrucción de zkWasm, podemos garantizar completamente la seguridad técnica y la corrección de todo el circuito de zkWasm. En este artículo, nos centraremos en la perspectiva del descubrimiento de vulnerabilidades, analizando las vulnerabilidades específicas identificadas durante los procesos de auditoría y verificación, y las lecciones aprendidas de ellas. Para una discusión general sobre la verificación formal avanzada de las cadenas de bloques ZKP, consulte el artículo sobre la verificación formal avanzada de las cadenas de bloques ZKP.

Antes de hablar de las vulnerabilidades de ZK, entendamos primero cómo CertiK realiza la verificación formal de ZK. Para sistemas complejos como la máquina virtual ZK (zkVM), el primer paso en la verificación formal (FV) es definir claramente lo que se debe verificar y sus propiedades. Esto requiere una revisión exhaustiva del diseño, la implementación del código y la configuración de prueba del sistema ZK. Este proceso se superpone con las auditorías periódicas, pero difiere en que, después de la revisión, se deben establecer los objetivos y las propiedades de la verificación. En CertiK, nos referimos a esto como verificación orientada a auditorías. El trabajo de auditoría y verificación suele estar integrado. En el caso de zkWasm, realizamos auditorías y verificaciones formales simultáneamente.

¿Qué es una vulnerabilidad ZK?

La característica principal de los sistemas de prueba de conocimiento cero (ZKP) es que permiten la transferencia de una breve prueba cifrada de los cálculos ejecutados fuera de línea o de forma privada (como las transacciones de blockchain) a un verificador de ZKP. El verificador comprueba y confirma la prueba para asegurarse de que el cálculo se ha realizado según lo declarado. En este contexto, una vulnerabilidad de ZK permitiría a un hacker presentar pruebas de ZK falsificadas para transacciones falsas y hacer que el verificador de ZKP las acepte.

Para un probador de zkVM, el proceso de prueba de ZK implica ejecutar un programa, generar registros de ejecución para cada paso y convertir estos registros de ejecución en un conjunto de tablas numéricas (un proceso conocido como "aritmética"). Estos números deben satisfacer un conjunto de restricciones (el "circuito"), que incluyen las relaciones entre celdas de tabla específicas, constantes fijas, restricciones de búsqueda de bases de datos entre tablas y ecuaciones polinómicas (o "puertas") que debe satisfacer cada par de filas de tabla adyacentes. La verificación en cadena puede confirmar la existencia de una tabla que cumple con todas las restricciones sin revelar los números específicos dentro de la tabla.

Tabla de aritmética en zkWasm

La precisión de cada restricción es crucial. Cualquier error en una restricción, ya sea demasiado débil o faltante, podría permitir a un pirata informático presentar pruebas engañosas. Estas tablas pueden parecer representar una ejecución válida de un contrato inteligente, pero en realidad no lo son. En comparación con las máquinas virtuales tradicionales, la opacidad de las transacciones de zkVM amplifica estas vulnerabilidades. En las cadenas que no son ZK, los detalles de los cálculos de las transacciones se registran públicamente en la cadena de bloques; sin embargo, las zkVM no almacenan estos detalles en la cadena. Esta falta de transparencia hace que sea difícil determinar los detalles de un ataque o incluso si se ha producido un ataque.

El circuito ZK que hace cumplir las reglas de ejecución de las instrucciones zkVM es extremadamente complejo. Para zkWasm, la implementación de su circuito ZK implica más de 6.000 líneas de código Rust y cientos de restricciones. Esta complejidad a menudo significa que podría haber múltiples vulnerabilidades esperando a ser descubiertas.

Arquitectura de circuito zkWasm

De hecho, a través de la auditoría y la verificación formal de zkWasm, hemos descubierto varias vulnerabilidades de este tipo. A continuación, discutiremos dos ejemplos representativos y examinaremos las diferencias entre ellos.

Vulnerabilidad de código: ataque de inyección de datos Load8

La primera vulnerabilidad involucra la instrucción Load8 en zkWasm. En zkWasm, las lecturas de memoria de pila se realizan mediante un conjunto de instrucciones LoadN, donde N es el tamaño de los datos que se van a cargar. Por ejemplo, Load64 debe leer datos de 64 bits de una dirección de memoria zkWasm. Load8 debe leer datos de 8 bits (es decir, un byte) de la memoria y rellenarlos con ceros para crear un valor de 64 bits. Internamente, zkWasm representa la memoria como una matriz de bytes de 64 bits, por lo que necesita "seleccionar" una parte de la matriz de memoria. Esto se hace utilizando cuatro variables intermedias (u16_cells), que juntas forman el valor de carga completo de 64 bits.

Las restricciones para estas instrucciones LoadN se definen de la siguiente manera:

Esta restricción se divide en tres casos: Load32, Load16 y Load8. Load64 no tiene restricciones porque las unidades de memoria son exactamente de 64 bits. Para el caso de Load32, el código garantiza que los 4 bytes (32 bits) altos en la unidad de memoria deben ser cero.

Para el caso de Load16, el código garantiza que los 6 bytes (48 bits) de la unidad de memoria sean cero.

Para el caso de Load8, debe requerir que los 7 bytes (56 bits) altos en la unidad de memoria sean cero. Desafortunadamente, este no es el caso en el código.

Como puede ver, solo los bits altos de 9 a 16 están restringidos a cero. Los otros 48 bits altos pueden ser cualquier valor y aún así pasar como "lectura de memoria".

Explotando esta vulnerabilidad, un hacker podría alterar la prueba ZK de una secuencia de ejecución legítima, lo que provocaría que la instrucción Load8 cargara estos bytes inesperados, lo que provocaría la corrupción de los datos. Además, a través de una disposición cuidadosa del código y los datos circundantes, podría desencadenar ejecuciones y transferencias falsas, lo que llevaría al robo de datos y activos. Estas transacciones falsificadas podrían pasar los controles de los verificadores de zkWasm y ser reconocidas incorrectamente como transacciones legítimas por la cadena de bloques.

Solucionar esta vulnerabilidad es bastante sencillo.

Esta vulnerabilidad representa una clase de vulnerabilidades ZK llamadas "vulnerabilidades de código" porque se originan en la implementación del código y se pueden solucionar fácilmente mediante modificaciones menores del código local. Como estarás de acuerdo, estas vulnerabilidades también son relativamente más fáciles de identificar para las personas.

Vulnerabilidad de diseño: Ataque de retorno falsificado

Echemos un vistazo a otra vulnerabilidad, esta vez relacionada con la invocación y el retorno de zkWasm. La invocación y la devolución son instrucciones fundamentales de la máquina virtual que permiten que un contexto en ejecución (por ejemplo, una función) llame a otro y reanude la ejecución del contexto de llamada después de que el destinatario complete su ejecución. Cada invocación espera un retorno más adelante. Los datos dinámicos rastreados por zkWasm durante el ciclo de vida de la invocación y el retorno se conocen como "trama de llamada". Dado que zkWasm ejecuta instrucciones secuencialmente, todas las tramas de llamada se pueden ordenar en función de su ocurrencia durante el tiempo de ejecución. A continuación se muestra un ejemplo de código de invocación/retorno que se ejecuta en zkWasm.

Los usuarios pueden llamar a la función buy_token() para comprar tokens (posiblemente mediante el pago o la transferencia de otros artículos valiosos). Uno de sus pasos principales es aumentar el saldo de la cuenta de tokens en 1 llamando a la función add_token(). Dado que el propio demostrador ZK no admite la estructura de datos de la trama de llamada, se necesitan la tabla de ejecución (E-Table) y la tabla de salto (J-Table) para registrar y realizar un seguimiento del historial completo de estas tramas de llamada.

La figura anterior ilustra el proceso de buy_token() llamando a add_token() y regresando de add_token() a buy_token(). Se puede ver que el saldo de la cuenta de tokens aumenta en 1. En la tabla de ejecución, cada paso de ejecución ocupa una fila, incluido el número de trama de llamada actual que se está ejecutando, el nombre de la función de contexto actual (solo con fines ilustrativos), el número de la instrucción de ejecución actual dentro de la función y la instrucción actual almacenada en la tabla (solo con fines ilustrativos). En la tabla de salto, cada trama de llamada ocupa una fila, almacenando el número de su trama de llamador, el nombre de contexto de la función de llamada (solo con fines ilustrativos) y la siguiente posición de instrucción de la trama de llamada (para que la trama pueda devolver). En ambas tablas, hay una columna "jops" que rastrea si la instrucción actual es una llamada/retorno (en la tabla de ejecución) y el número total de instrucciones de llamada/retorno para esa trama (en la tabla de salto).

Como era de esperar, cada llamada debe tener un retorno correspondiente, y cada trama debe tener solo una llamada y un retorno. Como se muestra en la figura anterior, el valor de "jops" para el primer fotograma de la tabla de salto es 2, correspondiente a la primera y tercera filas de la tabla de ejecución, donde el valor de "jops" es 1. Todo parece normal en este momento.

Sin embargo, hay un problema aquí: mientras que una llamada y una devolución aumentarán el recuento de "jops" para el marco a 2, dos llamadas o dos devoluciones también darán como resultado un recuento de 2. Tener dos llamadas o dos devoluciones por fotograma puede parecer absurdo, pero es importante recordar que esto es exactamente lo que un hacker intentaría hacer rompiendo las expectativas.

Es posible que ahora te sientas emocionado, pero ¿realmente hemos encontrado el problema?

Resulta que dos llamadas no son un problema porque las restricciones de la Tabla de Ejecución y la Tabla de Salto impiden que dos llamadas se codifiquen en la misma fila de una trama porque cada llamada genera un nuevo número de trama, es decir, el número de trama de llamada actual más 1.

Sin embargo, la situación no es tan afortunada para dos retornos: dado que no se crea una nueva trama en la devolución, un hacker podría obtener la Tabla de Ejecución y la Tabla de Salto de una secuencia de ejecución legítima e inyectar devoluciones falsificadas (y las tramas correspondientes). Por ejemplo, el ejemplo anterior de Tabla de ejecución y Tabla de salto de buy_token() llamando a add_token() podría ser manipulado por un hacker en el siguiente escenario:

El hacker inyectó dos retornos falsificados entre la llamada original y el retorno en la tabla de ejecución y agregó una nueva fila de marco falsificado en la tabla de salto (el retorno original y los pasos de ejecución de instrucciones posteriores en la tabla de ejecución deben incrementarse en 4). Dado que el recuento de "jops" para cada fila de la tabla de salto es 2, se satisfacen las restricciones y el verificador de pruebas de zkWasm aceptaría la "prueba" de esta secuencia de ejecución falsificada. Como se ve en la figura, el saldo de la cuenta de tokens aumenta 3 veces en lugar de 1. Por lo tanto, el hacker podría obtener 3 tokens por el precio de 1.

Hay varias formas de abordar este problema. Un enfoque obvio es realizar un seguimiento separado de las llamadas y las devoluciones y asegurarse de que cada trama tenga exactamente una llamada y una retorno.

Es posible que haya notado que hasta ahora no hemos mostrado ni una sola línea de código para esta vulnerabilidad. La razón principal es que no hay una línea de código problemática; La implementación del código se alinea perfectamente con los diseños de tablas y restricciones. El problema radica en el diseño en sí, al igual que la solución.

Podría pensar que esta vulnerabilidad debería ser obvia, pero en realidad no lo es. Esto se debe a que hay una brecha entre "dos llamadas o dos devoluciones también darán como resultado un recuento de 'jops' de 2" y "dos devoluciones son realmente posibles". Esto último requiere un análisis detallado y exhaustivo de varias restricciones en la Tabla de Ejecución y la Tabla de Salto, lo que dificulta la realización de un razonamiento informal completo.

Comparación de dos vulnerabilidades

La "Vulnerabilidad de inyección de datos de Load8" y la "Vulnerabilidad de devolución de falsificación" tienen el potencial de permitir a los piratas informáticos manipular las pruebas de ZK, crear transacciones falsas, engañar a los verificadores de pruebas y participar en robos o secuestros. Sin embargo, su naturaleza y la forma en que fueron descubiertos son bastante diferentes.

La "vulnerabilidad de inyección de datos Load8" se descubrió durante la auditoría de zkWasm. Esta no fue una tarea fácil, ya que tuvimos que revisar cientos de restricciones en más de 6.000 líneas de código Rust y docenas de instrucciones zkWasm. A pesar de esto, la vulnerabilidad fue relativamente fácil de detectar y confirmar. Dado que esta vulnerabilidad se corrigió antes de que comenzara la verificación formal, no se encontró durante el proceso de verificación. Si esta vulnerabilidad no se hubiera descubierto durante la auditoría, podríamos esperar que se encontrara durante la verificación de la instrucción Load8.

La "vulnerabilidad de devolución falsificada" se descubrió durante la verificación formal después de la auditoría. Una de las razones por las que no pudimos descubrirlo durante la auditoría es que zkWasm tiene un mecanismo similar a los "jops" llamados "mops", que rastrea las instrucciones de acceso a la memoria correspondientes a los datos históricos de cada unidad de memoria durante el tiempo de ejecución de zkWasm. De hecho, las restricciones en los recuentos de mops son correctas porque solo rastrea un tipo de instrucción de memoria, escrituras de memoria, y los datos históricos de cada unidad de memoria son inmutables y se escriben solo una vez (el recuento de trapeadores es 1). Pero incluso si hubiéramos notado esta vulnerabilidad potencial durante la auditoría, no habríamos podido confirmar o descartar fácilmente todos los escenarios posibles sin un razonamiento formal riguroso sobre todas las restricciones relevantes, ya que en realidad no hay ninguna línea de código que sea incorrecta.

En resumen, estas dos vulnerabilidades pertenecen a las categorías de "vulnerabilidades de código" y "vulnerabilidades de diseño", respectivamente. Las vulnerabilidades de código son relativamente sencillas, más fáciles de descubrir (código defectuoso) y más fáciles de razonar y confirmar. Las vulnerabilidades de diseño pueden ser muy sutiles, más difíciles de descubrir (sin código "defectuoso") y más difíciles de razonar y confirmar.

Mejores prácticas para descubrir vulnerabilidades de ZK

Basándonos en nuestra experiencia auditando y verificando formalmente zkVM y otras cadenas ZK y no ZK, aquí hay algunas sugerencias sobre cómo proteger mejor los sistemas ZK:

Comprobación del código y el diseño

Como se mencionó anteriormente, tanto el código como el diseño de ZK pueden contener vulnerabilidades. Ambos tipos de vulnerabilidades pueden comprometer potencialmente la integridad del sistema ZK, por lo que deben abordarse antes de que el sistema se ponga en funcionamiento. Un problema con los sistemas ZK, en comparación con los sistemas que no son ZK, es que cualquier ataque es más difícil de detectar y analizar porque sus detalles computacionales no están disponibles públicamente o no se conservan en la cadena. Como resultado, las personas pueden ser conscientes de que se ha producido un ataque de piratas informáticos, pero es posible que no conozcan los detalles técnicos de cómo sucedió. Esto hace que el costo de cualquier vulnerabilidad de ZK sea muy alto. En consecuencia, el valor de garantizar la seguridad de los sistemas ZK por adelantado también es muy alto.

Realizar auditorías y verificaciones formales

Las dos vulnerabilidades que discutimos aquí se descubrieron a través de la auditoría y la verificación formal. Algunos podrían suponer que la verificación formal por sí sola obvia la necesidad de auditoría, ya que todas las vulnerabilidades se detectarían mediante una verificación formal. Sin embargo, nuestra recomendación es realizar ambos. Como se explicó al principio de este artículo, el trabajo de verificación formal de alta calidad comienza con una revisión exhaustiva, una inspección y un razonamiento informal sobre el código y el diseño, que se superpone con la auditoría. Además, encontrar y resolver vulnerabilidades más simples durante la auditoría puede simplificar y agilizar el proceso de verificación formal.

Si está llevando a cabo una auditoría y una verificación formal para un sistema ZK, el enfoque óptimo es realizar ambas simultáneamente. Esto permite a los auditores y a los ingenieros de verificación formal colaborar de manera eficiente, lo que podría descubrir más vulnerabilidades, ya que se requieren entradas de auditoría de alta calidad para la verificación formal.

Si su proyecto ZK ya ha sido sometido a auditorías (kudos) o múltiples auditorías (grandes kudos), nuestra sugerencia es realizar una verificación formal en el circuito en función de los resultados de la auditoría anterior. Nuestra experiencia con la auditoría y la verificación formal en proyectos como zkVM y otros, tanto ZK como no ZK, ha demostrado repetidamente que la verificación formal a menudo captura vulnerabilidades que se pasan por alto durante la auditoría. Dada la naturaleza de ZKP, si bien los sistemas ZK deberían ofrecer una mejor seguridad y escalabilidad de blockchain que las soluciones que no son ZK, la criticidad de su seguridad y corrección es mucho mayor que la de los sistemas tradicionales que no son ZK. Por lo tanto, el valor de la verificación formal de alta calidad para los sistemas ZK supera con creces el de los sistemas que no son ZK.

Garantizar la seguridad de los circuitos y contratos inteligentes

Las aplicaciones ZK suelen constar de dos componentes: circuitos y contratos inteligentes. Para las aplicaciones basadas en zkVM, existen circuitos zkVM universales y aplicaciones de contratos inteligentes. Para las aplicaciones que no se basan en zkVM, hay circuitos ZK específicos de la aplicación junto con los contratos inteligentes correspondientes implementados en la cadena L1 o en el otro extremo de un puente.

Nuestros esfuerzos de auditoría y verificación formal para zkWasm solo involucran el circuito zkWasm. Sin embargo, desde la perspectiva de la seguridad general de las aplicaciones ZK, también es crucial auditar y verificar formalmente sus contratos inteligentes. Después de todo, sería lamentable que, después de invertir un esfuerzo significativo en garantizar la seguridad del circuito, la laxitud en el escrutinio de los contratos inteligentes llevara a comprometer la aplicación.

Dos tipos de contratos inteligentes merecen especial atención. El primer tipo maneja directamente las pruebas ZK. Aunque pueden no ser de gran escala, su riesgo es excepcionalmente alto. El segundo tipo comprende contratos inteligentes de mediana a gran escala que se ejecutan sobre zkVM. Sabemos que estos contratos a veces pueden ser muy complejos, y los más valiosos deben someterse a auditoría y verificación, especialmente porque los detalles de su ejecución no son visibles en la cadena. Afortunadamente, después de años de desarrollo, la verificación formal de los contratos inteligentes es ahora práctica y está preparada para objetivos apropiados de alto valor.

Resumamos el impacto de la verificación formal (FV) en los sistemas ZK y sus componentes con los siguientes puntos.

Declaración:

1. Este artículo se reproduce de [panewslab], los derechos de autor pertenecen al autor original [CertiK], si tiene alguna objeción a la reimpresión, comuníquese con el equipo de Gate Learn y el equipo lo manejará lo antes posible de acuerdo con los procedimientos pertinentes.

2. Descargo de responsabilidad: Los puntos de vista y opiniones expresados en este artículo representan solo los puntos de vista personales del autor y no constituyen ningún consejo de inversión.

3. Las versiones en otros idiomas del artículo son traducidas por el equipo de Gate Learn y no se mencionan en Gate.io, el artículo traducido no puede ser reproducido, distribuido o plagiado.