💻 computer science

Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL

Este artículo presenta una prueba mecanizada en Isabelle/HOL que establece garantías tanto de seguridad como de vivacidad para la preservación del estado regulatorio entre dominios bajo fallos bizantinos, utilizando un marco reutilizable de siete locales genéricos instanciados frente a un modelo exhaustivo de requisitos regulatorios financieros globales.

Autores originales: Jinwook Kim

Publicado 2026-06-01

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Jinwook Kim

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina un mundo donde los activos digitales (como acciones o bienes raíces tokenizados) pueden moverse libremente entre diferentes "vecindarios" (blockchains) y "libros de contabilidad en papel" (sistemas off-chain). El problema es: si un juez en el Vecindario A congela un activo, este congelamiento debe ocurrir de forma instantánea y perfecta en el Vecindario B, el Vecindario C y también en el libro de contabilidad en papel. Si no es así, los actores malintencionados podrían practicar la "arbitraje regulatorio", ocultando activos en lugares donde las reglas no se aplican.

Este documento es una prueba matemática de que un sistema específico para mover estos activos es tanto seguro (nunca comete errores) como vivo (nunca se queda trabado), incluso si algunos participantes intentan sabotearlo.

Aquí está el desglose utilizando analogías sencillas:

1. El Objetivo: La "Carrera de Relevos Perfecta"

Piensa en el sistema como una carrera de relevos donde el testigo es un "estado regulatorio" (como "Congelado" o "Activo").

El Desafío: Cuando un corredor (una blockchain) cambia el color del testigo, todos los demás corredores del equipo deben ver el mismo color instantáneamente.
El Riesgo: Si un corredor miente, olvida o se queda trabado, toda la carrera podría detenerse, o el testigo podría terminar teniendo dos colores distintos al mismo tiempo.

2. Las Dos Grandes Victorias (Seguridad y Vitalidad)

Los autores demostraron dos cosas sobre su sistema:

A. Seguridad: El "Espejo Inquebrantable"

Qué significa: Si el sistema funciona, el resultado siempre es consistente. Si la Cadena A dice "Congelar", la Cadena B debe decir "Congelar". No hay ambigüedad.
La Analogía: Imagina un conjunto de espejos mágicos. Si pones una pelota roja frente al Espejo A, el Espejo B, el Espejo C y el registro en papel todos muestran una pelota roja. Nunca muestran una pelota azul, y nunca discrepan.
La Prueba: Los autores construyeron un "mapa" (llamado locale) que demuestra que este reflejo ocurre perfectamente, incluso si las cadenas hablan idiomas diferentes (distintos vocabularios técnicos) o si el activo se mueve entre una blockchain y una base de datos en papel. Demostraron que no importa cómo se reordenen las operaciones, la imagen final siempre es la misma.

B. Vitalidad: El "Mecanismo Anti-Atascamiento"

Qué significa: El sistema nunca se congela, incluso si algunos participantes son "Bizantinos" (una palabra elegante para nodos maliciosos o defectuosos que mienten, retrasan mensajes o se niegan a soltar los activos).
La Analogía: Imagina a un grupo de personas intentando pasar una caja pesada por un pasillo estrecho.
- El Problema: Un actor malintencionado podría agarrar la caja y negarse a soltarla, bloqueando a todos los demás.
- La Solución: El sistema tiene un "tiempo de espera" integrado (como una trampilla con resorte). Si alguien sujeta la caja demasiado tiempo, el sistema automáticamente la arranca de sus manos y se la pasa a la siguiente persona.
- La Prueba: Demostraron matemáticamente que incluso si hasta 1/3 de las personas están intentando bloquear el pasillo, la caja siempre llegará al final. Ningún activo quedará bloqueado para siempre.

3. El "Truco de Magia": Combinar los Dos

Normalmente, las pruebas de seguridad asumen que todos son honestos. Las pruebas de vitalidad asumen que algunas personas son malas.

