💻 computer science

Sound Enforcement of Dynamic Release Information Flow Policy-Full Version

Este artículo presenta el primer sistema de tipos que aplica de manera sólida políticas de flujo de información de liberación dinámica, demostrando formalmente su corrección y su viabilidad práctica a través de un prototipo en Rust aplicado a sistemas de revisión de conferencias y Civitas.

Autores originales: Jeffrey C. Ching, Danfeng Zhang

Publicado 2026-08-11

📖 9 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Jeffrey C. Ching, Danfeng Zhang

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 que eres el guardián de una biblioteca masiva y de alta tecnología. Durante décadas, el libro de reglas para guardar secretos fue increíblemente simple: una vez que un libro se marca como "Secreto", permanece "Secreto" para siempre. Nunca puedes sacarlo del estante y nunca puedes permitir que un visitante normal lo vea. Esta regla, conocida en el mundo de la informática como "no interferencia", es excelente para mantener las cosas seguras, pero también es increíblemente rígida. En el mundo real, los secretos no permanecen secretos para siempre. A veces, un secreto necesita volverse público (como anunciar al ganador de un juego), y a veces, una pieza de información pública necesita convertirse en un secreto (como borrar tu número de tarjeta de crédito después de realizar una compra). Si las reglas de tu biblioteca son demasiado estrictas, no podrás hacer estas cosas necesarias sin romper las reglas. Pero si relajas demasiado las reglas, podrías filtrar un secreto accidentalmente. Este es el complejo rompecabezas que los científicos de la computación han intentado resolver: cómo construir un sistema de seguridad lo suficientemente inteligente como para saber cuándo un secreto puede cambiar su estado, sin dejar que los malos se cuelen.

Este artículo, titulado "Sound Enforcement of Dynamic Release Information Flow Policy" (Cumplimiento sólido de la política de flujo de información de liberación dinámica), aborda exactamente ese rompecabezas. Los autores, Jeffrey Ching y Danfeng Zhang, han creado un nuevo conjunto de reglas y un "verificador mágico" (un sistema de tipos) que permite a los programas informáticos cambiar sus etiquetas de seguridad sobre la marcha, pero solo cuando es seguro hacerlo. No solo soñaron con la idea; construyeron un prototipo en el lenguaje de programación Rust y demostraron matemáticamente que funciona. Demostraron que su sistema puede manejar escenarios complejos —como un juego de pujas donde las ofertas son secretas hasta que termina el juego, o un sistema de votación donde las credenciales se borran después de su uso— sin permitir que ninguna información no autorizada se filtre. Es como darle a tu guardia de la biblioteca un reloj inteligente que le dice exactamente cuándo un libro "Secreto" puede ser entregado a un visitante, y cuándo un libro "Público" debe ser guardado bajo llave, asegurando que la biblioteca permanezca segura sin importar cómo cambien las reglas.

El Problema: El Guardia de Seguridad "Estático"

Para entender la solución, primero debemos mirar la forma antigua de hacer las cosas. Durante mucho tiempo, la seguridad informática dependió de un concepto llamado no interferencia. Imagina a un guardia de seguridad en un banco que tiene una regla estricta: "Si una bóveda está cerrada, nada de lo que hay dentro puede salir jamás". Esto funciona muy bien si la bóveda siempre está cerrada. Pero ¿qué pasa si el gerente del banco dice: "Está bien, a las 5:00 PM vamos a abrir la bóveda y contar el dinero"? Bajo las reglas antiguas, el guardia diría: "¡No! La bóveda está cerrada, así que no puedes abrirla". El guardia no entiende que la bóveda debe abrirse en un momento específico.

En términos informáticos, esto significa que los sistemas de seguridad tradicionales asumen que la información es "Secreta" o "Pública" y que este estado nunca cambia. Pero en la vida real, los datos son dinámicos. Una puja en una subasta es secreta hasta que la subasta termina, luego se vuelve pública. Un número de tarjeta de crédito es necesario para una transacción, pero una vez que la transacción se ha completado, debe ser "borrado" para que nadie pueda usarlo de nuevo. Los antiguos guardias "estáticos" no pueden manejar estos cambios. O bloquean todo (haciendo que el sistema sea inútil) o se confunden y dejan escapar secretos.

