Renaming or Tightness: Enforcing Disjunctive Information Flow Policies

Resumen Técnico: ¿Renombrado o Precisión? La imposición de políticas de flujo de información disyuntiva

Planteamiento del problema
Las políticas de flujo de información disjuntiva restringen un valor para que dependa de, como máximo, uno de dos secretos, prohibiendo la combinación de liberaciones que de otro modo serían permisibles (por ejemplo, un muro ético que impide que un informe dependa tanto de los archivos del Cliente A como del Cliente B, o un esquema de intercambio de secretos que libera solo una parte). A diferencia de las políticas estándar basadas en retículos, donde la unión de dos dependencias admisibles es admisible, las políticas disyuntivas no tienen forma de retículo. Hunt y Sands proporcionaron anteriormente una semántica para estas políticas utilizando el "cuantale de la información", donde la conjunción es un tensor no idempotente ($\otimes$) en lugar de una unión. Sin embargo, la capa de ejecución —específicamente, lo que un sistema de tipos sensible al flujo puede certificar sobre tales políticas— seguía siendo un problema abierto.

El desafío central es que los sistemas de tipos existentes sensibles al flujo, que dependen de un objeto universal para permitir un análisis independiente de la política (mediante el renombrado monótono), no logran preservar la precisión bajo políticas disyuntivas. Específicamente, cuando una fuente se lee dos veces (por ejemplo, un resumen utilizado tanto en un encabezado como en una tabla), los mecanismos estándar pierden la correlación de que ambas lecturas respetan el mismo disjunto. En consecuencia, sobreaproximan el flujo de información, certificando que la salida revela ambos secretos ($\top$) incluso cuando la política se cumple.

Metodología
Los autores construyen una familia de sistemas de tipos sensibles al flujo ($F_1$) sobre un cuantale afín conmutativo $M$ arbitrario. El análisis procede investigando el "objeto universal" del cual todos los sistemas específicos de política se especializan. En la era de los retículos, el conjunto potencia de las variables servía como un único objeto universal. El artículo demuestra que, sobre un cuantale, este objeto se divide en tres candidatos distintos, cada uno con diferentes propiedades respecto a la precisión y la capacidad de soportar el renombrado monótono:

1. El Objeto de Multiconjunto ($U_N$): El monoide conmutativo libre sobre las variables (los elementos son multiconjuntos). Soporta el renombrado monótono completo y tipados principales, pero pierde la "correlación de misma fuente". Trata dos lecturas de una fuente como dos usos independientes, lo que conduce a una sobreaproximación ($\sigma(v) \otimes \sigma(v)$).
2. El Objeto de Conjunto ($U$): El monoide conmutativo idempotente libre (los elementos son conjuntos de variables, representados como subconjuntos descendentes del conjunto potencia). Preserva la correlación de misma fuente (dos lecturas de una fuente cuentan como una), pero rompe la propiedad homomórfica requerida para el renombrado monótono. La especialización aquí es una sección oplaxa, no un homomorfismo.
3. El Local Libre ($L$): El objeto de la era de los retículos (conjuntos de variables con la unión como combinación). Es ajustado para lecturas únicas, pero confunde la disyunción de rama con la combinación de tensores, borrando la distinción entre "la ejecución A usó X y la ejecución B usó Y" y "alguna ejecución usó X e Y".

El artículo analiza las compensaciones entre estos objetos, demostrando que ningún mecanismo de la forma de "atributo independiente" (donde los entornos mapean variables a elementos únicos del cuantale) puede soportar simultáneamente el renombrado monótono y lograr límites ajustados para políticas disyuntivas.

Contribuciones clave y resultados