El Truco del Documento: Ellos combinaron ambos. Demostraron que el "Mecanismo Anti-Atascamiento" (Vitalidad) es tan fuerte que corrige la suposición de "Personas Honestas" requerida para el "Espejo Inquebrantable" (Seguridad).
El Resultado: No necesitas confiar en nadie. Incluso con actores malintencionados, el sistema está garantizado para ser consistente y estar en movimiento.

4. El Kit de Herramientas: "Lego Bricks" para las Matemáticas

Los autores no solo demostraron esto para una blockchain específica. Construyeron 7 piezas de Lego reutilizables (llamadas locales en Isabelle/HOL).

Cómo funciona: Estas piezas son genéricas. Puedes encajarlas en cualquier sistema (un banco, una cadena de suministro, un juego) para obtener instantáneamente las mismas garantías de seguridad y vitalidad.
Pruebas en el mundo real: No se limitaron a dejar las piezas en la caja. Las encajaron en tres escenarios muy diferentes del mundo real para demostrar que funcionan:
1. Diferentes Lenguajes: Una cadena que solo habla "Congelar" frente a una que habla "Congelar" y "Descongelar".
2. Diferentes Mundos: Una blockchain frente a un documento legal complejo fuera de la cadena (DAML).
3. El Motor de Consenso: El mecanismo de votación específico utilizado para decidir quién se mueve después.

5. Lo que esto NO es

Para ser claros sobre los límites del documento:

No verifica si un juez específico tiene realmente el derecho legal de congelar un activo. Solo verifica que si se ordena un congelamiento, este ocurra correctamente en todas partes.
No demuestra que el código informático (Rust/Solidity) esté libre de errores; demuestra que el modelo matemático del sistema es sólido.
No gestiona el caos de una red que está añadiendo o eliminando constantemente nuevas cadenas mientras se ejecuta (eso es trabajo futuro).

Resumen

Este documento es un certificado matemático de confianza. Dice: "Hemos construido un sistema donde las reglas regulatorias (como congelar activos) se aplican perfectamente a través de diferentes mundos. Incluso si algunos participantes intentan romperlo, el sistema posee un mecanismo de autocorrección que garantiza que las reglas se sigan y que el sistema nunca se detenga".

Lo lograron escribiendo 3,215 líneas de código en un asistente de pruebas (Isabelle/HOL) que una computadora verificó paso a paso para asegurar que no existan brechas lógicas.

Resumen Técnico: Seguridad y Vitalidad de la Preservación de Estado entre Dominios bajo Fallos Bizantinos

1. Planteamiento del Problema

El artículo aborda el desafío crítico de garantizar la consistencia de los estados de cumplimiento regulatorio para activos tokenizados que operan a través de redes blockchain heterogéneas y libros contables fuera de la cadena (off-chain). Sin garantías formales, el arbitraje regulatorio se vuelve estructuralmente posible; por ejemplo, una orden de congelación emitida en una jurisdicción debe reflejarse de manera inmediata y determinista en todos los dominios conectados.

El problema se descompone en dos dimensiones:

Seguridad (Safety): Garantizar que, si se realiza una sincronización, el estado resultante sea consistente en todos los dominios con preservación estructural.
Vitalidad (Liveness): Garantizar que, en un entorno descentralizado que contiene nodos bizantinos (actores maliciosos), el proceso de sincronización realmente proceda, evitando bloqueos (deadlocks) y inanición (starvation).

Los trabajos previos no han verificado formalmente ambas propiedades simultáneamente en un único marco, ni han verificado propiedades de consenso específicas de la regulación (como el determinismo de prioridad y la ausencia de bloqueo de activos) utilizando Isabelle/HOL.

2. Metodología

Los autores emplean un enfoque de prueba mecanizada utilizando Isabelle/HOL. El desarrollo consiste en 3,215 líneas de código distribuidas en cuatro archivos de teoría, que se compilan sin utilizar sorry u oops (suposiciones no probadas).

2.1 Modelo de Sistema y de Amenazas

