Proving Circuit Functional Equivalence in Zero Knowledge

Este artículo presenta ZK-CEC, el primer marco de verificación formal que utiliza pruebas de conocimiento cero para garantizar la equivalencia funcional de circuitos de hardware y la seguridad de la propiedad intelectual sin revelar los diseños confidenciales, superando así las limitaciones de los métodos basados en simulación.

Lo esencial

¡Claro que sí! Imagina que este artículo científico es como una historia sobre cómo dos personas pueden tener una conversación secreta y confiable sin que una de ellas tenga que mostrarle a la otra su "receta secreta" de cocina.

Aquí tienes la explicación de "ZK-CEC" (la solución que proponen los autores) en un lenguaje sencillo, usando analogías:

🏭 El Problema: El Dilema del Chef y el Cliente

Imagina un Chef (el Vendedor de Chips) que quiere vender un nuevo tipo de motor para coches (un chip de computadora) a un Concesionario (el Comprador).

• El miedo del Concesionario: "¿Estás seguro de que este motor no tiene un truco oculto? ¿No tiene un botón secreto que lo haga fallar en situaciones raras? Quiero verlo funcionar perfectamente antes de pagar".
• El miedo del Chef: "¡No puedo mostrarte los planos del motor! Si te los doy, alguien me los robará, los copiará y me arruinará. Mi diseño es mi secreto más valioso".

Antes de este trabajo, la única forma de verificar el motor era simulada. Era como si el Chef dijera: "Mira, hice funcionar el motor 100 veces y salió bien". Pero el Concesionario pensaba: "¿Y si solo probaste las situaciones fáciles? ¿Y si el truco solo sale cuando llueve y hay luna llena?". Las simulaciones no garantizan el 100% de seguridad.

🕵️‍♂️ La Solución: La Caja Mágica (ZK-CEC)

Los autores (Sirui, Zunchen y Chenglu) crearon un sistema llamado ZK-CEC. Es como una Caja Mágica de Verificación que permite al Chef demostrar que su motor es perfecto sin abrir la caja ni mostrar los planos.

Funciona así:

1. La Prueba de "No Hay Trucos" (Lógica Formal): En lugar de probar el motor 100 veces, el Chef usa matemáticas avanzadas para demostrar que es imposible que el motor falle. Es como demostrar que, por las leyes de la física, un motor no puede explotar si está bien diseñado.
2. El Secreto (Cero Conocimiento): Aquí viene la magia. El Chef mete su diseño secreto en la caja. La caja hace los cálculos matemáticos por dentro. Al final, la caja le muestra al Concesionario un sello verde brillante que dice: "¡Verificado! El motor funciona exactamente como prometiste".
3. Lo que el Concesionario ve: Solo ve el sello verde y el tamaño de la caja. No ve el motor, ni los cables, ni los planos. Sabe que funciona, pero no sabe cómo funciona.

🧩 El Truco de la "Fórmula Secreta"

El papel explica un problema técnico interesante:

• Antes, existían cajas mágicas que podían verificar si una fórmula pública (algo que todos conocen) era correcta.
• Pero si la fórmula era secreta (el diseño del chip), la caja mágica antigua fallaba. Un Chef deshonesto podría meter una fórmula falsa en la caja y decir "¡Mira, mi fórmula secreta es correcta!" (cuando en realidad estaba mintiendo sobre qué fórmula estaba usando).

La Innovación de este Papel:
Los autores crearon un Nuevo Plano de Construcción (Blueprint) para la caja mágica.

• Imagina que el diseño del motor se divide en dos partes:
  • Parte Pública: Las reglas del tráfico (lo que todos saben que debe cumplir el motor).
  • Parte Secreta: Los planos del motor (lo que el Chef guarda).
• La nueva caja mágica verifica que, aunque no vea los planos, es imposible que el motor secreto rompa las reglas públicas. Verifica que el "secreto" y la "regla" no chocan entre sí. Si chocaran, la caja se pondría roja. Si no chocan, se pone verde.

🚀 ¿Qué lograron? (Los Resultados)

