Security Engineering in IIIf, Part II -- Shadowing the IIIf

Resumen Técnico: Sombreando al Insider de Isabelle y el Marco de Infraestructura

Planteamiento del Problema
El Marco de Infraestructura e Insider de Isabelle (IIIf) proporciona una base formal para la ingeniería de seguridad de sistemas que involucran actores humanos, políticas y componentes físicos/lógicos, utilizando un ciclo de Refinamiento-Riesgo (RR). Si bien el IIIf soporta el refinamiento basado en trazas y la preservación de propiedades para propiedades de seguridad estándar (p. ej., alcanzabilidad), enfrenta una limitación crítica con respecto al Control de Flujo de Información (IFC). Específicamente, la propiedad de No Interferencia (NI) —que asegura que los estados de alta seguridad (secretos) no influyan en las observaciones de baja seguridad (públicas)— no se preserva generalmente bajo el refinamiento de la especificación. Este fenómeno, conocido como la "paradoja del refinamiento", significa que una especificación que satisface la NI puede dar lugar a una implementación refinada que filtra información a través de flujos implícitos. Los enfoques de verificación de modelos existentes dentro del IIIf son insuficientes para verificar tales propiedades de conjuntos de trazas, lo que requiere una nueva metodología para caracterizar y garantizar refinamientos seguros.

Metodología
Para abordar la paradoja del refinamiento, el artículo introduce una formalización del concepto de "Sombra" (Shadow) de Morgan en el marco IIIf. La metodología procede a través de los siguientes pasos:

1. Integración de Caso de Estudio: Los autores utilizan una especificación de un sistema de radar de vuelo (previamente formalizada en IIIf) como un ejemplo continuo. Este sistema involucra posiciones de aeronaves, rutas y ubicaciones críticas. La especificación inicial demuestra cómo ocurren los flujos de información implícitos cuando una aeronave elude una ubicación crítica, revelando la existencia de esa criticidad a través de irregularidades observables en la trayectoria de vuelo.
2. Formalización de la No Interferencia (NI): La NI se define dentro de IIIf como una relación de indistinguibilidad sobre las transiciones de estado. Dos estados son indistinguibles para un atacante (con nivel de autorización $a$) si sus componentes observables (aquellos con etiquetas de seguridad $\leq a$) son idénticos. La NI se cumple si, para cualquier par de estados iniciales indistinguibles, sus trazas de ejecución subsecuentes permanecen indistinguibles.
3. Definición de la Sombra: Inspirado en la lógica epistémica de Morgan, se define una "Sombra" como el conjunto de todos los valores posibles que un componente de estado de seguridad crítica podría tener desde la perspectiva del atacante.
   • Inicialización: Un componente de sombra se inicializa con el "universo" de su tipo (todos los valores posibles), representando la máxima ignorancia.
   • Reducción (Shrinking): Durante las transiciones de estado, la sombra se "reduce" (disminuye el conjunto de valores posibles) solo si la transición revela información sobre el componente secreto al atacante.
   • Invariante: Un sistema seguro debe satisfacer el invariante $IFC_a$, donde la sombra de un componente secreto no se reduce durante la ejecución. Si la sombra se reduce, implica que el atacante ha ganado conocimiento sobre el secreto, indicando una violación de la NI.
4. Prueba de Equivalencia: El artículo establece formalmente (en papel, debido a las limitaciones de cuantificación de tipos en Lógica de Orden Superior) que el invariante de la sombra es equivalente a la No Interferencia ($NI_a$). Específicamente, se demuestra que la negación de la NI (la existencia de un flujo de información ilícito) es equivalente a la existencia de un componente cuya sombra se reduce.
5. Caracterización del Refinamiento Seguro: Los autores definen una condición para el refinamiento seguro. Un refinamiento de un sistema abstracto $A$ a un sistema concreto $C$ preserva la seguridad si el mapa de refinamiento $E$, cuando se restringe a los componentes de sombra de $C$, es inyectivo y compatible con la sombra abstracta.

