🤖 AI

Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI

Este artículo presenta una corrección verificada por máquina de un marco de trabajo de 2018 para la semántica epistémica de las políticas de flujo de información, lograda con la asistencia de un asistente de codificación de IA agéntica, para proporcionar una base robusta y general para especificar y aplicar requisitos de seguridad expresivos.

Autores originales: David A. Naumann

Publicado 2026-08-04

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: David A. Naumann

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

Los guardianes de los secretos y el susurro digital

Imagina un mundo donde cada programa informático es una ciudad bulliciosa, y la información es la moneda que fluye por sus calles. En esta ciudad, algunos secretos son tan valiosos —como una llave maestra o una contraseña— que nunca deben abandonar una bóveda específica. Este es el reino de la seguridad del flujo de información, una rama de la informática dedicada a garantizar que los datos sensibles no se filtren accidentalmente (o de forma malintencionada) hacia los ojos equivocados. Pero la vida no siempre es en blanco y negro. A veces, un secreto necesita ser compartido, pero solo bajo condiciones muy específicas. Tal vez un banco quiere decirle a un cliente que su cuenta está segura, pero solo después de que haya respondado correctamente a una pregunta de seguridad. Este delicado acto de equilibrio se llama degradación (downgrading): tomar un secreto de alto nivel y reducir cuidadosamente su nivel de protección para que pueda ser visto, pero solo cuando las reglas lo permitan.

Para dar sentido a estas complejas reglas, los científicos utilizan una rama de la lógica llamada lógica epistémica. Piensa en esto como la "lógica del conocimiento". En lugar de preguntar simplemente "¿Qué pasó?", pregunta "¿Qué sabe el observador?". Si un hacker está vigilando la ciudad, ¿qué puede deducir sobre los secretos en la bóveda basándose en el tráfico que ve? El desafío siempre ha sido escribir un libro de reglas perfecto que diga exactamente cuándo se puede compartir un secreto sin crear un vacío legal. Durante años, los investigadores intentaron construir un marco matemático para esto, pero los planos seguían teniendo grietas. Si las matemáticas están mal, la seguridad es una ilusión.

Reparando el plano con un asistente robot

Este artículo cuenta la historia de cómo un investigador, David Naumann, se asoció con un asistente de codificación de inteligencia artificial para arreglar un plano roto de estas reglas de seguridad. El plano original, publicado en 2018, fue un intento ingenioso de definir exactamente cuándo se le permite a un programa "desclasificar" un secreto. Utilizaba un concepto llamado anotaciones relacionales, que son como notas adhesivas colocadas en el código que dicen: "Está bien mostrar este secreto si el lanzamiento de la moneda aleatoria cayó en cara". La idea era que si dos ejecuciones diferentes del programa coincidían en el lanzamiento de la moneda, podrían coincidir en mostrar el secreto.

Sin embargo, cuando se presentó el artículo original, el autor se dio cuenta de que había un fallo significativo en su demostración. Era como construir un puente que parecía robusto pero colapsaba bajo un tipo específico de viento. El autor había esbozado una corrección, pero los detalles eran desordenados y no verificados. Este artículo toma ese esbozo y lo convierte en una estructura sólida e inamovible.

El principal hallazgo aquí es una demostración verificada por máquina. El autor no solo escribió las matemáticas en papel; las introdujo en un programa informático llamado Rocq (un asistente de demostración) que actúa como un tutor de matemáticas hiperatento. Este tutor robot revisó cada uno de los pasos de la lógica para asegurar que no hubiera brechas ocultas. El resultado es un marco corregido que demuestra: si un programa sigue un conjunto específico de reglas de "seguridad" (que son fáciles de verificar mientras el programa se ejecuta), entonces está matemáticamente garantizado que sea seguro según las complejas reglas de "conocimiento".

El artículo descarta explícitamente la idea de que la prueba de 2018 fuera correcta tal como fue escrita. Muestra que la definición anterior de "política de liberación" (el libro de reglas para cuándo se pueden compartir los secretos) era defectuosa porque no tenía en cuenta todas las formas en que un programa podría quedarse trabado o divergir. El autor argumenta que no se puede confiar simplemente en la intuición humana sobre estos complejos escenarios de múltiples ejecuciones; se necesita que la máquina verifique cada posibilidad.