Modelo de Sistema: El sistema comprende un conjunto finito de dominios (cadenas/libros contables) que comparten una estructura de máquina de estados. La sincronización se modela como una operación atómica que involucra verificación, validación, adquisición de bloqueo, actualización de estado y liberación de bloqueo.
Modelo de Amenazas:
- Propiedad 1 (Seguridad): Inicialmente asume nodos honestos y canales fiables.
- Propiedad 2 (Vitalidad): Relaja la suposición de nodos honestos para permitir hasta $f < n/3$ nodos bizantinos. Los nodos bizantinos pueden retener las liberaciones de bloqueo o actuar de forma maliciosa.
- Combinado: La Propiedad 2 descarta la suposición de "nodo honesto" de la Propiedad 1, produciendo una garantía incondicional.

2.2 Modelo de Transición de Estado Regulatorio

El modelo formal se basa en el marco del Protocolo de Cumplimiento Regulatorio (RCP), que sistematiza 31 requisitos de 15 autoridades financieras globales.

Estados: Cinco estados regulatorios (ACTIVE, FROZEN, SEIZED, CONFISCATED, RESTRICTED).
Acciones: Siete acciones regulatorias (FREEZE, SEIZE, CONFISCATE, RESTRICT, UNFREEZE, UNRESTRICT, RELEASE).
Restricciones: El modelo impone restricciones legales específicas, tales como la exclusión de las transiciones "SEIZED → FROZEN" (ya que la incautación es una restricción legal más fuerte que la congelación) y la naturaleza terminal del estado CONFISCATED.

2.3 Infraestructura de Verificación: Locales Genéricos

La metodología central se basa en la definición de siete locales genéricos e independientes del dominio en Isabelle/HOL. Estos locales sirven como una infraestructura de verificación reutilizable. Los teoremas probados dentro de estos locales son heredados automáticamente por cualquier dominio concreto que los instancie mediante el mecanismo de interpretación de Isabelle.

Locales de Seguridad (4):
1. state_machine: Define estados finitos, acciones y transiciones deterministas.
2. state_preservation: Establece una condición de naturalidad donde la sincronización conmuta con las transiciones de estado (homomorfismo).
3. symmetric_state_preservation: Añade mapas inversos para garantizar la preservación bidireccional de ida y vuelta.
4. multi_domain_preservation: Generaliza la consistencia a un conjunto arbitrario de dominios finitos (consistencia de $N$ dominios) y asegura el aislamiento por activo.
Locales de Vitalidad (3):
1. priority_system: Garantiza la selección determinista de acciones mediante prioridades inyectivas.
2. deadlock_free_locking: Asegura que ningún recurso se bloquee indefinidamente mediante una liberación forzada basada en tiempos de espera (timeouts).
3. fair_leader_system: Garantiza la ausencia de inanición bajo un esquema de programación de líder honesto periódico.

3. Contribuciones Clave

3.1 Prueba de Seguridad Mecanizada (Propiedad 1)

El artículo extiende el patrón de Functor de Merkle (previamente limitado a la integridad de datos unidireccional en un solo dominio) a un marco trans-dominio, bidireccional y multidominio.

Ida y Vuelta Bidireccional: Demuestra que las transiciones de estado se reflejan fielmente en ambas direcciones entre los domios.
Consistencia de N-Dominios: Demuestra que tras una sincronización en un dominio, todos los dominios conectados alcanzan el mismo estado resultante.
Aislamiento por Activo: Demuestra que la sincronización en un activo no afecta al estado de otros activos.
Instanciaciones Concretas: Los autores proporcionan testigos concretos para asegurar que los locales no se satisfacen de forma vacua:
- Instancia de Escalada: Una instancia de acciones heterogéneas donde una cadena soporta solo acciones de escalada (FREEZE, SEIZE, etc.) mientras que la otra soporta el conjunto completo, demostrando la preservación estructural a través de diferentes vocabularios.
- Instancia de Cruce de Capas: Un puente bidireccional entre un enumerado reg_state on-chain y un registro de permisos DAML off-chain, demostrando la inyectividad y la ausencia de pérdida de información.

