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

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.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.