Zcash completa la verificación formal de Ironwood, publica la eliminación del riesgo de falsificación de ZEC con el teorema de Lean

El proyecto Tachyon de Zcash anunció el 29 de julio que había completado la verificación formal del pool blindado de Ironwood y publicó una prueba de verificación por máquina, que incluye más de 2.700 teoremas escritos con el lenguaje de programación Lean. Esta verificación estableció una propiedad de seguridad llamada «integridad del saldo», que elimina de forma efectiva la posibilidad de que Ironwood, bajo sus supuestos criptográficos establecidos, tenga vulnerabilidades de falsificación que no puedan detectarse.

Se completa la verificación formal del proyecto Tachyon: más de 2700 teoremas en Lean

El trabajo de verificación formal del proyecto Tachyon se realizó en colaboración entre tres investigadores y un equipo de criptógrafos, y tomó más de un mes; la prueba de verificación por máquina publicada finalmente incluye más de 2.700 teoremas, todos escritos en el lenguaje de programación Lean. El significado de esta verificación es que se trata de una verificación «por máquina», es decir, que una computadora comprueba automáticamente la corrección de cada paso lógico, en lugar de depender únicamente de una revisión manual, lo que aporta un nivel mayor de certeza.

Tachyon indica que la verificación completada establece una garantía matemática de que el pool blindado de Ironwood no contiene vulnerabilidades de falsificación que no puedan detectarse, bajo sus supuestos criptográficos establecidos.

Propiedad de seguridad de “Integridad del saldo”: garantía matemática de que el fondo protegido no pagará de más

La «integridad del saldo (Balance Integrity)» es la propiedad de seguridad central establecida por esta verificación formal, definida matemáticamente como: la cantidad pagada por el fondo protegido de Ironwood no excederá la cantidad depositada públicamente. Para lograr esta propiedad, la verificación abarca los siguientes componentes:

· El sistema de pruebas de conocimiento cero (ZK) de Ironwood

· Reglas del circuito: reglas de cómputo que constituyen la base lógica de Ironwood

· Contabilidad a nivel de libro mayor: mecanismo de seguimiento de fondos y registro contable en toda la capa de red

Cabe destacar que esta prueba no incluye las medidas de protección de privacidad independientes del propio Ironwood; los investigadores afirman que la protección de la privacidad es una propiedad de seguridad independiente y requiere una verificación adicional.

Antecedentes de la vulnerabilidad de Orchard y el mecanismo contable público del “portón giratorio”

La razón directa para la implementación del pool blindado de Ironwood fue la vulnerabilidad hallada en el pool de seguridad de Orchard: en teoría, esta falla podría conducir a que las acciones de falsificación de ZEC no pudieran detectarse, poniendo en riesgo la integridad de la oferta de Zcash. Zcash introdujo Ironwood en la actualización de la versión NU6.3, y los desarrolladores señalan que no han encontrado evidencia de que alguna vulnerabilidad haya sido explotada en la práctica; el nuevo pool blindado busca restaurar la confianza del público en la integridad de la oferta de Zcash.

Los fondos transferidos desde Orchard deben pasar por un punto de verificación contable público denominado «portón giratorio (Revolving Door)», con el objetivo de evitar que cualquier token excedente hipotético ingrese en Ironwood; a medida que los fondos continúan saliendo de Orchard, este proceso también podría aportar progresivamente más evidencia para evaluar si el fondo anterior alguna vez fue mal utilizado.

Preguntas frecuentes

La validación formal del Ironwood del proyecto Tachyon incluye cuántos teoremas y con qué herramientas se completó?

Según el anuncio del proyecto Tachyon, la validación formal incluye más de 2.700 teoremas, todos escritos en el lenguaje de programación Lean; se completó en más de un mes gracias a la colaboración de tres investigadores y un equipo de criptógrafos; el resultado final es una prueba matemática verificada por máquina, donde la computadora verifica automáticamente cada paso lógico.

¿Qué garantiza específicamente la propiedad de seguridad de “Balance Integrity”?

“Balance Integrity” garantiza que la cantidad pagada por el fondo protegido de Ironwood no superará la cantidad depositada públicamente; esta validación cubre todos los componentes necesarios para lograr esta propiedad, incluyendo el sistema de pruebas de conocimiento cero de Ironwood, las reglas del circuito y la contabilidad a nivel de libro mayor; pero esta validación no cubre las medidas independientes de protección de la privacidad de Ironwood.

¿Por qué Zcash necesita introducir Ironwood y el fallo de Orchard ya ha sido explotado?

Ironwood fue introducido por Zcash en la actualización de la versión NU6.3, con el objetivo de abordar un fallo encontrado en el pool de seguridad de Orchard —dicho fallo, en teoría, podría hacer que las acciones de falsificación de ZEC no pudieran detectarse—; los desarrolladores de Zcash afirman que aún no se ha encontrado evidencia de que dicho fallo haya sido explotado en la práctica, y el nuevo pool de enmascaramiento busca restaurar la confianza del público en la integridad de la oferta de Zcash.