3.2 Prueba de Vitalidad Mecanizada (Propiedad 2)

Este es el primer uso de Isabelle/HOL por sí solo para verificar la vitalidad del consenso BFT en un contexto de blockchain.

Determinismo: Los conflictos entre acciones regulatorias se resuelven mediante un orden total sobre claves de prioridad (nivel de autoridad, marca de tiempo, severidad, ID de nodo).
Ausencia de Bloqueos (Deadlock Freedom): Demuestra que incluso si los nodos bizantinos retienen las liberaciones de bloqueo, el mecanismo de tiempo de espera asegura que el bloqueo expire en un tiempo acotado.
el sistema permanece vivo y determinista incluso con fallos bizantinos ( $f < n/3$ ), la garantía de seguridad condicional se promueve a una garantía incondicional: la preservación del estado entre dominios se mantiene incluso ante la presencia de nodos bizantinos.

3.3 Descarga de Suposiciones (Garantía Combinada)

El artículo demuestra un patrón de razonamiento de asunción-garantía (assume-guarantee). La Propiedad 2 descarga la suposición de "nodo honesto" requerida por la Propiedad 1. Al demostrar que el sistema permanece vivo y determinista incluso con fallos bizantinos ( $f < n/3$ ), la garantía de seguridad condicional se eleva a una garantía incondicional: la preservación del estado entre dominios se mantiene incluso en presencia de nodos bizantinos.

4. Resultados y Artefactos

Artefactos de la Prueba: El desarrollo incluye ocho interpretaciones de locales concretos (cubriendo los siete locales genéricos) junto con una instanciación multiparámetrica de múltiples dominios.
Modelo Regulatorio: El modelo cubre 31 requisitos regulatorios mapeados a 5 estados y 7 acciones.
Disponibilidad: Todos los artefactos están disponibles públicamente en GitHub y han sido enviados al Archive of Formal Proofs (AFP) para su revisión.
Guía de Diseño: Las pruebas derivan restricciones de parámetros específicas para la implementación (por ejemplo, $n \ge 3f + 1$ , tiempos de espera positivos, límites de equidad) que se traducen directamente en una base matemática de diseño para secuenciadores descentralizados.

5. Significancia y Reivindicaciones

El artículo reclama significancia en tres áreas principales:

Novedad en la Verificación Formal: Es el primer trabajo que verifica formalmente tanto la seguridad como la vitalidad simultáneamente para las transiciones de estado regulatorio entre dominios. También es el primero en verificar propiedades de consenso específicas de la regulación (determinismo de prioridad, ausencia de bloqueo de activos regulatorios) en cualquier herramienta.
Avance Metodológico: Al utilizar una jerarquía de locales genéricos, los autores proporcionan una infraestructura de verificación reutilizable que es independiente del dominio. Esto permite que las mismas pruebas de seguridad y vitalidad se apliquen a dominios arbitrarios (por ejemplo, DeFi, bases de datos distribuidas) simplemente instanciando los locales.
Puente entre la Teoría y la Práctica: El trabajo va más allá de la verificación de consenso abstracto (como acuerdo/validez) para abordar restricciones regulatorias específicas del dominio. Establece explícitamente el puente entre una máquina de estados teórica y un modelo de cumplimiento regulatorio, proporcionando una "guía de diseño" para los parámetros de implementación derivados directamente de las pruebas.

Los autores señalan explícitamente las limitaciones: el modelo no verifica características específicas de la cadena (gas, tiempos de bloque), no demuestra la refinación formal a código Rust/Solidity, y asume un sistema cerrado (la llegada dinámica de solicitudes es un trabajo futuro). El marco actual establece los locales y las instancias fundamentales, pero aún no formaliza las leyes de los functores de la teoría de categorías, las cuales quedan reservadas para trabajos futuros para lograr el estatus completo de "functor".