La Solución: La Política de "Liberación Dinámica"

Los autores proponen una nueva forma de pensar llamada Liberación Dinámica. En lugar de una etiqueta estática de "Secreto" o "Público", imagina que cada dato tiene una "etiqueta inteligente" que puede cambiar según los eventos.

Piénsalo como un ticket mágico para un concierto.

El Ticket: Este es tu dato (como una puja o una contraseña).
El Evento: Este es un momento específico en el tiempo, como "La subasta ha terminado" o "La transacción se ha completado".
La Regla: El ticket dice: "Soy un ticket VIP (Secreto) hasta que ocurra el evento. Una vez que el evento ocurre, me convierto en un ticket regular (Público)".

El artículo introduce un lenguaje donde puedes escribir estas reglas explícitamente. Puedes decir: "Este dato es Secreto, pero si ocurre el evento subasta_terminada, se vuelve Público". O bien: "Este dato es Público, pero si ocurre el evento transaccion_hecha, se convierte en Top Secret (lo que significa que debe ser destruido)".

El "Verificador Mágico" (El Sistema de Tipos)

Tener una etiqueta inteligente es genial, pero ¿cómo te aseguras de que la computadora realmente siga las reglas? No puedes simplemente pedirle al programador que sea cuidadoso; podría cometer un error. Los autores construyeron un Sistema de Tipos, que es como un superinteligente corrector de estilo para la seguridad.

Imagina que estás escribiendo una historia y tu corrector no solo busca errores ortográficos, sino que también busca agujeros en la trama.

Si escribes: "El héroe abre la puerta secreta", el corrector revisa: "¿Tenía el héroe la llave?".
Si aún no le has dado la llave al héroe, el corrector grita: "¡ERROR! ¡No puedes abrir la puerta todavía!".

En este artículo, el "corrector" es un Sistema de Tipos que se ejecuta antes de que el programa comience (en tiempo de compilación). Revisa cada línea de código y pregunta:

"¿Es este dato actualmente Secreto?"
"¿Está ocurriendo realmente en este momento el evento que permite que se vuelva Público?"
"Si intentas mostrar este dato al público, ¿lo permitirán las reglas?"

Si la respuesta a cualquiera de estas preguntas es "No", el programa se niega a ejecutarse. Es como un portero en un club que revisa tu identificación y tu lista de invitados. Si tu invitación dice "Entrada permitida solo después de las 10 PM", y son las 9:59 PM, el portero no te dejará entrar, sin importar cuánto discutas.

El Comando `relabel`

Una de las características más geniales que inventaron es un comando llamado relabel. Piensa en esto como una "varita mágica" que el programador puede usar para cambiar una etiqueta, pero solo si las condiciones son las adecuadas.

Imagina que eres un mago. Tienes una poción que está etiquetada como "Veneno". Quieres convertirla en "Agua Curativa". No puedes simplemente agitar tu varita y cambiar la etiqueta; eso sería peligroso. Necesitas una condición específica, como "El sol está saliendo".

El Comando: relabel(pocion, Veneno a Agua Curativa usando sol_saliendo)
La Verificación: El verificador mágico mira al cielo. ¿Está saliendo el sol?
- Sí: La poción se convierte en Agua Curativa. La etiqueta cambia de forma segura.
- No: El comando no hace nada. La poción sigue siendo Veneno. El sistema evita que cambies la etiqueta cuando la condición no se ha cumplido.

Esto asegura que incluso si el programador intenta cambiar las reglas sin cumplir la condición específica (como la salida del sol), el sistema no le permitirá cambiar las reglas a menos que el "evento" específico (como la salida del sol) haya ocurrido realmente.

Probando que Funciona

Los autores no solo construyeron esto y esperaron lo mejor. Hicieron dos cosas muy importantes:

Prueba Matemática: Escribieron una prueba formal (un argumento matemático riguroso) que demuestra que su sistema es "sólido" (sound). En lenguaje sencillo, esto significa que demostraron que si un programa pasa su corrector de estilo, es imposible que filtre un secreto. No es solo una suposición; es una garantía basada en la lógica. Tuvieron que inventar nuevas formas de probar esto porque los métodos antiguos asumían que los secretos nunca cambiaban, lo cual no funcionaba para su sistema dinámico.
Pruebas en el Mundo Real: Construyeron un prototipo en el lenguaje de programación Rust (un lenguaje popular conocido por ser seguro y rápido). Tomaron dos ejemplos del mundo real y los portaron a su nuevo sistema:
- Un Sistema de Revisión de Conferencias: Esto es como un sistema donde los profesores revisan artículos. Las puntuaciones son secretas hasta que las revisiones terminan. Su sistema evitó con éxito que las puntuaciones se filtraran prematuramente.
- Un Sistema de Votación Segura (Civitas): Este sistema maneja votos y credenciales. Tiene que borrar las credenciales después de usarlas para proteger la privacidad del votante. Su sistema aplicó con éxito esta política de "borrado".

Los Resultados

Cuando probaron su sistema, descubrieron que funcionaba perfectamente. Detectó todos los errores de seguridad que los sistemas antiguos habrían pasado por alto, y permitió que los programas hicieran las cosas dinámicas que necesitaban (como liberar pujas o borrar tarjetas).

También midieron qué tan lento corría el programa debido a estos controles de seguridad adicionales. Los resultados fueron sorprendentemente buenos: la ralentización fue mínima. Para un sistema de conferencias, añadió unos 0.004 milisegundos (de 0.029ms a 0.033ms). Para el sistema de votación, añadió unos 0.042 milisegundos (de 5.694ms a 5.736ms). Esto es tan pequeño que un humano ni siquiera podría notarlo. Demuestra que puedes tener una seguridad dinámica súper segura sin hacer que tu computadora sea lenta.

Por Qué Esto Importa

Este artículo es un gran paso adelante porque cierra la brecha entre la teoría y la práctica. Durante años, los investigadores tuvieron grandes ideas sobre cómo manejar secretos cambiantes, pero eran demasiado complicadas para usarse en software real. Este artículo proporciona una forma unificada, simple y probada de hacerlo.

Es como pasar de un mundo donde tienes que elegir entre una bóveda cerrada (demasiado estricta) y una puerta abierta (demasiado permisiva) a un mundo donde tienes una puerta inteligente que sabe exactamente cuándo cerrar y cuándo abrir. Los autores demostraron que esta puerta inteligente no solo es posible, sino también rápida y confiable. No solo dijeron "podría funcionar"; lo probaron matemáticamente y lo mostraron funcionando en código real.

En el futuro, esto podría significar que las aplicaciones que usamos a diario —aplicaciones bancarias, sistemas de votación, redes sociales— podrían ser mucho más seguras. Podrían proteger automáticamente nuestros datos cuando sean sensibles y liberarlos de forma segura cuando sea el momento, todo sin que tengamos que preocuparnos por las complejas reglas que ocurren detrás de escena. El "verificador mágico" asegura que las reglas se sigan, para que podamos confiar un poco más en nuestro mundo digital.

Resumen Técnico: Aplicación Sólida de la Política de Flujo de Información de Liberación Dinámica

Planteamiento del Problema

El análisis de flujo de información es el método estándar para evaluar la confidencialidad y la integridad, sin embargo, su adopción en sistemas del mundo real se ve obstaculizada por una brecha fundamental entre la teoría y la práctica. Las políticas de no interferencia tradicionales asumen que la confidencialidad e integridad de la información son estáticas; es decir, no cambian con el tiempo. Sin embargo, las preocupaciones de seguridad en el mundo real son inherentemente dinámicas. Por ejemplo, los datos sensibles pueden necesitar ser desclasificados (degradados) después de un evento específico, o los datos públicos pueden necesitar ser borrados (elevados) para prevenir filtraciones futuras.