El detective y la coartada

Para entender cómo funciona esto, imagina a un detective (el sistema de seguridad) tratando de averiguar si un sospechoso (el programa) está filtrando secretos. El detective tiene dos herramientas: Seguridad (Safety) y Seguridad (Security).

Security (Seguridad de objetivo) es la meta final: "El sospechoso no le dijo a nadie nada que no debía saber". Esto es difícil de probar porque tienes que imaginar cada escenario posible en el que el sospechoso pudo haber estado.
Safety (Seguridad de proceso) es una comprobación local más simple: "¿Siguió el sospechoso las reglas paso a paso a medida que avanzaba?".

El gran avance del artículo es demostrar que Safety implica Security. Si el programa sigue las reglas de "Safety" (que son como una lista de verificación de "coartadas" para cada paso), entonces la compleja garantía de "Security" se cumple automáticamente. Es como demostrar que si un conductor nunca se salta un semáforo en rojo o excede la velocidad (Safety), nunca causará un tipo específico de accidente (Security).

El autor utilizó un asistente de codificación de IA agéntica (específicamente una herramienta llamada Claude Code) para ayudar a escribir el código de la demostración en Rocq. Esto no fue solo un corrector ortográfico; la IA ayudó a traducir los desordenados bocetos matemáticos en código riguroso e incluso encontró algunos de los propios errores del autor. Por ejemplo, la IA señaló que una definición para la "divergencia" (cuando un programa se queda atrapado en un bucle infinito) era demasiado estricta y necesitaba ser relajada para que la demostración funcionara. La IA también intentó "hacer las suposiciones más fuertes de lo necesario", pero el autor humano la detectó y corrigió el rumbo.

El resultado: Un libro de reglas verificado

El artículo concluye que el marco corregido es sólido. La demostración verificada por máquina confirma que la idea original iba por el buen camino, pero los detalles necesitaban una revisión mayor. El nuevo marco permite una "política de liberación" que está claramente definida y separada de la propia comprobación de seguridad. Esto significa que los desarrolladores pueden escribir su código con sentencias "assume" (como "asuma que el usuario ha iniciado sesión") y tener la garantía matemática de que estas suposiciones controlan correctamente lo que se revela de los secretos.

El autor está muy seguro de este resultado porque ha sido verificado por máquina. Esto no es una simulación o una sugerencia; es una prueba formal de que la lógica se sostiene bajo el escrutinio de una computadora. Admite, sin embargo, que el código es actualmente un poco desordenado y necesita una limpieza humana para ser verdaderamente legible, de forma muy parecida a un brillante pero garabateado papel de servilleta que necesita ser transcrito a un libro limpio.

Al final, este artículo es una victoria para la precisión. Demuestra que incluso en el mundo abstracto de la seguridad informática, donde la lógica puede volverse increíblemente enredada, podemos usar tanto la visión humana como la asistencia de la IA para construir una base matemáticamente inquebrantable. Convierte un boceto tembloroso en una fortaleza verificada, asegurando que cuando decidimos compartir un secreto, lo hagamos exactamente cuando queremos, y no un momento antes.

Resumen Técnico: Asumiendo que lo Sabías: Corrigiendo una Semántica Epistémica para Políticas de Flujo Usando IA Agéntica

1. Planteamiento del Problema

Los requisitos de seguridad de alto nivel relativos al flujo de información, particularmente aquellos que involucran la degradación selectiva (desclasificación), son notoriamente difíciles de formalizar con precisión. Si bien la lógica epistémica ha emergido como un marco prometedor para definir la confidencialidad (lo que un observador en un nivel de privilegio específico tiene permitido saber), un marco robusto y general para políticas de flujo expresivas ha permanecido elusivo.

