Algebraic methods for the analysis of arithmetic circuits in zero-knowledge proofs

Algebraic methods for the analysis of arithmetic circuits in zero-knowledge proofs Métodos algebraicos para el análisis de circuitos aritméticos en pruebas de conocimiento nulo Pedro Palacios Almendros Doble Grado en Ingeniería Informática - Matemáticas Facultad de Matemáticas Universidad Complutense de Madrid Trabajo de Fin de Grado del Grado en Matemáticas Madrid, 2022-2023 Directores: Albert Rubio Gimeno Clara Rodríguez Núñez Abstract In this work, an algebraic method has been developed to verify the safety of Circom circuits, a domain-specific language for defining arithmetic circuits for zero-knowledge proofs. The method is based on the reduction of the Circom circuit verification problem (for a fixed input or for any input) to the unsatisfiability of polynomial systems with coefficients in a finite field problem. Computational methods based on Gröbner bases have been studied to determine the unsatisfiability of such polynomial systems. A modular algorithm has also been implemented in order to deal with large circuits that otherwise would not be tractable using purely algebraic methods. Finally, the modular algorithm has been run on several Circom open source repositories with practical applicability, and the results have been analyzed. Keywords Circom, arithmetic circuit safety, zero-knowledge proof, Gröbner bases, finite fields, polynomial systems. Resumen En este trabajo se ha desarrollado un método algebraico para verificar la seguridad de circuitos Circom, un lenguaje de dominio específico para definir circuitos aritméticos para pruebas de conocimiento nulo. El método se basa en reducir el problema de la verificación de circuitos Circom (para una entrada fija o para cualquier entrada) al problema de insatisfacibilidad de sistemas polinómicos con coeficientes en un cuerpo finito. Se han estudiado métodos computacionales basados en bases de Gröbner para determinar la insatisfacibilidad de dichos sistemas polinómicos. También se ha creado un algoritmo modular para poder tratar circuitos grandes que de otra forma no serían abordables con métodos puramente algebraicos. Finalmente, se ha ejecutado el algoritmo modular sobre varios repositorios de código abierto escritos en Circom con aplicabilidad práctica, y se han analizado los resultados. Palabras clave Circom, seguridad de circuitos aritméticos, pruebas de conocimiento nulo, bases de Gröbner, cuerpos finitos, sistemas polinómicos. Índice general Índice i I. Introducción 1 I.1. Objetivos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 I.2. Estructura del trabajo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 I.3. Plan de trabajo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 II. Conceptos básicos 3 II.1. Pruebas de conocimiento nulo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 II.2. Circuitos aritméticos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 II.3. R1CS y ZK-SNARKs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 II.4. Circom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 III. Verificación de seguridad 11 III.1. Motivación para la seguridad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 III.2. Definición de seguridad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 III.3. De la seguridad a la satisfacibilidad de ecuaciones . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 IV. Métodos algebraicos 16 IV.1. Ideales y variedades . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 IV.2. Algoritmo de división en K[x1, . . . , xn]..................................... 18 IV.3. Bases de Gröbner . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 IV.4. Algoritmo de Buchberger . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 V. Algoritmo modular 30 V.1. Motivación para un algoritmo modular . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 V.2. Grafo de verificación . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 V.3. Algoritmo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 VI. Resultados 38 VI.1. Proyectos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 VI.2. Interpretación de los resultados . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 VII. Conclusiones 41 VII.1. Trabajo futuro . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 i Bibliografía 42 A. Código fuente 44 B. Teorema de la base de Hilbert 45 C. Ejemplos de verificación de algunos circuitos 47 C.1. Num2Bits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 C.2. Split . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 D. Ejemplos de circuitos inseguros encontrados 50 D.1. Decoder . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 D.2. FullAdder . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ii Cap´ ıtulo I Introducción En el mundo actual, la criptografía tiene más importancia que nunca debido a sus aplicaciones en transacciones financieras, comunicaciones gubernamentales y encriptación de datos personales al acceder a páginas web. La criptografía ha sido usada desde tiempos inmemoriales, pero su uso ha explotado desde la introducción de Internet. Las técnicas criptográficas usadas actualmente requieren conceptos matemáticos complejos: curvas elípticas, cuerpos finitos, geometría algebraica, etc. Debido al rápido avance de la tecnología y la alta demanda de soluciones criptográficas en ámbitos muy diversos es necesario crear un puente entre los matemáticos que desarrollan la teoría y los informáticos que las implementan en sistemas reales. Entre estos sistemas criptográficos, unos de los más útiles son las pruebas de conocimiento nulo, que permiten a un demostrador probar una afirmación a un verificador sin desvelar ningún dato más allá de la veracidad de la afirmación dada. En concreto las ZK-SNARKs permiten crear pruebas de conocimiento nulo eficientes a partir de circuitos aritméticos, cuyo funcionamiento se basa en sistemas polinómicos con coeficientes en cuerpos finitos. Debido a la alta complejidad del desarrollo de ZK-SNARKs con polinomios, lenguajes de dominio específico como Circom han sido creados para poder describir declarativamente un circuito aritmético y generar todos los artefactos necesarios para una prueba de conocimiento nulo, incluyendo el sistema polinómico. Circom permite a informáticos con poca experiencia previa en criptografía diseñar circuitos aritméticos para generar pruebas de conocimiento nulo. Sin embargo, cierto conocimiento específico sigue siendo necesario para escribir circuitos aritméticos seguros, y algunos programadores inexpertos pueden fácilmente crear circuitos inseguros. Debido al papel crucial de la criptografía, las consecuencias de los problemas de seguridad y el auge de los ciberataques, es más importante que nunca poder verificar la seguridad de protocolos criptográficos, y en concreto los basados en circuitos aritméticos diseñados con Circom. I.1. Objetivos La finalidad de este trabajo es desarrollar un método algebraico para verificar la seguridad de circuitos Circom y realizar una implementación práctica que permita su aplicación en los circuitos Circom de gran tamaño usados en la práctica. Para ello plantearemos los siguientes objetivos: 1. Estudiar métodos algebraicos para analizar la satisfacibilidad de sistemas de ecuaciones polinómicas y su aplicación en cuerpos finitos Fp. 1 I. Introducción 2 2. Aplicar dichas técnicas al problema práctico de la verificación de seguridad de circuitos Circom para pruebas de conocimiento nulo. 3. Diseñar un algoritmo modular utilizando heurísticas combinadas con técnicas algebraicas para poder verificar eficientemente circuitos Circom de gran tamaño. 4. Implementar dicho algoritmo modular en Rust de forma que pueda integrarse con el compilador de Circom. 5. Realizar una evaluación experimental de dicho algoritmo utilizando repositorios de código abierto usados en la práctica. I.2. Estructura del trabajo En el capítulo II se introducen los conceptos de pruebas de conocimiento nulo, circuitos aritméticos y Circom que utilizaremos en el resto del trabajo. En el capítulo III se define la seguridad de un circuito Circom y se expone una nueva forma de reducir el problema de la seguridad de Circom a la satisfacibilidad de un sistema polinómico con coeficientes en un cuerpo finito Fp. En el capítulo IV se exponen técnicas algebraicas para determinar la insatisfacibilidad de un sistema de polinomios utilizando bases de Gröbner, centrándonos en cuerpos finitos. En el capítulo Vse diseña un algoritmo modular que combina heurísticas con los métodos algebraicos desarrollados anteriormente para poder tratar circuitos grandes de forma eficiente. En el capítulo VI se realiza una evaluación del algoritmo modular implementado en el lenguaje Rust utilizando repositorios de código abierto escritos en Circom y se interpretan los resultados. Finalmente, en el capítulo VII se enumeran todas las conclusiones a las que se ha llegado en el trabajo y se exploran algunas líneas de trabajo futuro. En el apéndice Ase incluye un enlace al repositorio con todo el código fuente en Rust del algoritmo modular implementado. En el apéndice Bse muestra una demostración del teorema de la base de Hilbert, necesaria para demostrar la terminación de cierto algoritmo del capítulo IV para computar bases de Gröbner. En el apéndice Cse estudian dos ejemplos de verificación de circuitos Circom. En el apéndice Dse estudian dos circuitos inseguros que se encontraron en la práctica utilizando el algoritmo modular de verificación desarrollado en este trabajo. I.3. Plan de trabajo Las actividades realizadas siguieron este orden: Primero, investigar sobre conceptos básicos de ZK-SNARKs y Circom. Segundo, investigar formas de convertir el problema de seguridad de Circom a un problema algebraico. Tercero, estudiar técnicas algebraicas basadas en bases de Gröbner para resolver dicho problema. Cuarto, diseñar un algoritmo modular e implementarlo en Rust. Finalmente, realizar experimentos de prueba. Cap´ ıtulo II Conceptos básicos Este capítulo es una introducción a los conceptos subyacentes a Circom, sus aplicaciones y sus herramientas básicas. Primero introducimos las pruebas de conocimiento nulo y los circuitos aritméticos, después estudiamos los ZK-SNARK y sistemas R1CS y finalmente exploramos el compilador Circom y algunas de sus características más relevantes para nuestro trabajo. II.1. Pruebas de conocimiento nulo Una prueba de conocimiento nulo [15] es un protocolo criptográfico que permite a una de las dos partes (el demostrador), probar una afirmación a la otra parte (el verificador) sin desvelar ningún otro dato más allá de la veracidad de la afirmación expuesta. Estas pruebas son una herramienta muy importante en criptografía, como se puede ver en los siguientes ejemplos de aplicación: “Demostrar que se conoce la clave privada asociada a una clave pública”. Esto permite a una persona autenticarse sin revelar su clave privada. “Demostrar que el salario de un solicitante de crédito está en cierto rango sin desvelar el valor exacto”. Esto permite una mayor privacidad a la hora de realizar operaciones financieras, aún garantizando requisitos puestos por alguna de las dos partes. El banco ING implementó [22] en Ethereum [25] una prueba de concepto de esta tecnología. “Demostrar que el hash de un bloque de transacciones en el blockchain [26] no incurre en balances negativos”. Esto permite demostrar la validez de las transacciones del bloque sin revelar los destinatarios, los remitentes o el valor de las transacciones contenidas en dicho bloque. La criptomoneda Monero [20] utiliza tecnología similar para garantizar la privacidad en sus transacciones. Un tipo muy importante de pruebas de conocimiento nulo son las pruebas de conocimiento nulo no interactivas [9] (NIZK por sus siglas en inglés Non-Interactive Zero-Knowledge proofs), en las que el demostrador no interactúa con el verificador durante la generación de la prueba. Varios verificadores pueden, a posteriori, comprobar la veracidad de la afirmación sin necesidad de comunicarse con el demostrador. Esta propiedad permite a los smart-contracts [27] (programas almacenados en el blockchain que se ejecutan en reacción a transacciones y permiten automatizar contratos) verificar las pruebas de conocimiento nulo, pues la ejecución de los smart-contracts está aislada del mundo exterior. Algunas propiedades deseables en protocolos NIZK son las siguientes: 3 II. Conceptos básicos 4 Bajo coste computacional para generar la prueba. Pequeño tamaño de la prueba. Bajo coste computacional para verificar la prueba. Los dos últimos factores son muy relevantes al utilizar smart-contracts, pues el tiempo empleado en la verificación de la prueba y el tamaño de la prueba cuesta recursos en el blockchain y dinero. II.2. Circuitos aritméticos Un tipo importante de afirmaciones computacionales que se pueden demostrar utilizando pruebas de conocimiento nulo es la satisfacibilidad de circuitos aritméticos [24]. En general trabajaremos en el cuerpo finito de pelementos Fp . .=Z/pZcon pprimo, que es típicamente un número primo grande, de más de 250 bits. Para ilustrar la magnitud de estos primos, mostramos un ejemplo de un primo putilizado asiduamente en Ethereum para operaciones con curvas elípticas p= 21888242871839275222246405745257275088548364400416034343698204186575808495617 Intuitivamente, un circuito aritmético está formado por un conjunto de cables que toman valores en Fpy están conectados a puertas que realizan algún tipo de operación. Nosotros vamos a trabajar con dos posibles puertas: la suma de dos elementos de Fpy la multiplicación de dos elementos de Fp, ambas realizadas módulo p. A los cables del circuito se les llama señales, y pueden ser de tres tipos: Entrada (input en inglés): Son las entradas al circuito. Pueden ser públicas (las conoce tanto el demostrador como el verificador) o privadas (las conoce únicamente el demostrador). Representaremos cada entrada como ij, y al vector de todas las entradas como ¯ i. Intermedia (intermediate en inglés): Son las salidas de las puertas intermedias del circuito. Asumiremos que son siempre privadas, el verificador no las conoce. Representaremos cada intermedia como xjy al vector de todas las intermedias como ¯x. Salida (output en inglés): Son las salidas del circuito. Nosotros asumiremos que siempre son públicas, es decir, que tanto el demostrador como el verificador conocen el valor de las salidas. Representaremos cada salida como ojy al vector de todas las salidas como ¯o. El demostrador ejecutará el circuito aritmético usando los inputs tanto públicos como privados, y encontrará una asignación para cada señal que haga que se satisfaga el circuito. A este conjunto de asignaciones se le llama testigo owitness. El demostrador publicará el output (que es público), las inputs públicas (pero no las privadas) y una prueba (idealmente pequeña en tamaño) de que conoce un testigo que satisfaga el circuito. Dicha prueba no deberá revelar las asignaciones a las variables privadas. En la sección II.3 veremos algunas herramientas que nos permiten realizar estas tareas, pero antes estudiemos un circuito de ejemplo. En la figura II.1 podemos ver un circuito de ejemplo, en el que las entradas son {i0, i1, i2, i3}, las señales intermedias son {x0, x1}y la salida es o0. En este caso un testigo sería una tupla (i0, i1, i2, i3, x0, x1, o0)tal que el circuito se satisface. Si asumimos que las entradas públicas son {i0, i2}, estamos trabajando en F7, y las señales públicas Cap´ ıtulo III Verificación de seguridad En este capítulo primero motivamos la importancia de la seguridad en circuitos Circom, después definimos formalmente nuestro concepto de seguridad e introducimos un nuevo resultado: una reducción del problema de la seguridad de los circuitos Circom a la insatisfacibilidad de un cierto sistema de ecuaciones, problema que podemos resolver computacionalmente como veremos en el capítulo IV. III.1. Motivación para la seguridad Como hemos visto en el capítulo anterior, Circom permite disociar la generación de código WebAssembly de la generación de restricciones mediante el uso del operador <--, lo cual conlleva graves riesgos, pues puede provocar que la lista de restricciones R1CS (que no olvidemos es la usada para generar el demostrador y el verificador ZK-SNARK) esté subrestringida, es decir, que el testigo generado no sea la única solución válida del sistema de restricciones. Esto puede tener graves consecuencias: supongamos que cierto módulo tiene como función verificar que se conoce la clave privada asociada a una clave pública para autorizar un pago y su salida es una señal binaria que indica si la entrada privada i0es la clave privada asociada a la entrada pública i1, que representa la clave pública. Si el sistema de restricciones está subrestringido, es posible que existan varias soluciones (testigos) para el R1CS con la misma entrada. Es decir, si la entrada es una clave privada inválida, que no es la asociada a la clave pública, aparte de existir un testigo cuya salida indica que la clave privada es inválida, podría existir también otro testigo (indeseado) que afirma erróneamente que dicha clave privada es válida. Esto permitiría a un posible atacante autorizar el pago mediante una “clave privada” falsa que el verificador acepta como válida, a pesar de no ser la clave privada correcta. Más aún, es sencillo que a un programador se le olvide declarar una restricción necesaria, sin darse cuenta generando un sistema subrestringido. El paradigma de las restricciones polinómicas es radicalmente distinto al paradigma algorítmico iterativo al que están acostumbrados los programadores, acentuando aún más este problema de seguridad. Por ejemplo, en el apéndice Dse puede ver un ejemplo de un módulo inseguro de la librería estándar de Circom, que el algoritmo modular introducido en el capítulo Ves capaz de detectar. III.2. Definición de seguridad El objetivo último de este trabajo es hallar formas automáticas de probar que un circuito Circom es seguro, para lo que es necesario tener una definición formal de la seguridad. Seguiremos las definiciones sobre circuitos Circom y sus propiedades dadas en [7]. 11 III. Verificación de seguridad 12 Definición III.1. (Sistema de ecuaciones polinómico) Llamaremos sistema de ecuaciones polinómico o simplemente sistema de ecuaciones a un subconjunto finito de Fp[¯s] = Fp[s1, . . . , sn], el conjunto de polinomios sobre las variables ¯s. Representaremos el conjunto de todos los sistemas de ecuaciones polinómicos sobre las variables ¯scomo S(Fp[¯s]). Diremos que una constante ¯s0 satisface o es solución de un sistema de ecuaciones Ssi p(¯s0)=0,∀p∈ S. Observación III.2. (Restricción vs. ecuación) Para nosotros, las restricciones siempre serán cuadráticas, lineales o constantes, mientras que las ecuaciones polinómicas pueden ser polinomios de cualquier grado. Definición III.3. (Circuito Circom) Llamamos Cn×t×mal conjunto de circuitos Circom válidos que se pueden crear con nseñales de entrada, tseñales intermedias y mseñales de salida. Llamamos W:Cn×t×m×Fn p→Ft p×Fm pa la función parcial que dado un circuito y sus variables de entrada, nos devuelve las variables intermedias y de salida que genera el programa de cómputo de witness en WebAssembly generado por Circom, es decir, W(C,¯ i) = (¯x, ¯o). Dado un circuito C∈Cn×t×m, llamamos C(C)∈S(Fp[¯ i, ¯x, ¯o]) al sistema de ecuaciones polinómicas sobre las señales del circuito generado por Circom (las restricciones de la lista R1CS) cuyas variables son las entradas ¯ i, intermedias ¯xy salidas ¯o. Como las restricciones son ecuaciones polinómicas a lo sumo cuadráticas, en concreto son ecuaciones polinómicas. Es importante notar que Wes una función parcial, pues no todos los circuitos Circom tienen un witness para todas las entradas, puede haber restricciones contradictorias entre sí o alguna condición adicional necesaria sobre las entradas para que estas sean válidas. Estos problemas son detectados por el código de generación de witness, pues todas las restricciones se convierten en aserciones en WebAssembly, y se aborta el proceso de generación de la prueba. Por ello, podemos restringirnos únicamente a las entradas que generen un witness válido. Definición III.4. (Circuito Circom correcto) Decimos que un circuito Circom C∈Cn×t×m es correcto si para cualquier entrada ¯ i0∈Fn ptal que C(C)es satisfacible sustituyendo las entradas ¯ ipor ¯ i0, existe la imagen de (C,¯ i0)a través de la función Wy llamando W(C,¯ i0) = (¯xw,¯ow), entonces (¯ i0,¯xw,¯ow)es solución de C(C). A partir de ahora, salvo que digamos lo contrario, asumiremos que los programas Circom con los que tratamos son correctos. En [7] se introduce la noción de circuito Circom seguro y fuertemente seguro para todas las entradas. En el capítulo Vdesarrollaremos un algoritmo para probar que un circuito es seguro para una cierta entrada fija, por lo que extendemos la definición de seguridad para reflejar esto. Los programas Circom fuertemente seguros son aquellos en los que la entrada fija las señales intermedias y las salidas, y los programas Circom seguros son aquellos en los que la entrada fija las salidas, pero las señales intermedias pueden variar. Más formalmente: Definición III.5. .(Programa Circom seguro) Decimos que un programa Circom correcto C∈Cn×t×mes seguro para cierta entrada fija ¯ i0∈Fn ptal que existe W(C,¯ i0)si cuando llamamos (¯xw,¯ow). .=W(C,¯ i0)∈Ft×m p, entonces todos los vectores de señales en {¯ i0} × Ft×m p que satisfacen todas las restricciones de C(C)son de la forma (¯ i0,¯x′,¯ow). De igual forma, decimos que es fuertemente seguro para cierta entrada fija ¯ i0∈Fn ptal que existe W(C,¯ i0) = (¯xw,¯ow) si el único vector de {¯ i0} × Ft×m pque satisface todas las restricciones de C(C)es (¯ i0,¯xw,¯ow). Si un circuito es seguro (respectivamente fuertemente seguro) para toda entrada ¯ i∈Fn ptal que existe W(C,¯ i), diremos que el circuito es seguro (respectivamente fuertemente seguro). III. Verificación de seguridad 13 Un ejemplo de módulo seguro pero no fuertemente seguro es IsZero, definido en el código II.4 como veremos en el ejemplo III.11. III.3. De la seguridad a la satisfacibilidad de ecuaciones En esta sección introducimos el primer resultado novedoso de este trabajo. Para poder desarrollar algoritmos para verificar automáticamente la seguridad de un circuito, reduciremos el problema de la seguridad a la insatisfacibilidad de un sistema de ecuaciones, que podemos analizar con técnicas algebraicas que estudiaremos en el capítulo IV. Para ello, dado un circuito Circom C, vamos a hallar un sistema de ecuaciones polinómicas S, tal que si el sistema Sno tiene ninguna solución, entonces podamos garantizar alguna propiedad de seguridad de C. Para hallar dicho sistema S, primero necesitamos definir algunos conceptos. Definición III.6. (Sustitución) Dado un sistema de ecuaciones polinómicas S ∈ S(Fp[¯s, ¯x]), un vector de variables ¯s∈Fn py otro vector de variables ¯s′∈Fn p, definimos S′=S[¯s→¯s′] = S[s1→s′ 1, . . . , sn→s′ n]∈S(Fp[¯s′,¯x]) como el sistema de ecuaciones resultante de sustituir simultáneamente en el sistema Stodas las apariciones de las variables ¯spor ¯s′. Análogamente definimos la sustitución de variables por constantes, dejando de ser dichos símbolos variables a resolver y pasando a ser constantes fijas. El primer paso para verificar la seguridad (que consiste en la no existencia de dos soluciones distintas con la misma entrada) es codificar que dos vectores de señales son distintos utilizando una ecuación polinómica. Veamos como hacerlo añadiendo unas variables auxiliares ¯uque tendrán como función poder ser el inverso multiplicativo de cualquier número no nulo. Definición y Teorema III.7. (Prohibición) Dado un vector de variables ¯x∈Fn py otro vector de variables ¯y∈Fn p, definimos el sistema P(¯x, ¯y)∈S(Fp[¯x, ¯y, ¯u]): P(¯x, ¯y) = {((x1−y1)·u1−1) ·((x2−y2)·u2−1) · · · ((xn−yn)·un−1) = 0} Entonces: 1. Si (¯x′,¯y′,¯u′)es solución de P(¯x, ¯y), entonces ¯x′= ¯y′, donde la desigualdad es en sentido vectorial, es decir, existe algún índice ital que x′ i=y′ i. 2. Dadas dos ¯x′,¯y′∈Fn ptal que ¯x′= ¯y′, entonces ∃¯u′tal que (¯x′,¯y′,¯u′)es solución de P(¯x, ¯y). Demostración. 1. Veamos que existe un ital que x′ i=y′ i. Supongamos que no ocurre, por lo que para todo ise da que x′ i−y′ i= 0 y al ser (¯x′,¯y′,¯u′)solución de P(¯x, ¯y), tenemos que (0 ·u′ 1−1) ·(0 ·u′ 2−1) · · · (0 ·u′ n−1) = 0 ⇐⇒ (−1)n= 0, llegando a una contradicción. 2. Supongamos que existe un ital que x′ i=y′ i, por lo que x′ i−y′ i= 0 y por ser Fpun cuerpo, ∃u′ i:= (x′ i−y′ i)−1. Finalmente, tenemos que (x′ i−y′ i)ui−1=1−1=0, por lo que (¯x′,¯y′,¯u′)es solución de P(¯x, ¯y), pudiendo elegir valores arbitrarios para ujpara j=i. Abusaremos de la notación y permitiremos crear sistemas de ecuaciones prohibición P(¯x, ¯x0) donde ¯x0sea un vector de constantes en vez de variables, que tiene la misma definición y propiedades que las vistas en el teorema III.7. III. Verificación de seguridad 14 Ahora estamos en condiciones de hallar los sistemas polinómicos Stal que su satisfacibilidad es equivalente a alguna propiedad de seguridad de un circuito Circom. En el caso de la seguridad para cierta entrada fija añadiremos a las restricciones del circuito Circom (en las que sustituimos las entradas por la entrada fija dada) la restricción prohibición que garantice que alguna salida (o en el caso de seguridad fuerte, también alguna intermedia) sea distinta a su valor en el testigo producido por el código WebAssembly. Teorema III.8. (Seguridad para cierta entrada) Dado un circuito Circom correcto C∈ Cn×t×mcon C(C)∈S(Fp[¯ i, ¯x, ¯o]) y cierta entrada fija ¯ i0∈Fn ptal que W(C,¯ i0) = (¯xw,¯ow), entonces: 1. Ces seguro para ¯ i0si y solo si Sno tiene solución, donde S=C(C)[¯ i→¯ i0]∪ P(¯o, ¯ow)∈S(Fp[¯x, ¯o, ¯u]) 2. Ces fuertemente seguro para ¯ i0si y solo si Sno tiene solución, donde S=C(C)[¯ i→¯ i0]∪ P((¯x, ¯o),(¯xw,¯ow)) ∈S(Fp[¯x, ¯o, ¯u]) Demostración. Demostramos únicamente la primera afirmación, al ser la segunda demostración análoga pero ampliando la lista de variables prohibidas de P(¯o, ¯ow)aP((¯x, ¯o),(¯xw,¯ow)). Probemos que Stiene solución ⇐⇒ Cno es seguro: ⇒Supongamos que Stiene una solución (¯x′,¯o′,¯u′), lo que por construcción indica que (¯ i0,¯x′,¯o′)es solución de C(C)y por tanto un witness válido del circuito. Sin embargo, (¯o′,¯u′)también es solución de P(¯o, ¯ow), por lo que por el teorema III.7,¯o′= ¯ow, por lo que Cno es seguro. ⇐Supongamos que Cno es seguro para ¯ i0, por lo que existe (¯ i0,¯x′,¯o′)que satisface C(C)y cumple ¯o′= ¯ow. Pero por el teorema III.7, esta última condición nos indica que ∃¯u′tal que (¯o′,¯u′)es solución de P(¯o, ¯ow). Por tanto, (¯x′,¯o′,¯u′)es una solución de S. Encontramos ahora una caracterización de una propiedad de seguridad más fuerte, que un circuito Circom sea seguro para todas las entradas, no solo para una. Para ello, añadiremos dos copias de las restricciones del circuito Circom, cada una de ellas con sus variables intermedias y salidas distintas, pero compartiendo las mismas entradas. Después, utilizando el polinomio prohibición, garantizaremos que alguna salida (o también alguna variable intermedia en el caso de seguridad fuerte) difiera entre las dos copias. Teorema III.9. (Seguridad para todas las entradas) Dado un circuito Circom correcto C∈Cn×t×mcon C(C)∈S(Fp[¯ i, ¯x, ¯o]), entonces: 1. C es seguro si y solo si Sno tiene solución, donde S=C(C)[¯x→¯x1,¯o→¯o1]∪ C(C)[¯x→¯x2,¯o→¯o2]∪ P(¯o1,¯o2)∈S(Fp[¯ i, ¯x1,¯x2,¯o1,¯o2,¯u]) 2. C es fuertemente seguro si y solo si S ∈ S(Fp[¯ i, ¯x1,¯x2,¯o1,¯o2,¯u]) no tiene solución, donde S=C(C)[¯x→¯x1,¯o→¯o1]∪ C(C)[¯x→¯x2,¯o→¯o2]∪ P((¯x1,¯o1),(¯x2,¯o2)) III. Verificación de seguridad 15 Demostración. Demostramos únicamente la primera afirmación, al ser la segunda demostración análoga pero ampliando la lista de variables prohibidas de P(¯o1,¯o2)aP((¯x1,¯o1),(¯x2,¯o2)). Probemos que Stiene solución ⇐⇒ Cno es seguro: ⇒Supongamos que Stiene una solución (¯ i′,¯x′1,¯x′2,¯o′1,¯o′2,¯u′). Entonces, por la construcción de S,(¯ i′,¯x′1,¯o′1)y(¯ i′,¯x′2,¯o′2)satisfacen C(C), por lo que ambas son witness válidas del circuito. Además, por el teorema III.7, como (¯o′1,¯o′2)satisfacen P(¯o1,¯o2), entonces ¯o′1= ¯o′2y por lo tanto las dos witnesses tienen salidas distintas, por lo que Cno es seguro. ⇐Supongamos que Cno es seguro, por lo que existen (¯ i′,¯x′1,¯o′1)y(¯ i′,¯x′2,¯o′2)dos witnesses de Ctal que ¯o′1= ¯o2. Por ser witness del circuito, tenemos que (¯ i, ¯x′1,¯o′1)y(¯ i, ¯x′2,¯o′2) satisfacen C(C). Además, como ¯o′1= ¯o′2, por el teorema III.7 ∃¯u′tal que (¯o′1,¯o′2,¯u′)es solución de P(¯o1,¯o2). Juntándolo todo, tenemos que (¯ i′,¯x′1,¯x′2,¯o′1,¯o′2,¯u′)es solución de S. Por tanto, si encontramos una forma de determinar que un sistema polinómico con coeficientes en Fpno tiene solución, como haremos en el capítulo IV, habremos conseguido el objetivo de crear un algoritmo que automáticamente garantice la seguridad de un circuito: primero construimos el sistema Sde los teoremas III.8 oIII.9 y determinamos si tiene una única solución. Observación III.10. (Completitud) Nótese que un algoritmo que no sea completo también tendría un gran interés. Debido a la magnitud del problema a resolver, con circuitos que implementan primitivas criptográficas complejas de varios cientos de miles de restricciones es muy improbable encontrar un algoritmo completo que sea capaz de tratar las entradas en un tiempo razonable. Un algoritmo que determine la insatisfacibilidad de un sistema de ecuaciones de forma correcta pero produzca falsos negativos (es decir, clasifique sistemas como satisfacibles cuando son insatisfacibles) también sería de gran interés, pues sería un algoritmo correcto pero no completo para garantizar la seguridad de ciertos circuitos Circom. Ejemplo III.11. El circuito IsZero descrito en el código II.4 no es fuertemente seguro para todas las entradas. Demostración. El sistema polinómico Sdel teorema III.9 es                    out1 +inp ·inv1 −1 = 0 inp ·out1 = 0 out2 +inp ·inv2 −1 = 0 inp ·out2 = 0 ((out1 −out2)·u1−1) ·((inv1 −inv2)·u2−1) = 0 Una solución para Ses inp = 0,out1 =out2 = 1,inv1 = 1,inv2 = 0,u1= 0,u2= 1, por lo que Ses satisfacible y por el teorema III.9 el circuito IsZero no es fuertemente seguro. En cambio, el sistema es insatisfacible si incluimos únicamente la salida en el polinomio prohibición. Esta insatisfacibilidad se puede determinar utilizando métodos algebraicos que veremos en el capítulo IV. Cap´ ıtulo IV Métodos algebraicos En los teoremas III.8 yIII.9 redujimos el problema de demostrar la seguridad de un circuito Circom a discernir si un sistema de ecuaciones polinómico tiene alguna solución en un cuerpo finito Fp. En este capítulo estudiamos las herramientas algebraicas necesarias para decidir la satisfacibilidad de un sistema de ecuaciones polinómico. Primero damos una introducción a los ideales y variedades, después examinamos algunos resultados sobre el algoritmo de división en un anillo de polinomios en varias variables, introducimos las bases de Gröbner como herramienta para determinar la insatisfacibilidad y finalmente estudiamos el algoritmo de Buchberger para poder obtener computacionalmente una base de Gröbner. Este estudio se basa en los resultados obtenidos en los libros [5,10], aunque se ha condensado el material y reescrito para adaptarse a las contingencias de nuestra aplicación concreta. IV.1. Ideales y variedades En vez de trabajar con sistemas de ecuaciones, vamos a trabajar con objetos algebraicos llamados ideales, que nos permitirán expresar dichos sistemas de una forma más útil computacionalmente. Notación IV.1. (Anillo de polinomios) Llamaremos K[x1, . . . , xn]al anillo conmutativo de polinomios sobre las variables x1, . . . , xncon coeficientes en el cuerpo K. Definición IV.2. (Ideal) Diremos que un subconjunto Ide un anillo conmutativo Aes un ideal si: 1. 0∈I 2. Si f, g ∈I, entonces f+g∈I 3. Si f∈Iyh∈ A, entonces f·h∈I Definición IV.3. Sean f1, . . . , fm∈ A, siendo Aun anillo conmutativo. Definimos el ideal generado por f1, . . . , fmcomo el conjunto ⟨f1, . . . , fm⟩=(m X i=1 fi·gi:gi∈ A) Es inmediato comprobar que I=⟨f1, . . . , fm⟩es un ideal. Diremos que {f1, . . . , fm}es una base de I y que Ies finitamente generado. De aquí en adelante, salvo mención expresa, trabajaremos en el anillo K[x1, . . . , xn], y cuando nos refiramos a un ideal nos referiremos siempre a ideales de dicho anillo. 16 IV. Métodos algebraicos 17 Definamos ahora la variedad asociada a un ideal finitamente generado, que es lo que nos permitirá enlazar los ideales con los sistemas de ecuaciones polinómicos. Definición IV.4. Dado un ideal de K[x1, . . . , xn]finitamente generado I=⟨f1, . . . , fm⟩, definimos la variedad V(I)asociada al ideal como el conjunto V(I) = {x∈Kn:fi(x)=0 ∀i∈ {1, . . . , m}} es decir, el conjunto de puntos de Kndonde se anulan todos los polinomios de la base simultáneamente. Es fácil comprobar que la definición anterior no depende de la base elegida para el ideal. Definición IV.5. (Ideal asociado a un sistema de ecuaciones) Si tenemos un sistema de ecuaciones polinómicas sobre un cuerpo K            f1(¯x) = 0 f2(¯x) = 0 . . . fm(¯x) = 0 definimos el ideal asociado al sistema de ecuaciones como I=⟨f1, . . . , fm⟩. Por la propia definición se deduce que V(I)es el conjunto de soluciones del sistema polinómico. Por tanto, el problema de los teoremas III.8 yIII.9 se reduce a decidir si V(I) = ∅dado un ideal finitamente generado I. Teorema IV.6. Sea f1, . . . , fmun ideal finitamente generado. Si 1∈I, entonces V(I) = ∅ Demostración. Si 1∈I, por definición de base, 1 = f1g1+· · · +fmgmpara ciertos gi∈ K[x1, . . . , xn]. Si V(I)=∅, entonces ∃x∈V(I), y aplicando los polinomios de la igualdad anterior en xllegamos a que 1 = f1(x) |{z} 0 g1(x) + · · · +fm(x) |{z} 0 gm(x) = 0, una contradicción. Observación IV.7. (Completitud) El teorema IV.6 es la implicación trivial de la forma débil del Nullstellensatz, demostrado por Hilbert. La otra implicación también se da en cuerpos algebraicamente cerrados. En [14] se demuestra una versión débil del Nullstellensatz para cuerpos finitos, que se reduce a lo siguiente: Sea K=Fp, y sea I=⟨f1, . . . , fm, xp 1−x1, . . . , xp n−xn⟩. Entonces, 1/∈Isi y solamente si existe una solución simultánea para todas las ecuaciones fi(¯x) = 0 en Fn p. Como vemos, hay que añadir al ideal los polinomios xp i−xi, que “codifican” los ceros que añade el cuerpo finito. Estos polinomios tienen el primo pdel cuerpo en el exponente. Recordemos que en nuestro problema, ppuede tener más de 250 bits, haciendo el problema intratable computacionalmente. Por tanto, renunciaremos a la completitud al no añadir los polinomios xp i−xiextra, conformándonos con poder demostrar la seguridad correctamente, tal y como comentamos en la observación III.10. Además, en el capítulo VI veremos que en la práctica no hemos encontrado ningún circuito en el que se pierda completitud por no añadir los polinomios xp i−xi. En las siguientes secciones desarrollaremos métodos para poder decidir si un polinomio dado (estando nosotros interesados en el polinomio constantemente uno) pertenece a un ideal, hallando IV. Métodos algebraicos 18 así un algoritmo correcto (pero no completo) para garantizar la seguridad de ciertos circuitos Circom. IV.2. Algoritmo de división en K[x1, . . . , xn] Para decidir si un polinomio está en un ideal, nos gustaría poder dividir un polinomio f∈ K[x1, . . . , xn]por otros polinomios f1,...fm∈K[x1, . . . , xn], es decir, expresar fcomo f=q1f1+· · · +qmfm+r donde q1, . . . , qm, r ∈K[x1, . . . , xn], y nos gustaría poner alguna restricción sobre el resto r. Antes de desarrollar un algoritmo de este estilo, recordemos el algoritmo de la división en polinomios de una única variable, para encontrar alguna manera de generalizarlo a polinomios de varias variables. Para ello, necesitamos algunas definiciones. Definiciones IV.8. Sea p=Pm i=0 aixi∈K[x]con am= 0, entonces llamamos grado a deg(p) = mytérmino director aTD(p) = amxm. En el caso de que p= 0, definimos TD(0) = 0 y diremos que deg(0) no está definido. Algoritmo de división en K[x] Algoritmo 1 Algoritmo de división en K[x] Entrada: a, b ∈K[x],b= 0 Salida: Cociente q∈K[x], resto r∈K[x] q←0 r←a while r= 0 and deg(r)≥deg(b)do ▷El invariante del bucle es a=b·q+r tmp ←TD(r) TD(b) q←q+tmp r←r−tmp ·b end while Teorema IV.9. El algoritmo 1termina y computa una división en K[x], es decir, al finalizar se cumple que a=b·q+ry o bien r= 0 o bien deg(r)< deg(b). Demostración. Corrección. Comenzaremos demostrando que en toda iteración del bucle se cumple el invariante a=b·q+r. Esto es trivialmente cierto al comienzo del programa, ya que a= 0·b+a, y si se cumple al comienzo de una iteración del bucle, al final también: b·q+TD(r) TD(b) | {z } q′ +r−TD(r) TD(b)b | {z } r′ =b·q+r | {z } a +bTD(r) TD(b)−TD(r) TD(b)b | {z } 0 =a Por tanto, al terminar el algoritmo se cumplirá que a=b·q+r, y como hemos salido del bucle, también se cumplirá la negación de la condición, por lo que o bien r= 0 o bien deg(r)<deg(b). IV. Métodos algebraicos 19 Terminación. La observación clave es que en cada iteración del bucle, o bien rse convierte en 0, o bien el grado de rdecrece estrictamente, ya que el término de mayor grado de r se convierte en 0 al realizar la operación r−b·TD(r) TD(b). Como hemos definido el grado de un polinomio como un número natural, por la buena ordenación de los naturales no puede existir una secuencia infinita de grados de restrictamente decrecientes, por lo que en algún momento se deberá salir del bucle. Una propiedad muy importante de la división en K[x]es que el cociente y el resto son únicos, sin importar el algoritmo que se use para realizar la división. Teorema IV.10. Sean a, b = 0 ∈K[x], entonces, existen qyren K[x]tal que a=b·q+ry o bien r= 0 o bien deg(r)< deg(b). Además, esta descomposición es única. Demostración. Hemos demostrado la existencia en el teorema IV.9, estudiemos ahora la unicidad de la descomposición. Supongamos que no es única, por lo que a=b·q+r=b·q′+r′con ry r′satisfaciendo la desigualdad del grado. Sacando factor común, b(q−q′) = r′−r. Como b= 0, si r=r′, entonces q=q′y hemos terminado. Supongamos que r=r′, por lo que q−q′= 0 y deg(r′−r)<deg(b)por la desigualdad del grado de los restos de la división. Sin embargo, deg(r−r′) = deg(b(q−q′)) = deg(b) + deg(q−q′)≥deg(b) por lo que llegamos a una contradicción, y r=r′yq=q′. Orden monomial Hemos visto que una parte importante del algoritmo de la división en polinomios de una variable es el concepto de grado y el concepto de coeficiente director, que lleva implícito un orden entre monomios. Por tanto, para generalizar el algoritmo de la división a polinomios de varias variables, primero necesitaremos generalizar el concepto de grado y el concepto de orden entre monomios. Definición IV.11. (Monomio) Un monomio en K[x1, . . . , xn]es un producto de variables x1, x2, . . . , xnelevados a exponentes α1, α2, . . . , αn∈N0, es decir, el término xα1 1xα2 2· · · xαn n. Por notación, si denotamos la tupla α= (α1, α2, . . . , αn)∈Nn 0, definimos el monomio xα. .= xα1 1xα2 2· · · xαn n. Tal y como hemos visto en la definición IV.11, podemos hacer una biyección entre los monomios y las tuplas de N0, lo que nos será muy útil para definir órdenes entre monomios. Definiremos la suma entre tuplas de N0como la suma elemento a elemento. Una propiedad muy deseable en el orden de monomios será que se respeten las operaciones del anillo de los polinomios. La suma de monomios no es un monomio, por lo que no podremos compararlos directamente. La multiplicación de dos monomios sí que es un monomio, por lo que sería interesante que si xα> xβ, entonces xα+γ=xα·xγ> xβ·xγ=xβ+γ. Finalmente, nos gustaría que el orden fuese un buen orden, propiedad que utilizamos para demostrar la terminación de la división en K[x]. Estamos listos para la definición formal. Definición IV.12. (Orden total) Siendo S=∅, diremos que ≥es una relación de orden total si satisface las siguientes propiedades: 1. Reflexiva: Para todo e∈S,e≥e. IV. Métodos algebraicos 20 2. Antisimétrica: Para todo x, y ∈S,x≥y∧y≥x=⇒x=y. 3. Transitiva: Para todo x, y, z ∈S,x≥y∧y≥z=⇒x≥z. 4. Total: Para todo x, y ∈S, o bien x≥yo bien y≥x. Nótese que una relación de orden ≥induce una relación de orden >y viceversa, donde x > y⇐⇒ x≥y∧x=y. Dada la biyección vista entre los monomios y Nn 0, podemos identificar los órdenes entre monomios y los órdenes entre tuplas de Nn 0. Definición IV.13. (Orden monomial) Un orden monomial <es una relación de orden en Nn 0(definiendo por tanto una relación de orden entre monomios) que cumple las siguientes propiedades: 1. ≤es un orden total. 2. ∀α, β, γ ∈Nn 0, si α > β, entonces α+γ > β +γ. 3. Nn 0es un conjunto bien ordenado con <, es decir, ∀S=∅ ⊆ Nn 0, entonces ∃m∈Stal que para todo e∈S, m ≤e. Vamos a demostrar ahora un lema que utilizaremos para caracterizar los buenos órdenes. Lema IV.14. Un orden total ≤en un conjunto Ses un buen orden si y solo si toda sucesión (an)donde an∈Sya0> a1> a2>· · · termina, es decir, es finita. Demostración. ⇒Supongamos que la sucesión (an)no termina, es decir, es infinita. Sea A={an} =∅. El conjunto Ano es vacío y no tiene elemento mínimo, por lo que llegamos a una contradicción. ⇐Si <no es un buen orden, existe un conjunto A=∅ ⊆ Sque no tiene elemento mínimo. Elegimos a0∈A. Como Ano tiene elemento mínimo, en concreto a0no es un elemento mínimo, por lo que ∃a1∈Atal que a0> a1. Repitiendo esta construcción hallamos una secuencia infinita a0> a1> a2>· · · . Ejemplo IV.15. (Orden lexicográfico) Sea α, β ∈Nn 0. Diremos que α >lex βsi el primer elemento no nulo del vector α−βes positivo. Este orden en Nn 0induce un orden monomial en K[x1, . . . , xn]. Demostración. Veamos que >lex satisface todas las propiedades de la definición IV.13. 1. Que >lex es un orden total en Nn 0se deduce de que >es un orden total en N0. 2. Esta propiedad se deduce de que (α+γ)−(β+γ) = α−β, por lo que el primer elemento no nulo de un vector será positivo si y solo si lo es del otro, y por tanto si α >lex β, tendremos que α+γ >lex β+γ. 3. Por el lema IV.14 basta con comprobar que no existe ninguna sucesión de desigualdades a0>lex a1>lex · · · . Como N0es un conjunto bien ordenado con >, cada una de las dimensiones del vector debe estabilizarse en algún momento, no pueden descender infinitamente. Como N0tiene únicamente ndimensiones, un número finito de dimensiones, la sucesión no puede continuar de forma infinita, sino que tiene que parar en algún momento. IV. Métodos algebraicos 27 de la tercera suma también tienen multigrado estrictamente menor que α, y hemos asumido que multideg(g)< α, por lo que la primera suma tiene también multigrado estrictamente menor que α. Sin embargo, cada uno de los sumandos TD(hi)fitiene multigrado exactamente α, por lo que estamos en las condiciones de la proposición IV.31, y podemos expresar la primera suma como X multideg(hifi)=α TD(hi)fi=X i,j ci,jS(TD(hi)fi,TD(hj)fj) con ci,j ∈K. Vamos a intentar expresar S(TD(hi)fi,TD(hj)fj)en términos de S(fi, fj). En primer lugar notamos que como multideg(hifi) = α, entonces MD(TD(hk)fk) = xα para k∈ {i, j}. Por tanto, S(TD(hi)fi,TD(hj)fj) = xα TD(TD(hi)fi)TD(hi)fi−xα TD(TD(hj)fj)TD(hj)fj(IV.2) Observamos que TD(TD(hk)fk) = TD(hk) TD(fk), por lo que 1 TD(fk)=TD(hk) TD(TD(hk)fk)para k∈ {i, j}. Llamando xβi,j = mcm(MD(fi),MD(fj)), multiplicando y dividiendo en IV.2 por xβi,k obtenemos S(TD(hi)fi,TD(hj)fj) = xα−βi,j xβi,j TD(hi) TD(TD(hi)fi)fi−xβi,j TD(hj) TD(TD(hj)fj)fj =xα−βi,j S(fi, fj) Como el resto de dividir S(fi, fj)entre Bes 0, el algoritmo 2de división nos proporciona unos cocientes qktal que S(fi, fj) = Pm k=1 qkfk. Además, tal y como vimos en el teorema IV.18, se cumple que multideg(qkfk)≤multideg(S(fi, fj)) para todos los qkfk= 0. Multiplicando por xα−βi,j obtenemos que multideg(xα−βi,j qkfk)≤multideg(xα−βi,j S(fi, fj)) Por la proposición IV.30 tenemos que TD(S(fi, fj)) <mcm (MD(fi),MD(fj)) = βi,j por lo que multideg(xα−βi,j qkfk)≤multideg(xα−βi,j S(fi, fj)) < α, lo que significa que podemos reescribir la primera suma de IV.1 como X multideg(hifi)=α TD(hi)fi=X i,j m X k=1 ci,kxα−βi,j qkfk donde cada término tiene multigrado estrictamente menor que αy es una combinación lineal de fk. Esto contradice la minimalidad de α, terminando la demostración. IV.4. Algoritmo de Buchberger La principal aplicación del criterio de Buchberger, demostrado en el teorema IV.32 es la creación de un algoritmo para hallar una base de Gröbner a partir de una base de un ideal, tal y como se puede ver en el algoritmo 3. Notación IV.33. Sea S= (b1, . . . , bm)ya, donde a, b1, . . . , bm∈K[x1, . . . , xn], entonces denotamos resto(a, S)como el resto producido por el algoritmo 2de división. IV. Métodos algebraicos 28 Algoritmo 3 Algoritmo de Buchberger Entrada: {f1, . . . , fm} ⊆ K[x1, . . . , xm]con fi= 0 Salida: Base de Gröbner Bdel ideal I=⟨f1, . . . , fm⟩ B ← [f1, . . . , fm]▷Vector I← {(i, j):1≤i<j≤m}▷ I representa el conjunto de índices de S(fi, fj)a probar. k←m ▷ k es el tamaño del vector B while S=∅do Elegir (i, j)∈S I←I\ {(i, j)} (fi, fj)←(B[i],B[j]) ▷ fies el elemento i-ésimo de B. r←resto (S(fi, fj),B) if r= 0 then k←k+ 1 B.append(r)▷Añadir ral final del vector B I←I∪ {(i, k):1≤i≤k−1} end if end while Comencemos demostrando la corrección del algoritmo, ya que la terminación es un poco más delicada. Teorema IV.34. (Corrección del algoritmo de Buchberger) Si el algoritmo 3termina, entonces el resultado Bes una base de Gröbner del ideal I=⟨f1, . . . , fm⟩. Demostración. Sea B={g1, . . . , gs}al finalizar el algoritmo. Veamos primero que B ⊆ I, que es trivialmente cierto al comienzo, pues f1, . . . , fm∈Iy lo es en cada paso, pues al expandir Bañadimos el resto rde dividir S(gi, gj)entre B′⊆I, siendo B′el valor intermedio de Bal principio de la iteración. Como gi, gj∈ B′⊆I, entonces S(gi, gj)∈I. Como el divisor y los dividendos están en I, podemos expresar el resto como combinación lineal de ellos, y por tanto r∈I, y B ⊆ I. Además, {f1, . . . , fm} ⊆ B y es una base de I, por lo que Btambién será una base de I. Veamos que al terminar el bucle while tenemos que resto(S(gi, gj),B) = 0 para todo i=j, por lo que aplicando el teorema IV.32 estaría demostrado que Bes una base de Gröbner. Notemos primero que si resto(S(gi, gj),B)=0y expandimos BaB′añadiendo elementos al final de la tupla, entonces resto(S(gi, gj),B′) = 0, pues en el bucle for del algoritmo 2de la división comprobaremos primero los polinomios de B, y en el mismo orden y como el resto era 0, en toda iteración se producía una división, por lo que se sale del bucle for mediante la instrucción break antes de que los nuevos polinomios añadidos a la base puedan afectar al resultado. Notamos también que S(gj, gi) = −S(gi, gj), por la construcción de los polinomios-S. Además, si resto(S(gi, gj),B) = 0, entonces también tendremos que resto(−S(gi, gj),B) = 0, pues la única decisión que afecta al resto es si el término director de algún gidivide al término director del dividendo, y al trabajar en un cuerpo K, los coeficientes no afectan a la divisibilidad de los términos, que está únicamente determinada por los monomios. Por tanto, basta con demostrar que resto(S(gi, gj),B′) = 0 para el B′de alguna iteración y para i<j. En primer lugar, entramos al bucle con cada (i, j)en esas condiciones, pues inicializamos IV. Métodos algebraicos 29 Scon todas las tuplas requeridas, y al añadir un elemento al final de S, añadimos todas las tuplas requeridas con los elementos anteriores. Además, al final de cada iteración del bucle nos aseguramos que resto(S(gi, gj),B′) = 0, donde B′es la tupla Bal finalizar esa iteración. Si r= 0, claramente se cumple. Si no es 0, estamos añadiendo el resto de la división a B′, por lo que el resto de la nueva división entre S(gi, gj)yB′sí será 0. La clave para demostrar la terminación del algoritmo está en comprobar que si el algoritmo no termina tendríamos una cadena infinita de inclusiones estrictas de ideales. Para demostrar que esto es imposible, es necesario utilizar el teorema de la base de Hilbert y que el anillo K[x1, . . . , xn]es Noetheriano. Una demostración puede hallarse en el apéndice B. Teorema IV.35. (Terminación del algoritmo de Buchberger) El algoritmo 3termina en tiempo finito. Demostración. Supongamos que el algoritmo no termina en tiempo finito. Eso significa que debemos añadir infinitas veces elementos al conjunto S, lo que significa que debemos añadir infinitas veces el resto ra la base B. Podemos definir una cadena de inclusiones de conjuntos B1⊊B2⊊B3⊊· · · Cada uno de los Bi+1 se forma añadiendo a Biel resto de una división entre Bi. Viendo el algoritmo 2, notamos que si el resto es no nulo es porque el monomio director de ningún divisor divide al monomio director del dividendo, que pasa a añadirse al resto. En concreto, el monomio director del resto no es dividido por el monomio director de ningún dividendo. Por el lema IV.24, esto significa que si Bi={g1, . . . , gm}, entonces el resto rde cualquier división entre Bi satisfará que TD(r)∈ ⟨TD(Bi)⟩. .=⟨TD(g1),...,TD(gm)⟩. Como Bi+1 =Bi∪ {r}, esto significa que TD(Bi)⊊TD(Bi+1). Como el algoritmo no termina, esto sucede infinitas veces, generando la cadena ascendente de ideales TD(B1)⊊TD(B2)⊊TD(B3)⊊· · · lo cual entra en contradicción con que K[x1, . . . , xn]sea Noetheriano por el corolario B.4, por lo que el algoritmo debe terminar en tiempo finito. Observación IV.36. (Complejidad computacional) Aún usando los algoritmos más eficientes para computar bases de Gröbner que se conocen en la actualidad (los algoritmos F4 y F5 de Faugère [11,12], que son bastante más eficientes que el algoritmo 3) los grados y coeficientes de los polinomios intermedios pueden explotar, requiriendo cantidades excesivas de tiempo y memoria. De hecho, se ha demostrado que al computar la base de Gröbner para un ideal cuyos polinomios todos tienen grado igual o menor que d, es posible que aparezcan polinomios intermedios de grado proporcional a 22d[21], es decir, crecimiento doblemente exponencial. El número de variables también es un factor crítico. Por lo tanto, en la práctica, las bases de Gröbner son útiles para un número reducido de polinomios de grado reducido. En el capítulo Vveremos como evitar parcialmente estas restricciones y poder garantizar la seguridad de circuitos grandes. Cap´ ıtulo V Algoritmo modular En este capítulo desarrollamos un algoritmo modular para demostrar la seguridad de circuitos Circom grandes, combinando heurísticas con los métodos algebraicos del capítulo IV. V.1. Motivación para un algoritmo modular En el capítulo III estudiamos como convertir el problema de la verificación de circuitos Circom (consistente en demostrar que para las entradas dadas existen unos únicos valores para las salidas que puedan ser solución del sistema R1CS) a un problema de insatisfacibilidad de un sistema polinómico. En el capítulo IV vimos un algoritmo no completo para verificar la insatisfacibilidad de un sistema polinómico. Sin embargo, también vimos en la observación IV.36 que la complejidad de decidir la insatisfacibilidad puede crecer muy rápidamente con el número de variables, grado de los polinomios y número de restricciones. Por tanto, aunque para demostrar la seguridad de un circuito podríamos hallar su sistema R1CS, añadir el polinomio de prohibición del teorema III.8 y decidir la satisfacibilidad utilizando bases de Gröbner, la aplicabilidad de ese método estaría limitada a los circuitos más pequeños. En lugar de eso, vamos a desarrollar un algoritmo modular que demuestre por separado propiedades de seguridad para subcomponentes más pequeños utilizando las bases de Gröbner y después una inductivamente dichas demostraciones de los subcomponentes para demostrar la seguridad del circuito completo. Para ello, este algoritmo tendrá la siguiente filosofía: Aplicabilidad práctica: El objetivo no es obtener un algoritmo completo, sino un algoritmo que utilice heurísticas basadas en las particularidades de los sistemas que aparecen en los circuitos Circom prácticos para poder demostrar la mayoría de ellos de forma eficiente. Esto significa sacrificar completitud, que con los métodos que hemos presentado es computacionalmente infactible. Seguridad: Nos vamos a centrar en demostrar la seguridad (no seguridad fuerte) para una única entrada dada. Eso significa que nuestro algoritmo recibirá el circuito Circom y un testigo y garantizará que la salida del componente principal es única (está fija) para la entrada recibida. Vamos a demostrar únicamente la seguridad para una entrada dada debido al número de optimizaciones agresivas que podemos realizar, con el objetivo de poder verificar circuitos grandes. Una vez hemos demostrado que cierta señal está fija, podemos sustituir las apariciones de dicha señal por su valor, simplificando en muchos casos el problema de forma notable. Modularidad: Vamos a intentar reducir al máximo posible el tamaño de los sistemas de 30 V. Algoritmo modular 31 ecuaciones a los que aplicamos el método de las bases de Gröbner. En concreto, al tratar un componente, vamos a asumir que cada subcomponente suyo es seguro y repetiremos el proceso para todos los subcomponentes para demostrar la seguridad modularmente. En el componente padre, cada subcomponente se tratará como una caja negra segura, y luego verificaremos por separado cada subcomponente con el mismo algoritmo para verificar que efectivamente es seguro. Esta asunción suele funcionar en los circuitos reales y nos permite dividir la verificación de seguridad en subproblemas más manejables, sacrificando completitud por eficiencia. V.2. Grafo de verificación El algoritmo modular trabaja sobre un grafo que representa el circuito Circom. Este grafo es la entrada del algoritmo. Dos ejemplos de grafos de verificación se pueden ver en la figura V.1. adder: Adder() o a <== b === c adder.b <== adder.o adder.a b2n: Bits2Num(2) n2bb: Num2Bits(2)n2ba: Num2Bits(2) sub: BinSub(2) out a n2ba.in <== b n2bb.in <== b2n.out <== b2n.in[0] b2n.in[1] n2ba.out[0] n2ba.out[1] sub.in[0][0] <== sub.in[0][1] <== n2bb.out[0] n2bb.out[1] sub.in[1][0] <== sub.in[1][1] <== sub.out[0] sub.out[1] <== <== Figura V.1: Dos ejemplos de grafos de verificación Los grafos de la figura V.1 han sido creados automáticamente a partir de un circuito Circom por una herramienta escrita en Rust [6] con el propósito de ayudar a la depuración. También puede mostrar estados intermedios del grafo de verificación en distintas etapas del algoritmo. Definición V.1. (Grafo de verificación) Llamaremos grafo de verificación de un componente a un conjunto de tres hipergrafos distintos (grafos cuyas aristas pueden relacionar cualquier número de vértices). V. Algoritmo modular 32 Todos los hipergrafos tienen el mismo conjunto de vértices, que son las señales del componente que se está verificando que pueden ser o bien entradas, salidas, señales intermedias, señales de entrada de un subcomponente o señales de salida de un subcomponente. Nótese que las señales intermedias de cada subcomponente no están representadas en el grafo de verificación del componente padre, lo estarán en el grafo de verificación del subcomponente. Cada hipergrafo tiene un conjunto de aristas diferente. El primero de ellos consiste en las aristas dirigidas de las asignaciones duales <==. Existe una arista por cada una de dichas asignaciones. El conjunto de vértices “cabeza” son las señales que aparecen en el lado derecho de la asignación <== y el único vértice “cola” es la señal asignada. El segundo consiste en las aristas no dirigidas formadas por las restricciones de igualdad ===. El conjunto de vértices relacionados por cada restricción de igualdad son las señales que aparecen en dicha restricción. El tercer tipo de aristas consiste en las aristas dirigidas formadas por los diferentes subcomponentes. Existe una arista por subcomponente instanciado. El conjunto de vértices cabeza de cada arista son las entradas del subcomponente y el conjunto de vértices cola las salidas del subcomponente. Podemos interpretar este conjunto de tres hipergrafos como un gran único hipergrafo en el que hay tres tipos diferentes de aristas, dos dirigidos y uno no dirigido. El algoritmo irá modificando este grafo eliminando los nodos que ya hayan sido fijados (de los que se haya demostrado unicidad). El objetivo es eliminar del grafo todas las salidas, y así habremos logrado fijar su valor para cierta entrada dada y demostrar la seguridad del circuito para dicha entrada. Una vez demostremos la unicidad de una señal, podemos sustituir la señal por su valor en el testigo computado por el programa WebAssembly (pues sabemos que es una solución válida, y como es única, es forzosamente esa) y propagarla para así demostrar la unicidad de más señales. Además del grafo de verificación, mantendremos también una lista de nodos fijados que todavía no han sido procesados y eliminados del grafo, una lista de subcomponentes para verificar (pues verificaremos la seguridad de cada subcomponente independientemente, y la seguridad del componente padre estará condicionada a la seguridad de sus subcomponentes) y una lista de sistemas polinómicos para los que demostrar la unicidad de ciertas variables utilizando el teorema III.8 y las técnicas del capítulo IV basadas en bases de Gröbner. Intentaremos que el tamaño de cada uno de los sistemas polinómicos sea lo más reducido posible. V.3. Algoritmo El primer paso es, dado el grafo de verificación de cierto componente de entrada, determinar qué nodos están inicialmente fijos y añadirlos a la lista de nodos fijados. Son los siguientes: Las señales de entrada, pues queremos verificar que las salidas se fijen para una entrada determinada fija. Las señales objeto de una asignación <== en el que el lado derecho es constante. Después de fijar el lado izquierdo, eliminamos dicha asignación. Las señales que sean la única señal de una restricción === lineal donde el resto de elementos son constantes y el coeficiente asociado a dicha señal es no nulo. Después de fijar la señal, borramos la restricción. V. Algoritmo modular 33 Las salidas de subcomponentes que no tienen entradas (componentes cuya función es devolver una constante). Además, añadimos dicho subcomponente a la lista de componentes a demostrar recursivamente. Una vez tenemos las señales iniciales fijas, utilizamos el algoritmo 4para propagarlas. Algoritmo 4 Propagación de señales fijadas Entrada: Ggrafo de verificación, xseñal fijada, wtestigo del circuito Salida: Fconjunto de valores a fijar, Clista de subcomponentes a verificar F← ∅ C← ∅ for all ain G.asignaciones_duales tal que x∈a.rhs do ▷Asignaciones <== a.sustituir_señal(x→w[x])▷Sustituimos el valor constante del testigo de la señal if a.rhs es constante then F←F∪ {a.lhs}▷Fijamos la señal asignada G.eliminar_asignacion_dual(a) end if end for for all rin G.restricciones tal que x∈rdo ▷Restricciones === r.sustituir_señal(x→w[x])▷Sustituimos el valor constante del testigo de la señal if res lineal y contiene una única señal sy su coeficiente es no nulo then F←F∪ {s}▷Fijamos la señal de la restricción G.eliminar_restriccion(r) end if end for if ∃c∈ G.componentes tal que x∈c.inputs then c.inputs ←c.inputs \ {x} if c.inputs =∅then ▷Todas las entradas han sido fijadas F←F∪c.outputs ▷ Fijamos todas las salidas C←C∪ {c} G.eliminar_componente(c) end if end if F←F∩ G.nodos ▷ Nos quedamos con los nodos que no hayan sido fijados previamente G.eliminar_nodo(x)▷Borra toda referencia a la señal, como la pertenencia a componentes Teorema V.2. El algoritmo 4es correcto. Demostración. En el caso de las asignaciones <==, si tras sustituir el nuevo valor fijado (que podemos hacer por haber demostrado que ese valor es fijo) el lado derecho de la asignación es constante, entonces el lado izquierdo también será fijo (y será igual a su valor computado en el testigo), pues es la única solución a la restricción generada por Circom. Lo mismo sucede si tras sustituir el valor fijado, una señal ses la única en una restricción ===, esta es lineal y el coeficiente asociado ces no nulo. Es decir, la restricción se puede expresar como cs =apara c, a ∈Fpfijos. Como c= 0, s =c−1a, quedando el valor de sfijo. Finalmente, debido a la heurística que estamos usando, sacrificando completitud en pos de ganar eficiencia práctica, asumimos que todos los subcomponentes son seguros. Entonces, si todas las entradas de un subcomponente han sido fijadas, las salidas también lo estarán. Añadimos dicho subcomponente a una lista de V. Algoritmo modular 34 componentes a verificar recursivamente, para posteriormente verificar que efectivamente dicho componente es seguro. Después de propagar iterativamente los valores fijados hasta que no quede ningún valor fijo es posible que ya hayamos fijado todas las salidas del componente, en cuyo caso hemos terminado la demostración y el componente es seguro (condicionado a la seguridad de los subcomponentes). Sin embargo también es posible que no hayamos fijado todas las salidas pero que haya varias señales conectadas por restricciones === que formen un sistema polinómico que garantice la unicidad de algunas de sus señales. Podemos demostrar la unicidad de esas señales usando bases de Gröbner y después sustituir dichas señales por sus valores en el testigo. Si incluimos una entrada o salida de un subcomponente en cierta componente conexa de restricciones ===, incluiremos todas las entradas y salidas de dicho subcomponente, por simplicidad al generar el sistema polinómico del que demostraremos la unicidad de ciertas variables utilizando las herramientas algebraicas del capítulo IV. El algoritmo que computa una componente conexa es el algoritmo 5que añade recursivamente elementos a una componente conexa utilizando una búsqueda en profundidad (DFS). Algoritmo 5 Creación de componente conexa Entrada: Ggrafo de verificación, Sconjunto de la componente conexa, xseñal a visitar Salida: Nueva componente conexa, posiblemente ampliada function DFS(G,S,x) if x∈Sthen return S end if S←S∪ {x} for all rin G.restricciones tal que x∈rdo ▷Restricciones === for all yin r.se˜nales tal que y=xdo S←S∪DFS(G,S,y) end for end for if ∃ccomponente tal que x∈c.inputs ∪c.outputs then for all yin c.inputs ∪c.outputs do S←S∪DFS(G,S,y) end for end if return S end function Dada una componente conexa, podemos generar un sistema polinómico para demostrar la unicidad de ciertas señales de dicha componente conexa usando bases de Gröbner, para poder después sustituir las señales por sus valores en el testigo. El método de las bases de Gröbner necesita como entrada un conjunto de ecuaciones polinómicas y una lista de señales de las que demostrar la unicidad, junto con sus valores en el testigo (para generar la restricción de prohibición vista en el teorema III.8). El conjunto de ecuaciones polinómicas es el formado por las restricciones === y las asignaciones V. Algoritmo modular 35 <== entre señales de la componente conexa. También debemos marcar un conjunto de señales para las que demostrar la unicidad (fijar) utilizando bases de Gröbner. Las salidas del componente principal serán unas de esas señales, pues son el objetivo principal. También marcaremos como variables a fijar aquellas que formen parte del lado derecho de una asignación <== que salga fuera de la componente conexa. El algoritmo 6calcula esos datos para una componente conexa dada, que se pueden utilizar junto al teorema III.8 y los algoritmos vistos en el capítulo IV para demostrar la unicidad del conjunto de señales marcadas a fijar y luego sustituir las señales por sus valores en el testigo. Algoritmo 6 Sistema polinómico para una componente conexa Entrada: Ggrafo de verificación, Scomponente conexa, wtestigo Salida: Cconjunto de ecuaciones, Fconjunto de señales a fijar C← ∅ for all rin G.restricciones tal que r.se˜nales ⊆Sdo ▷Restricciones === C←C∪ {r} end for for all ain G.asignaciones_duales tal que a.se˜nales ⊆Sdo ▷Asignaciones <== C←C∪ {a.lhs −a.rhs = 0} end for for all cin G.componentes tal que c.inputs ∪c.outputs ⊆Sdo C←C∪c.expandir_R1CS() ▷Añadimos las ecuaciones del R1CS del subcomponente end for F←S∩ G.outputs ▷ Marcamos las salidas del componente principal como señales a fijar F←F∪ {x∈S:∃a∈ G.restricciones tal que x∈a.rhs ∧a.lhs ∈ S} Es posible que haya más de una componente conexa de restricciones === y que algunas dependan de otras por asignaciones <==, así que debemos establecer alguna heurística para elegir qué componente conexa será tratada primero usando bases de Gröbner. Primero, calcularemos todas las posibles componentes conexas de restricciones ===. Si existe alguna componente conexa que no tenga ninguna asignación <== entrante desde fuera, entonces la tratamos con bases de Gröbner. Si no existe ninguna, escogemos alguna asignación <== que no satisfaga la condición y combinamos todas las componentes conexas de las señales participantes en la asignación en una sola, repitiendo este proceso varias veces si es necesario. Ahora estamos en condiciones de estudiar el algoritmo completo de verificación modular, cuyo pseudocódigo puede verse en el algoritmo 7. Hay que recordar que este algoritmo no es completo, hemos utilizado algunas heurísticas a cambio de poder tratar circuitos grandes. Sin embargo, sí que es correcto, como podemos ver en el teorema V.3. Teorema V.3. (Corrección del algoritmo modular). El algoritmo 7termina y es correcto. Demostración. Veamos primero que el algoritmo termina. Al comienzo de cada iteración del bucle principal propagamos los nodos fijados y en concreto eliminamos del grafo Gtodos los nodos fijados. Es por tanto suficiente con demostrar que en cada iteración que no terminemos o bien borraremos al menos un nodo de Go que al menos se marcará un elemento como fijado para demostrar que el algoritmo termina (pues al grafo Gnunca se añaden nodos). Si G.outputs = ∅, hemos acabado. Si hay alguna salida pero no hay ninguna restricción ===, también hemos acabado. En caso de que sí que haya alguna restricción ===, entonces extendemos la componente V. Algoritmo modular 36 Algoritmo 7 Verificación modular Entrada: Ggrafo de verificación, wtestigo Salida: Resultado de la verificación Inicializar Fel conjunto de nodos fijados y Cconjunto de subcomponentes a verificar como se describió al principio de la sección while true do while F=∅do Elegir x∈F (F′, C′)←propagar_señal_fijada(G, x, w)▷Algoritmo 4 F←(F∪F′)\ {x} C←C∪C′ end while if G.outputs =∅then ▷Todas las salidas han sido fijadas Verificar recursivamente los subcomponentes de la lista C if Todos los subcomponentes son seguros then return “El componente es seguro” end if else ▷Hay al menos una salida sin fijar después de la propagación if G.restricciones =∅then ▷Hay alguna restricción === A← G.se˜nales ▷ Nodos sin componente conexa todavía B← ∅ ▷Conjunto de componentes conexas while A=∅do Elegir x∈A S←DFS(G,∅, x)▷Algoritmo 5 A←A\S B←B∪ {A} end while while true do ▷Hasta tener una componente conexa suficientemente grande if ∃CC ∈Btal que ∄asignación <== entrante desde otra c.c. then Creamos un sistema polinómico a fijar para CC según el algoritmo 6 Añadimos al sistema polinómico el polinomio prohibición (definición III.7) para las señales a fijar y sus valores en el testigo w if El sistema no tiene ninguna solución utilizando bases de Gröbner then Borrar de Gtodos los nodos de CC no fijados Añadir a Flos nodos fijados de CC break else return “El componente es posiblemente inseguro” end if else Elegir una asignación dual aque no satisfaga la condición Combinar todas las componentes conexas de a.lhs ya.rhs en una sola end if end while else ▷No hay ninguna restricción === que pueda fijar la salida return “El componente es posiblemente inseguro” end if end if end while [16] Groth, J. (2010). Short Non-interactive Zero-Knowledge Proofs. [17] Groth, J. (2016). On the Size of Pairing-Based Non-interactive Arguments. [18] Haas, A., Rossberg, A., Schuff, D. L., Titzer, B. L., Holman, M., Gohman, D., Wagner, L., Zakai, A., and Bastien, J. (2017). Bringing the web up to speed with WebAssembly. pages 185–200. ACM. [19] Iden3. JavaScript and Pure Web Assembly implementation of zkSNARK and PLONK schemes. URL: https://github.com/iden3/snarkjs (8/6/2023). [20] Koe, Alonso, K. M., and Noether, S. (2020). Zero to Monero. [21] Mayr, E. W. and Meyer, A. R. (1982). The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics, 46:305–329. [22] Morais, E., van Wijk, C., and Koens, T. (2018). Zero Knowledge Set Membership. [23] Moura, L. D. and Bjørner, N. (2011). Satisfiability Modulo Theories: Introduction and Applications. Communications of the ACM, 54:69–77. [24] Shpilka, A. and Yehudayoff, A. (2009). Arithmetic Circuits: A survey of recent results and open questions. Foundations and Trends®in Theoretical Computer Science, 5:207–388. [25] Tikhomirov, S. (2018). Ethereum: State of Knowledge and Research Perspectives. [26] Vujicic, D., Jagodic, D., and Randic, S. (2018). Blockchain technology, bitcoin, and Ethereum: A brief overview. pages 1–6. IEEE. [27] Wang, S., Yuan, Y., Wang, X., Li, J., Qin, R., and Wang, F.-Y. (2018). An Overview of Smart Contract: Architecture, Applications, and Future Trends. pages 108–113. IEEE. [28] Wohrer, M. and Zdun, U. (2018). Smart contracts: security patterns in the ethereum ecosystem and solidity. pages 2–8. IEEE. 43 Ap´ endice A Código fuente El algoritmo modular descrito en el capítulo Vha sido implementado en el lenguaje de programación Rust. Este lenguaje ha sido escogido por ser el lenguaje en el que el compilador Circom está escrito, lo que permite una gran interoperabilidad. También ha sido escogido por sus grandes garantías de seguridad, así como ser un lenguaje lo suficientemente eficiente para gestionar grandes volúmenes de datos. El código Rust genera sistemas polinómicos para los que se debe demostrar su insatisfacibilidad, tal y como vimos en el capítulo IV. Para demostrar la insatisfacibilidad, se crean archivos en el programa de álgebra computacional CoCoA [8], que se comunica con el código en Rust. El código fuente del algoritmo modular puede encontrarse en el siguiente repositorio de GitHub: https://github.com/palmenros/zksnark-safety-verificator. 44 Ap´ endice B Teorema de la base de Hilbert En este apéndice se estudia una demostración del teorema de la base de Hilbert y un corolario que garantiza que los anillos de polinomios en varias variables K[x1, . . . , xn]son Noetherianos. Esto es necesario para demostrar la terminación del algoritmo 3de Buchberger para hallar una base de Gröbner, vista en el teorema IV.35. Comencemos definiendo el concepto de anillo Noetheriano. Definición B.1. (Anillo Noetheriano). Sea Aun anillo conmutativo. Diremos que Aes Noetheriano si satisface la condición de la cadena ascendente, es decir, si toda cadena numerable de inclusión de ideales I1⊆I2⊆I3⊆. . . se acaba estabilizando, es decir, ∃n≥1tal que ∀m≥n, Im=In. Proposición B.2. Sea Aun anillo conmutativo. Entonces Aes Noetheriano si y solo si todo ideal de Aes finitamente generado. Demostración. ⇒Supongamos por contradicción que existe un ideal Ide Aque no es finitamente generado. Elegimos f1∈ A, y como no es finitamente generado, ⟨f1⟩⊊A. Supongamos que tenemos J=⟨f1, . . . , fn⟩⊊A. Como J=A,∃fn+1 ∈ A tal que fn+1 ∈ J. Además, como Ano es finitamente generado, ⟨f1, . . . , fn⟩⊊⟨f1, . . . , fn, fn+1⟩⊊A. Repitiendo, hallamos una cadena estrictamente ascendente ⟨f1⟩⊊⟨f1, f2⟩⊊· · · ⊊⟨f1, . . . , fn⟩⊊· · · lo que entra en contradicción con que Asea Noetheriano. ⇐Sea I1⊆I2⊆I3⊆. . . una cadena numerable de ideales. Sea I=S∞ i=1 Ii. Veamos que I es un ideal. Como 0∈I1,0∈I. Sean f, g ∈I, por lo que ∃i, j tal que f∈Ii, g ∈Ij. Sea k= m´ax {i, j}, por lo que f, g ∈Ik=⇒f+g∈Ik⊆I. Además, por ser Iiun ideal, si h∈ A, f ·h∈Ii⊆I. Por tanto, Ies un ideal, por lo que es finitamente generado. Es decir, I=⟨f1, . . . , fs⟩. Cada fi∈Iαi, sea n= m´ax {α1, . . . , αs}, entonces f1, . . . , fs∈In=I por lo que f1, . . . , fs∈Impara todo m≥ny por tanto In=I⊆Im⊆Ipor lo que Im=I=Inpara todo m≥n. La demostración aquí presentada del teorema de la base de Hilbert sigue la línea de la demostración original y de [13]. Teorema B.3. (Teorema de la base de Hilbert) Sea Aun anillo conmutativo Noetheriano, entonces el anillo A[x]es también Noetheriano. 45 Demostración. Supongamos por reducción al absurdo que existe un ideal I⊆ A[x]no finitamente generado. Escogemos f1∈I\ {0}de forma que deg(f1) = m´ın {deg(f) : f∈I\ {0}}, posible por estar N0bien ordenado. Inductivamente, si tenemos un ideal Jn=⟨f1, . . . , fn⟩podemos elegir un fn+1 ∈I\ ⟨f1, . . . , fn⟩de forma que deg(fn+1) = m´ın {deg(f) : f∈I\Jn}, por ser Ino finitamente generado, definiendo así Jn+1 =⟨f1, . . . , fn+1⟩. Por la minimalidad del grado de cada fn, tenemos que deg(fi)≤deg(fi+1)para todo i≥1. Sea an= CD(fn)∈ A y sea Ln=⟨a1, . . . , an⟩⊆A. Tenemos por tanto una cadena ⟨a1⟩⊆⟨a1, a2⟩⊆⟨a1, a2, a3⟩ · · · Por ser ANoetheriano, ∃n≥1tal que Lk=Lnpara todo k≥n. En concreto eso quiere decir que existen c1,...cn∈ A tal que an+1 =Pn i=1 ciai. Consideremos ahora el polinomio g=fn+1 − n X i=1 cixdeg(fn+1)−deg(fi)fi que está bien definido pues si 1≤i≤n, entonces deg(fi)≤deg(fn+1). Además, g∈I\Jn, pues el sumatorio de la derecha pertenece a Jn, y si g∈Jn=⇒fn+1 ∈Jn, lo cual es falso por construcción de los fi. Finalmente, por construcción, CD(fn+1) = an+1 se cancela con el sumatorio de la derecha, por lo que deg(g)<deg(fn+1), lo cual contradice la minimalidad del grado de los fi, probando que todo ideal I⊆ A[x]es finitamente generado. Corolario B.4. Si Kes un cuerpo, el anillo K[x1, . . . , xn]es Noetheriano. Demostración. En primer lugar, observemos que Kes un anillo Noetheriano. Sus dos únicos ideales son {0}yK=⟨1⟩, ambos finitamente generados. Efectivamente, sea un ideal I. Si a= 0 ∈I, entonces a·a−1= 1 ∈I=⇒ ∀b∈K, b = 1 ·b∈I. Por el teorema B.3, como Kes Noetheriano, K[x]también lo es. Aún más, como K[x1, . . . , xn]∼ = (K[x1, . . . , xn−1]) [xn]para n≥2, podemos aplicar inductivamente el teorema B.3 para demostrar que K[x1, . . . , xn]es Noetheriano. 46 Ap´ endice C Ejemplos de verificación de algunos circuitos En este apéndice se estudia la verificación de seguridad para dos circuitos concretos con aplicabilidad real que resultan en sistemas polinómicos interesantes: Num2Bits ySplit. C.1. Num2Bits Un módulo de CircomLib [2] ampliamente usado por múltiples circuitos es Num2Bits, cuya implementación puede verse en el código C.1. Código C.1 Implementación del módulo Num2Bits 1template Num2Bits (N) { 2signal input in; 3signal output out [N]; 4var lc1 =0; 5 6var e2 =1; 7for (var i = 0; i<N; i ++) { 8out[i] <-- (in >> i) & 1; 9out[i] * (out [i] -1 ) === 0; 10 lc1 += out [i] * e2; 11 e2 = e2+e2; 12 } 13 14 lc1 === in; 15 } El módulo tiene como entrada un número in de Nbits en Fpy su salida es la representación binaria de dicho número. Veamos un ejemplo para N= 4 yin = 13. Tras realizar la propagación del algoritmo V, resulta el sistema de ecuaciones                13 −out[0] −2·out[1] −4·out[2] −8·out[3] = 0 (out[0] −1) ·out[0] = 0 (out[1] −1) ·out[1] = 0 (out[2] −1) ·out[2] = 0 (out[3] −1) ·out[3] = 0 Vemos que a cada salida se le asigna una restricción que la fuerza a ser binaria (o 0 o 1), y luego tenemos una restricción que construye el número deseado (in) a partir de la salida 47 binaria. Aplicando la optimización descrita en la observación V.4, la restricción del polinomio de prohibición resulta ser (out[0] −0) ·(out[1] −1) ·(out[2] −0) ·(out[3] −0) = 0 El principal problema con el módulo Num2Bits es que es instanciado para parámetros de Nenormes, con N > 250, para luego realizar operaciones con los bits resultantes. Como comentamos en la observación IV.36, el método de cálculo de bases de Gröbner escala muy mal con el grado de los polinomios. En un tiempo razonable (menos de un minuto), solo hemos sido capaces de demostrar la seguridad de Num2Bits(N) para N≤12. Sin embargo, otras técnicas como SMT (Satisfiability Modulo Theory) pueden tener un mejor comportamiento para circuitos de este estilo. C.2. Split Otro módulo con un sistema polinómico interesante resultante al verificar su seguridad es Split en Circom-ECDSA [1]. Su implementación puede encontrarse en el código C.2. Código C.2 Implementación del módulo Split 1template Split(N, M) { 2assert(N <= 126); 3signal input in; 4signal output small ; 5signal output big ; 6 7small <-- in % (1 << N); 8big <-- in \ (1 << N); 9 10 component n2b_small = Num2Bits (N); 11 n2b_small . in <== small ; 12 component n2b_big = Num2Bits (M); 13 n2b_big . in <== big; 14 15 in === small + big * (1 << N); 16 } La función del módulo Split(N, M) es descomponer un número in ∈Fpde N+Mbits en dos números small de Nybig de Mbits tal que in =small + 2n·big. Los dos componentes Num2Bits fuerzan a que efectivamente small ybig tengan NyMbits respectivamente. Sin embargo, estos componentes fuerzan restricciones sobre las señales small ybig, por lo que no se puede demostrar la seguridad modularmente para cada subcomponente como indicamos en el capítulo VI. Para poder verificar la seguridad de este circuito, debemos tratar como un único sistema de polinomios todas las restricciones del componente y subcomponentes. Para N= 2, M = 3,in = 23, tras propagar los valores de la entrada, queda el sistema polinómico 48                                                n2b_small.in −n2b_small.out[0] −2·n2b_small.out[1] = 0 (−1 + n2b_small.out[0]) ·n2b_small.out[0] = 0 (−1 + n2b_small.out[1]) ·n2b_small.out[1] = 0 n2b_big.in −n2b_big.out[0] −2·n2b_big.out[1] −4·n2b_big.out[2] = 0 (−1 + n2b_big.out[0]) ·n2b_big.out[0] = 0 (−1 + n2b_big.out[1]) ·n2b_big.out[1] = 0 (−1 + n2b_big.out[2]) ·n2b_big.out[2] = 0 small −n2b_small.in = 0 big −n2b_big.in = 0 −23 + small + 4 ·big = 0 Las tres primeras ecuaciones corresponden al subcomponente n2b_small, y las siguientes 4 al subcomponente n2b_big. Las siguientes dos asignan a los subcomponentes Num2Bits sus entradas. La última es la restricción que realmente garantiza la salida que queremos, que es expresar 23 como small + 22·big. La restricción asociada al polinomio de prohibición es ((small −3) ·u1−1) ∗((big −5) ·u2−1) = 0 El sistema polinómico una vez añadida la restricción de prohibición es lo suficientemente pequeño para tratarlo con bases de Gröbner y demostrar que no tiene ninguna solución, por lo que la salida queda fija para dicha entrada. 49 Ap´ endice D Ejemplos de circuitos inseguros encontrados En este apéndice se estudian dos casos de circuitos inseguros detectados gracias a la herramienta desarrollada en el capítulo Vy las pruebas realizadas. D.1. Decoder El componente Decoder es parte del repositorio oficial de CircomLib [2], la librería estándar de componentes Circom. Se puede encontrar la implementación original Circom de dicho módulo en el código D.1. Código D.1 Implementación del módulo Decoder 1template Decoder (W) { 2signal input inp; 3signal output out [W]; 4signal output success; 5var lc =0; 6 7for (var i =0; i<W; i++) { 8out[i] <-- (inp == i) ? 1 : 0; 9out[i] * (inp -i) === 0; 10 lc = lc + out[i]; 11 } 12 13 lc == > success ; 14 success * ( success -1) === 0; 15 } Vemos que el módulo tiene una entrada inp ∈FpyWsalidas binarias out[i].Wes un parámetro del módulo, y se puede elegir cuantas salidas existen. También existe una salida binaria success. El funcionamiento deseado del módulo es el siguiente: si 0≤inp < W, entonces out[inp] = 1,out[i] = 0 ∀i=inp ysuccess = 1. En caso contrario, success = 0 yout[i] = 0 ∀i. Intuitivamente, se pone el elemento de out en la posición inp a 1 si existe y el resto a 0. Si el elemento existe, entonces success = 1 y si no, success = 0. Podemos ver que el testigo que computa el circuito mediante las asignaciones inseguras <-- es el descrito por el comportamiento anterior. Sin embargo, ese comportamiento no es forzado al sistema de restricciones R1CS asociado, que también permite la alternativa de fallar con success = 0 aún sí inp está en un rango válido. Veamos un ejemplo con W= 3 einp = 2. El sistema R1CS generado por Circom es 50                inp ·out[0] = 0 (inp −1) ·out[1] = 0 (inp −2) ·out[2] = 0 (success −1) ·success = 0 out[0] + out[1] + out[2] −success = 0 Vemos que efectivamente la solución computada por el testigo de Circom es válida (inp = 2,out = [0,0,1],success = 1) pero la solución alternativa inp = 2,out = [0,0,0],success = 0 también satisface el sistema, por lo que el módulo no es seguro. Nuestro algoritmo modular descrito en el capítulo Vmarcó que este módulo no era seguro. Tras ejecutar la propagación descrita dicho capítulo, el sistema de ecuaciones resultante tras añadir el polinomio prohibición es:      out[2] −success = 0 (success −1) ·success = 0 ((out[2] −1) ·u3−1) ·(success −0) = 0 Vemos que este sistema no es insatisfacible, pues success = 0,out[2] = 0, u3=−1es una solución. D.2. FullAdder El subcomponente fulladder es parte del repositorio ED25519-Circom [4], y se usa como subcomponente de un sumador binario. Su implementación se puede encontrar en el código D.2. Código D.2 Implementación del módulo fulladder 1template fulladder () { 2signal input bit1; 3signal input bit2; 4signal input carry ; 5 6signal output val ; 7signal output carry_out ; 8 9val <-- ( bit1 + bit2 + carry) % 2; 10 val * (val - 1) === 0; 11 carry_out <-- ( bit1 + bit2 + carry) \ 2; 12 carry_out * ( carry_out - 1) === 0; 13 } Podemos ver que el problema es que a val únicamente se asigna con una asignación insegura <--, que solamente genera dicha asignación en el código WebAssembly para generar el testigo, pero no genera una restricción equivalente en el sistema de restricciones R1CS. 51 Esto significa que el sistema de ecuaciones para este subcomponente es: (val ·(val −1) = 0 carry_out ·(carry_out −1) = 0 La única restricción que impone ese sistema es que ambas salidas val ycarry_out sean binarias, pero pueden tomar cualquier valor, y no tienen ninguna relación con las entradas. Olvidar restricciones debido al uso erróneo de asignaciones inseguras <-- es algo común tanto en el repositorio ED25519-Circom como en programadores inexpertos, debido al cambio radical de paradigma requerido para trabajar con polinomios. 52