La investigación existente ha abordado instancias específicas de políticas dinámicas, tales como la desclasificación, el endoso, el borrado y la revocación. Sin embargo, el campo sufre de una terminología, formalismos y semánticas inconsistentes, lo que dificza la comparación de políticas o su aplicación uniforme. Un trabajo reciente de Li y Zhang [30] propuso la "Liberación Dinámica" (Dynamic Release) como una política de extremo a extremo unificada que permite que las restricciones de flujo de información se degraden y se eleven de formas arbitrarias, pero carecía de un mecanismo de aplicación sólido. El desafío central abordado en este artículo es cómo aplicar sólidamente esta poderosa y general política de liberación dinámica en un lenguaje de programación.

Metodología

Los autores presentan un marco integral que consiste en un lenguaje central, un sistema de tipos estático y pruebas de solidez formales.

1. Lenguaje Central y Semántica

Los autores definen un lenguaje imperativo simple extendido con especificaciones de seguridad adaptadas para la liberación dinámica:

Eventos de Seguridad: Un conjunto distinguido de eventos de seguridad ( $S$ ) que pueden activarse mediante los comandos eventon y eventoff. Estos eventos controlan la evolución de las etiquetas de seguridad.
Etiquetas Dinámicas: Las etiquetas se definen como $cnd? p \diamond q$ $c n d ? p ⋄ q$ , donde $cnd$ es una condición sobre los eventos de seguridad, y $\diamond$ $⋄$ especifica la dirección (degradación, elevación o bidireccional) y la persistencia (transitoria o persistente) de la transición.
- Políticas transitorias ( $\to_t, \leftrightarrow_t$ ) no permiten que la información filtrada en el pasado sea revelada nuevamente si las restricciones se elevan.
- Políticas persistentes ( $\to_p, \leftrightarrow_p$ ) permiten que la información previamente filtrada sea revelada nuevamente incluso si las restricciones se elevan posteriormente.
Salida Controlada: El comando output(L, e, using s0...sk) revela el valor $e$ al nivel $L$ solo si todos los eventos de seguridad especificados están habilitados. Si no se cumplen las condiciones, el comando actúa como un no-op (operación nula).
Comando de Relabel (Relabelado): El comando x := relabel(e, p to L using s0...sk) permite una verificación más permisiva del flujo de información. Actualiza $x$ con el valor de $e$ solo si se cumplen las condiciones using. Esto permite que el sistema de tipos razone sobre los flujos basados en la suposición de que han ocurrido eventos específicos, sin necesidad de un conocimiento profundo del estado en tiempo de ejecución.

La semántica operacional se define utilizando semántica de pasos pequeños que rastrea una traza de eventos de seguridad ( $\sigma$ ). Esta traza registra la secuencia de eventos desencadenados durante la ejecución, lo cual es esencial para interpretar las etiquetas dinámicas.

2. Sistema de Tipos Estático

Para aplicar la política en tiempo de compilación, los autores desarrollan un sistema de tipos basado en dos relaciones estáticas novedosas parametrizadas por un conjunto de hechos computados estáticamente ( $S$ ) sobre los eventos de seguridad:

Relación de Flujo-hacia ( $\sqsubseteq^\sim$ ): Determina si una etiqueta $p$ es menos restrictiva o equivalente a una etiqueta $q$ dado el hecho actual de eventos. Esta relación maneja la complejidad de comparar etiquetas dinámicas donde la interpretación de una etiqueta cambia según la traza de eventos. Los autores proporcionan reglas de inferencia específicas (por ejemplo, R-To, D-To) para manejar condiciones anidadas y asegurar la solidez evitando suposiciones erróneas sobre el orden de los eventos.
Relación de Liberación-hacia ( $<\sim$ ): Verifica si la información con la etiqueta $p$ puede ser liberada de forma segura al nivel de seguridad $L$ en un punto determinado del programa. Esta relación es más simple que la de flujo-hacia, ya que no necesita considerar cambios futuros en la etiqueta tras la liberación.

El sistema de tipos utiliza estas relaciones para verificar asignaciones, condicionales, bucles y los novedosos comandos relabel y output. Distingue entre políticas transitorias y persistentes, particularmente en la regla Output-Per, que permite la re-liberación de datos inmutables si estos fueron liberados previamente bajo una política persistente.