Un trabajo previo, referido como CN (Naumann et al., CSF 2018), intentó proporcionar un marco unificador para modelos de programas reactivos. En CN, las políticas se expresaban mediante sentencias assume dentro del código, mientras que la política de liberación derivada se expresaba únicamente en términos de flujos de entrada. Sin embargo, la formalización en CN contenía un error significativo en su demostración, anunciado durante la presentación en la conferencia. La definición original de la política de liberación y la subsecuente prueba de que la seguridad implica la protección eran imprecisas e incorrectas. Además, las adaptaciones existentes verificadas por máquina (por ejemplo, Murray et al. para programas C concurrentes) suelen depender de propiedades fuertes como la ejecución en tiempo constante, lo que trivializa las complejidades de alinear múltiples ejecuciones requeridas para el razonamiento epistémico.

El desafío central es proporcionar una formalización corregida y verificada por máquina que:

Revise la semántica epistémica para manejar correctamente la degradación dependiente del estado.
Defina explícitamente la semántica de una política de liberación derivada de las anotaciones del código.
Demuestre que una propiedad orientada al programa llamada seguridad (safety) implica la propiedad epistémica de protección (security).

2. Metodología

El autor emplea un enfoque de verificación formal utilizando el asistente de pruebas Rocq (anteriormente Coq). La metodología involucra:

Modelo de Programa: Un pequeño lenguaje imperativo reactivo con manejadores de entrada para niveles de seguridad específicos. Los programas consumen flujos de entrada y producen salidas.
Anotaciones: El marco utiliza aserciones relacionales (assert) y suposiciones (assume) para especificar requisitos de flujo de información. Estas anotaciones permiten flujos condicionales que se desvían de la política base de no-interferencia.
Semántica Epistémica: La seguridad se define en términos del conocimiento de un observador. Un observador en el nivel $\ell$ conoce un conjunto de historias de entrada posibles consistentes con sus observaciones visibles (entradas y salidas en niveles $\ell' \sqsubseteq \ell$ ).
Política de Liberación ( $RP_\ell$ ): Definida como el conjunto de listas de entrada que un observador tiene permitido aprender, derivado de las sentencias assume en el código. Esta política se interpreta mediante alineaciones entre una pre-ejecución "mayor" (ejecución real) y pre-ejecuciones "menores" (posibles ejecuciones con diferentes entradas).
Condición de Seguridad (Safety): Una propiedad orientada al programa definida por la ausencia de "fallos" (fallos de aserción, fallos de alineación) o la presencia de "fiats" específicos (fiats de suposición, fiats de divergencia) al comparar una ejecución mayor contra todas las posibles ejecuciones menores.
IA Agéntica de Asistencia: La formalización fue desarrollada con la ayuda de Claude Code, un asistente de codificación de IA agéntica. La IA fue guiada para traducir definiciones de LaTeX a especificaciones de Rocq y asistir en la construcción de pruebas, aunque requirió una curaduría humana significativa para corregir errores lógicos, refinar definiciones y gestionar la estrategia de la prueba.

3. Contribuciones Clave

A. Semántica Epistémica Corregida

El artículo presenta una formalización revisada de la semántica epistémica para las políticas de flujo. Las revisiones técnicas clave incluyen:

Definición de la Política de Liberación: La definición de la política de liberación $RP_\ell(gs)$ se corrige para ser un predicado sobre pre-ejecuciones (prefijos de ejecución finitos) en lugar de solo trazas de eventos observados. Se define mediante semi-conformidad: una relación entre una pre-ejecución mayor y pre-ejecuciones menores que las alinea en puntos de anotación específicos.
Seguridad Independiente del Progreso: El marco adopta una definición de seguridad insensible al progreso. Utiliza una noción de conocimiento de progreso ( $k_\ell^\to$ ) para manejar la divergencia, asegurando que las garantías de seguridad se mantengan incluso si el programa diverge, siempre que la divergencia misma no filtre información sobre las entradas ocultas.
Programas Bien Especificados: El autor introduce "anotaciones de boilerplate" (suposiciones al inicio de los manejadores y aserciones antes de las salidas) para agilizar la formalización y asegurar que las políticas base se codifiquen sin alterar el comportamiento observable.

B. La Seguridad (Safety) Implica la Protección (Security)

El resultado teórico central es el Teorema 2: Para todo nivel $\ell$ , cualquier pre-ejecución que sea segura (safe) para $\ell$ es protegida (secure) para $\ell$ .

La Seguridad (Safety) se define como la ausencia de fallos de aserción/alineación y la presencia de fiats válidos (de suposición o de divergencia) para cualquier lista de entrada alternativa.
La prueba demuestra que si un programa es seguro, el conjunto de entradas que un observador aprende ( $k_\ell$ ) es un subconjunto de las entradas permitidas por la política de liberación ( $RP_\ell$ ), interceptado con el conocimiento de progreso.
Este resultado valida el enfoque de imponer la seguridad mediante la verificación relacional de las anotaciones del programa en lugar de un monitoreo en tiempo de ejecución complejo de todas las ejecuciones posibles.

C. Verificación Verificada por Máquina

Todo el desarrollo, incluyendo las definiciones corregidas y el teorema principal, ha sido verificado por máquina en Rocq. Esto confirma que las correcciones a la definición de CN son fundamentalmente sólidas, mientras que también descubre detalles sutiles en las pruebas que fueron omitidos en los esquemas originales escritos por humanos.

D. Experiencia con IA Agéntica

El artículo documenta el uso de una IA agéntica (Claude Code) en el proceso de formalización. El autor señala que, si bien la IA fue capaz de generar infraestructura no trivial y pruebas rutinarias, requirió supervisión humana para:

Corregir formalizaciones defectuosas de lemas (por ejemplo, el Lema 3).
Identificar y corregir brechas lógicas en la definición de "divergence fiat".
Refinar las definiciones de conocimiento ( $k_\ell$ ) para usar prefijos en lugar de igualdad, un cambio necesitado por contraejemplos encontrados por la IA.
Evitar que la IA sobre-fortaleciera las suposiciones o introdujera hipótesis de decidibilidad innecesarias.

4. Resultados

Corrección Formal: La prueba verificada por máquina confirma que la condición de seguridad revisada implica correctamente la propiedad de protección epistémica para el modelo de programa reactivo.
Resolución de Fallos de CN: Los fallos específicos del error de la prueba de CN de 2018 respecto a la alineación de ejecuciones y la definición de la política de liberación han sido resueltos.
Viabilidad de la Formalización Asistida por IA: El estudio demuestra que la IA agéntica puede asistir eficazmente en la traducción de especificaciones matemáticas complejas en pruebas verificadas por máquina, siempre que el experto humano guíe activamente la herramienta, corrija sus errores lógicos y gestione la arquitectura general de la prueba.

5. Significado y Reivindicaciones

El artículo reclama contribuciones modestas pero significativas:

Marco Unificador: Ofrece un marco corregido y general para expresar y verificar políticas de flujo expresivas utilizando lógica epistémica y anotaciones relacionales.
Verificación Práctica: Al mostrar que la seguridad (safety) (una propiedad susceptible de monitoreo en tiempo de ejecución y prueba inductiva) implica la protección (security), este trabajo cierra la brecha entre las especificaciones de políticas de alto nivel y las propiedades de programa ejecutables.
Fiabilidad de la Verificación por Máquina: El trabajo subraya la necesidad de la verificación por máquina, incluso para desarrollos teóricos en entornos idealizados, ya que expone errores sutiles que la revisión humana podría pasar por alto.
IA en Métodos Formales: Proporciona un caso de estudio concreto del uso de IA agéntica para desarrollos formales sustanciales, destacando tanto el potencial de ganancias de eficiencia como la necesidad crítica de la experiencia humana para asegurar el rigor lógico.

El autor establece explícitamente que el desarrollo de reglas de prueba composicionales para la condición de seguridad sigue siendo un problema abierto, y que el trabajo actual se centra en la semántica fundacional y el teorema de implicación principal. El artículo está dedicado a David Basin, reconociendo su papel pionero en la formalización verificada por máquina.