Extensión de CIRCOM con buses: expresividad y seguridad

Abstract

A lo largo de este proyecto se ha desarrollado una extensión de circom, un lenguaje de dominio específico ampliamente extendido para la definición de circuitos aritméticos orientados a demostraciones de “conocimiento nulo” (protocolos criptográficos que permiten verificar la veracidad de un predicado sin revelar información sobre el mismo). El alcance de dicha extensión incluye la incorporación de sintaxis para poder definir conjuntos de señales personalizados llamados buses, los cuales hacen las veces de los structs de la mayoría de lenguajes de programación. Los buses permiten realizar el etiquetado de grupos de señales mediante tags, un elemento de circom gracias al cual se pueden anotar propiedades sobre las señales. Los tags funcionan como un tipado débil orientado a reforzar la corrección y seguridad de los circuitos aritméticos generados. Para añadir las nuevas funcionalidades mencionadas a circom se ha trabajado sobre un fork del compilador original con vistas a incorporar estos cambios a la versión oficial proximamente. También se han llevado a cabo mejoras sobre circuitos de la circomlib (la librería oficial del lenguaje circom) empleando los nuevos buses y tags de buses con el objetivo de mejorar la comprensión y seguridad de los programas. Estos circuitos actualizados serán incluidos en la nueva versión oficial de la circomlib. Además, se han realizado pruebas de rendimiento con las que se ha comprobado que el uso de buses no tiene un impacto negativo en el tamaño de las pruebas generadas por circuitos de circom. Una versión extendida de este trabajo se tratará de publicar en una revista internacional de alto impacto, como IEEE Transactions on Dependable and Secure Computing.Throughout this project, an extension of circom has been developed. Circom is a widely used domain-specific language for defining arithmetic circuits aimed at zero-knowledge proofs (cryptographic protocols that allow the verification of a predicate’s truth without revealing information about it). The scope of this extension includes the incorporation of syntax to define custom signal sets called buses, which function similarly to the structs found in most programming languages. Buses allow the labelling of signal groups using tags, a feature of circom that enables the annotation of properties on signals. Tags function as a weak typing mechanism aimed at reinforcing the correctness and security of the generated arithmetic circuits. To add the mentioned new functionalities to circom, work has been done on a fork of the original compiler in view of incorporating these changes into the official version soon. Improvements have also been made to circuits in the circomlib (the official library of the circom language) using the new buses and bus tags with the aim of improving the understanding and security of the programs. These updated circuits will be included in the new official version of the circomlib. Additionally, the performance tests conducted have shown that the use of buses does to not have a negative impact on the size of the proofs generated by circom circuits. An extended version of this work will be submitted for publication in a high-impact international journal, such as IEEE Transactions on Dependable and Secure Computing.