3. Prueba de Solidez

Los autores prueban formalmente que el sistema de tipos aplica la política de liberación dinámica para todas las ejecuciones del programa.

Desafío: Las pruebas de no interferencia estándar dependen de una relación de indistinguibilidad sobre los estados de memoria que permanece invariante porque el conjunto de variables públicas es estático. En la liberación dinámica, el conjunto de variables públicas cambia a medida que las etiquetas evolucionan, rompiendo los invariantes estándar.
Solución: Los autores introducen una novedosa relación de indistinguibilidad parametrizada por una etiqueta dinámica distinguida $B$ (que representa la fuente sensible) y el nivel del atacante $L$ . Prueban que el conjunto de variables consideradas "secretas" respecto a $B$ no aumenta durante la ejecución (Lema de Preservación de Traza).
Consistencia: La prueba tiene en cuenta la "consistencia" de las trazas, un concepto único de la liberación dinámica, que gestiona la alineación de las salidas entre diferentes ejecuciones donde la degradación puede causar que las trazas difieran en longitud.
Resultado: La prueba establece que, para cualquier programa bien tipado, el conocimiento que un atacante obtiene al observar las salidas está limitado por la concesión de la política en cada punto del programa.

4. Implementación

Los autores implementaron un prototipo del sistema de tipos como una biblioteca para el lenguaje Rust, aprovechando el sistema de traits de Rust y los phantom types para la verificación en tiempo de compilación.

Mapearon los constructos del lenguaje central a genéricos de Rust (DRLabel).
Portaron dos casos de estudio existentes a esta implementación:
1. Un Sistema de Revisión de Conferencias (basado en Lifty), que maneja escenarios como la divulgación de contraseñas y la liberación de puntuaciones.
2. Civitas, un sistema de votación segura (originalmente en Jif), que maneja el borrado de credenciales y la desclasificación.
La evaluación de rendimiento en estos casos de estudio mostró una sobrecarga mínima en tiempo de ejecución, ya que la traza de eventos solo crece con comandos específicos y se verifica con poca frecuencia.

Contribuciones Clave

Formalización: Un lenguaje central y una especificación de seguridad que soporta políticas de liberación dinámica, incluyendo constructos novedosos como relabel y output controlado por eventos.
Sistema de Tipos: Un sistema de tipos estático que emplea relaciones de "flujo-hacia" y "liberación-hacia" para verificar flujos de información dinámicos en tiempo de compilación.
Prueba de Solidez: Técnicas de prueba novedosas que establecen la solidez de extremo a extremo del sistema de tipos frente a la política de liberación dinámica, abordando los desafíos de la interpretación de etiquetas dinámicas y la consistencia de trazas.
Implementación: Un prototipo funcional en Rust y la verificación exitosa de aplicaciones realistas (Revisión de Conferencias y Civitas), demostrando la viabilidad de aplicar una política dinámica unificada.

Resultados y Significado

El artículo afirma proporcionar la primera aplicación sólida de la política de liberación dinámica. La importancia de este trabajo radica en su capacidad para unificar varias políticas dinámicas (desclasificación, endoso, borrado, revocación) bajo un único marco general. A diferencia de trabajos previos que construyeron mecanismos de aplicación aislados para políticas específicas, este enfoque ofrece un sistema de tipos unificado capaz de razonar sobre degradaciones y elevaciones arbitrarias.

Los autores demuestran que su marco puede verificar con éxito requisitos de seguridad realistas en sistemas complejos (como la gestión de votaciones y conferencias) con una sobrecarga mínima en tiempo de ejecución. Al pasar de una aplicación ad-hoc y específica de cada política a un sistema general y probado sólidamente, este trabajo cierra la brecha entre la expresividad teórica de la liberación dinámica y su implementación práctica en lenguajes de programación del mundo real. El artículo concluye que, si bien el prototipo actual tiene limitaciones (por ejemplo, falta de inferencia automática de anotaciones y soporte para funciones de primer orden), establece una base teórica y práctica sólida para futuras extensiones.