Contribuciones Clave

• Formalización de la Sombra en IIIf: El artículo extiende el IIIf con una definición formal de componentes de "Sombra" para estados de infraestructura, permitiendo el seguimiento de la incertidumbre de un atacante respecto a los componentes de estado secretos.
• Equivalencia de Sombra y NI: Demuestra que la invariante de la sombra ($IFC_a$) es equivalente a la propiedad de No Interferencia ($NI_a$) dentro del contexto del modelo de transición de estados de IIIf.
• Teorema de Refinamiento Seguro (Teorema 2): La contribución principal es un teorema que caracteriza el refinamiento seguro. Establece que si un mapa de refinamiento $E$ es inyectivo en los componentes de sombra del sistema concreto y es compatible con la sombra abstracta, entonces la invariante de la sombra (y, por tanto, la NI) se preserva desde el sistema abstracto al sistema concreto.
• Resolución de la Paradoja del Refinamiento: La metodología proporciona un mecanismo para verificar que un paso de refinamiento no introduzca nuevos flujos de información que violen la NI, abordando un fallo conocido en el ciclo RR estándar de IIIf.

Resultados

• Aplicación al Sistema de Radar de Vuelo: Los autores aplican la definición de sombra al caso de estudio del sistema de radar de vuelo.
  • En una versión insegura (sin mecanismos de ocultación), la sombra del componente de ubicación crítica se reduce cuando un avión elude un área crítica, demostrando la violación de $IFC_a$ y la NI.
  • En una versión asegurada (usando un componente critpos para ocultar la elusión real), el invariante de la sombra se mantiene, confirmando la ausencia de flujos ilícitos.
• Análisis de Refinamiento: El artículo demuestra que añadir un nuevo componente (p. ej., "velocidad") calculado basándose en posiciones ocultas constituye un refinamiento inseguro porque causa que la sombra se reduzca, violando las condiciones de inyectividad/compatibilidad del Teorema 2. Por el contrario, muestra que añadir componentes que no dependen de secretos y que son manejados correctamente por el mapa de refinamiento preserva la seguridad.
• Límites Meta-Teóricos: Los autores señalan que, si bien la equivalencia entre Sombra y NI puede razonarse, la formalización completa del teorema de equivalencia sobre todos los tipos de infraestructura está limitada por el sistema de tipos de Isabelle/HOL, ya que requiere la cuantificación sobre componentes de diferentes tipos del estado.

Significancia y Reivindicaciones
El artículo afirma extender las capacidades de ingeniería de seguridad del marco IIIf mediante la integración del Control de Flujo de Información. Su significancia radica en:

1. Abordar la Paradoja del Refinamiento: Ofrece una metodología concreta para asegurar que las propiedades de seguridad (específicamente la NI) se preserven durante el proceso de refinamiento, una capacidad que carecía el marco anteriormente.
2. Puente entre Abstracción e Implementación: Al utilizar el concepto de sombra, el marco puede ahora razonar formalmente sobre la "ignorancia" de un atacante y asegurar que los refinamientos no reduzcan inadvertidamente dicha ignorancia (es decir, filtren información).
3. Verificación Práctica: El enfoque permite la verificación de sistemas complejos y heterogéneos (que combinan aspectos físicos y lógicos) donde la verificación de modelos estándar falla.

Los autores mantienen la modestia respecto al alcance, reconociendo que las pruebas de equivalencia se establecen actualmente "en papel" debido a las restricciones de la teoría de tipos en Isabelle/HOL, y que la metodología está diseñada específicamente para el modelo de infraestructura IIIf en lugar de una lógica de lenguaje de programación de propósito general. El trabajo se basa en los conceptos fundacionales de Morgan pero los adapta a un sistema de transición de estados con actores y políticas explícitos, evitando la necesidad de una lógica epistémica dedicada al aprovechar el modelo de derechos de acceso de actores ya existente en IIIf.