1. Familia de Sistemas de Tipos ($F_1$): Una familia de sistemas de tipos sólida anclada a los lemas de composición de Hunt y Sands. Maneja los bucles mediante el cierre idempotente del factor de guardia, un ajuste necesario para los cuantales que es invisible en los retículos.
2. La división del objeto universal: El artículo establece una trichotomía:
   • Sobre $U_N$, todo el mecanismo de tipados principales y completitud interna sobrevive incondicionalmente, pero el límite es laxo para fuentes reutilizadas.
   • Sobre $U$, el límite es estrictamente más preciso (registrando que dos lecturas respetan un solo disjunto), pero la especialización ya no es un homomorfismo, rompiendo la propiedad de renombrado.
   • Sobre $L$, el objeto pierde la disyunción de rama, fallando en distinguir entre ejecuciones alternativas y ejecuciones combinadas.
3. Imposibilidad de renombrado y ajuste: Los autores demuestran que para cualquier mecanismo sólido de la forma de atributo independiente que soporte el renombrado monótono, el límite certificado para una fuente reutilizada bajo una etiqueta "saturada" (donde $m \otimes m = \top$) es $\top$. Esto significa que, bajo etiquetas de muro ético o intercambio de secretos, una segunda lectura de una fuente no certifica nada, causando que el mecanismo rechace programas que en realidad satisfacen la política.
4. La reparación (Especialización diferida): Para recuperar la precisión, el artículo propone diferir la especialización al nivel del juicio. En lugar de aplicar el mapa de etiquado al entorno (lo que fuerza una estructura homomórfica), el mapa se aplica solo a la observación final (lectura).
   • Este enfoque utiliza el Objeto de Conjunto ($U$) para el tipado y el mapa $\alpha_\sigma$ para la lectura.
   • Se demuestra que el mapa de lectura resultante es el mapa menor sonido preservador de la unión.
   • Esta "reparación" sacrifica la capacidad de presentar el resultado como una derivación dentro del sistema objetivo (renombrado), pero logra el límite más ajustado posible para los mecanismos de atributo independiente.
5. Decidibilidad: El artículo muestra que la verificación de cumplimiento es decidible. Aunque $U_N$ es infinito, el límite especializado depende solo de las multiplicidades hasta el orden de la etiqueta (por ejemplo, 2 para muros éticos), permitiendo una truncación finita. $U$ es un retículo finito, lo que asegura la terminación.

Significado y afirmaciones
El artículo afirma que la transición de sistemas basados en retículos a sistemas basados en cuantales fuerza una elección fundamental que antes estaba oculta: se puede tener renombrado monótono o precisión, pero no ambos.

• Para el paradigma de renombrado: El artículo demuestra que el enfoque del "objeto universal", que permite analizar un programa una vez y reutilizar el resultado para cualquier política, encuentra un techo duro. Para políticas disyuntivas, este techo es tan bajo (a menudo $\top$) que vuelve inútil el mecanismo para escenarios comunes como el intercambio de secretos o los muros éticos donde un valor se usa múltiples veces.
• Para la precisión: El artículo proporciona una solución constructiva (especialización diferida) que recupera la precisión perdida. Muestra que al mantener el tipo universal en el Objeto de Conjunto ($U$) y aplicar el etiquado solo al final, se pueden certificar programas que el paradigma de renombrado rechaza.
• Implicación práctica: La distinción entre "una fuente leída dos veces" (segura bajo políticas disyuntivas) y "dos fuentes leídas una vez" (insegura) se preserva solo mediante el Objeto de Conjunto. El objeto de multiconjunto (amigable con el renombrado) y el objeto de local (amigable con los retículos) fallan en distinguir estos casos correctamente en el contexto de las políticas disyuntivas.

Los autores concluyen que, mientras que el objeto de la era de los retículos es un cociente que pierde la disyunción de rama, y el objeto de multiconjunto pierde la correlación de misma fuente, el Objeto de Conjunto ($U$) es el único que retiene ambos. El costo de esta precisión es la pérdida de la propiedad de renombrado, una compensación que es necesaria para la ejecución de políticas disyuntivas. El artículo no pretende resolver el problema para análisis relacionales o mecanismos sensibles a la ruta (que se sugieren como direcciones futuras en trabajos relacionados), sino que caracteriza plenamente los límites y posibilidades de la familia de atributos independientes.