• Funciona de verdad: Probaron su sistema con circuitos reales, desde sumadores simples hasta componentes de cifrado muy complejos (como los que usan los bancos para proteger tus datos).
• Es rápido: Antes, hacer esto matemáticamente tomaba una eternidad. Ellos optimizaron el proceso y lograron hacerlo hasta 3 veces más rápido en algunos casos.
• Es seguro: Garantizan que el vendedor no puede engañar al comprador, y el comprador no puede robar el secreto del vendedor.

🎯 En Resumen

Este papel presenta la primera herramienta que permite a los fabricantes de chips decir: "Confía en mí, mi chip es perfecto y seguro", sin tener que decir "Aquí tienes los planos, por favor no los copies".

Es como si pudieras probar que tu casa es a prueba de incendios mostrando un certificado oficial, sin tener que abrir las puertas y dejar que todos vean cómo están construidas las vigas de madera. ¡Una revolución para la confianza en la tecnología!

Resumen técnico

1. Planteamiento del Problema

El ecosistema de circuitos integrados (IC) moderno depende cada vez más de la integración de Propiedad Intelectual de terceros (3PIP). Esto genera riesgos de seguridad como hardware Trojans, errores de diseño intencionales y vulnerabilidades.

• El Dilema de Confianza: Existe un bloqueo entre los proveedores de IP y los integradores del sistema. El proveedor no puede revelar el diseño (riesgo de piratería), pero el integrador necesita verificar que el diseño es correcto y seguro antes de comprarlo.
• Limitaciones de los Métodos Actuales: Las soluciones existentes de verificación con preservación de la privacidad se basan en simulación (usando cifrado homomórfico o máquinas virtuales de conocimiento cero - zkVM). La simulación no es exhaustiva; no puede garantizar la ausencia de Trojans o errores en casos extremos (corner cases) que solo se activan bajo condiciones muy específicas.
• La Necesidad de Verificación Formal: La verificación formal (como la comprobación de equivalencia combinacional, CEC) ofrece garantías matemáticas exhaustivas. Sin embargo, los protocolos de prueba de conocimiento cero (ZKP) existentes para verificación formal (como ZKUNSAT) están diseñados para fórmulas públicas. Si se intenta usarlos con fórmulas secretas, un probador malicioso podría forjar una fórmula falsa y demostrar propiedades sobre ella, rompiendo la solidez (soundness) del protocolo.

2. Metodología Propuesta: ZK-CEC

Los autores proponen ZK-CEC, el primer marco de verificación formal de hardware con preservación de la privacidad. La metodología se basa en combinar la verificación formal con pruebas de conocimiento cero (ZKP) utilizando el protocolo VOLE (Vector Oblivious Linear Evaluation).

A. El "Blueprint" (Bosquejo) para Verificación de Fórmulas Secretas

Para resolver el problema de solidez en fórmulas secretas, proponen un nuevo esquema que divide el problema en:

1. Fórmula del Sistema ($\Phi_{sys}$): Secreta (el diseño del proveedor).
2. Fórmula de la Propiedad ($\Phi_{prop}$): Pública (la especificación o requisito de seguridad).
3. Objetivo: Demostrar que la conjunción de ambas es insatisfacible ($\Phi_{sys} \land \Phi_{prop} \models \bot$), lo que implica que el sistema secreto cumple la propiedad pública.

Para garantizar la solidez, el protocolo verifica cuatro propiedades críticas:

1. Correctitud de la Propiedad: La fórmula pública es correcta y satisfacible.
2. Insatisfacibilidad de la Mitad: El circuito de "miter" (comparación entre especificación e implementación) es insatisfacible.
3. Satisfacibilidad del Sistema Secreto: El diseño secreto no contiene contradicciones internas (es un diseño válido).
4. Aislamiento de Variables: Las variables secretas y públicas solo interactúan a través de la interfaz definida, evitando que el probador manipule la lógica interna para engañar.

B. Protocolo ZK-CEC y Codificación

El protocolo se construye sobre cuatro sub-protocolos ($\Pi_{P1}$ a $\Pi_{P4}$) que utilizan:

• Codificación Polinómica: Las cláusulas de la fórmula CNF se codifican como polinomios univariados donde las literales son raíces. Esto permite verificar operaciones lógicas (pertenencia, implicación) mediante aritmética de polinomios.
• Compromisos VOLE: Se utiliza el esquema de compromiso basado en VOLE para ocultar los valores de las literales secretas mientras se permiten operaciones lineales y multiplicativas.
• Prueba de Resolución: Se utiliza un sistema de prueba de refutación (resolución) para demostrar la insatisfacibilidad, modelado como un programa de RAM/ROM en el entorno de conocimiento cero.

C. Optimización

Los autores introducen una optimización de compresión de resolventes. Dado que en los algoritmos SAT modernos (CDCL) muchas cláusulas intermedias se aprenden y reutilizan, el protocolo fusiona múltiples pasos de resolución en un solo derivado, almacenando solo las cláusulas aprendidas clave. Esto reduce la sobrecarga computacional sin permitir al verificador reconstruir la fórmula original (análisis de límites inferiores de complejidad factorial).

3. Contribuciones Clave

1. Nuevo Blueprint de Verificación: Un marco general para la verificación formal de propiedades en sistemas con lógica oculta (hardware, software, ciber-físicos), resolviendo el dilema de solidez de los protocolos ZK anteriores.
2. Primer Protocolo ZK para CEC: La implementación del primer protocolo de conocimiento cero para la Combinational Equivalence Checking (CEC). Permite a un proveedor demostrar que su IP secreta es funcionalmente equivalente a una especificación pública sin revelar el diseño.
3. Garantías Formales: A diferencia de la simulación, ZK-CEC ofrece garantías matemáticas exhaustivas contra Trojans y errores de diseño.
4. Implementación y Evaluación: Implementación completa basada en el EMP-toolkit y evaluación en una amplia gama de circuitos.

4. Resultados Experimentales

El equipo evaluó ZK-CEC en 37 circuitos combinacionales, incluyendo:

• Unidades aritméticas (sumadores, multiplicadores).
• Lógica de control (codificadores, máquinas de estado finito).
• Componentes criptográficos (S-Boxes de AES, SM4, Ascon, Present).

Hallazgos principales:

• Viabilidad Práctica: El protocolo logró verificar diseños prácticos, como la S-Box de AES, dentro de límites de tiempo razonables.
• Rendimiento:
  • La verificación de la insatisfacibilidad (parte más costosa, $\Pi_{P1} + \Pi_{P2}$) domina el tiempo de ejecución, lo cual es esperable dado que la insatisfacibilidad es un problema co-NP-completo.
  • Las partes de satisfacción ($\Pi_{P3}$) y aislamiento ($\Pi_{P4}$) escalan linealmente con el tamaño del circuito.
  • La optimización de compresión de resolventes logró acelerar el tiempo de prueba hasta en un 2.88x (ej. en multiplicadores de 6x6 y S-Boxes complejas).
• Escalabilidad: El principal cuello de botella es el crecimiento exponencial de la longitud de la prueba de refutación en circuitos muy grandes, lo que puede llevar a desbordamientos de memoria, aunque el marco es funcional para diseños de tamaño medio y grande.

5. Significado e Impacto

• Seguridad de la Cadena de Suministro: ZK-CEC ofrece una solución técnica viable para romper el bloqueo de confianza en la cadena de suministro de hardware. Permite transacciones justas donde el comprador verifica la seguridad y funcionalidad sin que el vendedor pierda la propiedad intelectual.
• Avance en Verificación Formal Privada: Marca un hito al trasladar la verificación formal (que tradicionalmente requiere ver el código completo) al ámbito de la privacidad, superando las limitaciones de los métodos basados en simulación.
• Generalidad: El "blueprint" propuesto no se limita al hardware; es aplicable a la verificación de software y sistemas ciber-físicos donde se necesita probar propiedades sobre lógica oculta.

En resumen, el paper presenta ZK-CEC como una herramienta fundamental para la seguridad de la cadena de suministro de semiconductores, combinando la rigurosidad matemática de la verificación formal con la privacidad de las pruebas de conocimiento cero.