Alignment Contracts for Agentic Security Systems

A continuación se presenta un resumen técnico detallado del artículo "Contratos de Alineación para Sistemas de Seguridad Agénticos" de Isaac David, Marco Guarnieri y Arthur Gervais.

1. Planteamiento del Problema

El auge de los Sistemas de Seguridad Agénticos—agentes autónomos impulsados por Modelos de Lenguaje Grandes (LLM) que pueden planificar, ejecutar y validar pruebas de seguridad (por ejemplo, pruebas de penetración)—crea un problema de control asimétrico crítico.

• El Dilema: Estos agentes deben mantener capacidades ofensivas robustas (por ejemplo, explotar vulnerabilidades, sondear sistemas) dentro de un ámbito autorizado, mientras deniegan estrictamente esas mismas capacidades fuera de ese ámbito (por ejemplo, atacar objetivos no autorizados, exfiltrar datos a adversarios).
• El Fracaso de las Barreras de Seguridad Existentes: Los mecanismos de seguridad actuales (por ejemplo, filtrado de prompts, clasificación de intenciones o rechazo generalizado) son insuficientes porque:
  1. A menudo dependen de inferir la intención del agente, lo cual es poco fiable frente a la inyección de prompts adversarios o puertas traseras del modelo.
  2. Carecen de una definición formal y de primera clase de la "frontera" entre acciones autorizadas y no autorizadas basada en efectos observables.
  3. No pueden garantizar que un agente, incluso si está comprometido o manipulado, no realizará acciones dañinas si la acción en sí misma es técnicamente "permitida" por una política laxa.

El desafío central es hacer cumplir una frontera de responsabilidad donde el sistema garantice que todos los efectos realizados (solicitudes de red, accesos a archivos, ejecuciones de procesos) permanezcan dentro de las restricciones definidas por el operador, independientemente del estado interno del LLM o de la manipulación adversaria.

2. Metodología: Contratos de Alineación

Los autores proponen Contratos de Alineación, un marco formal para especificar y hacer cumplir restricciones de comportamiento sobre trazas de efectos observables.

A. Conceptos Centrales

• Alfabeto de Efectos ($\Sigma$): Un conjunto finito de clases de efectos observables (por ejemplo, NET para red, FS para sistema de archivos, EXEC para ejecución de procesos).
• Evento: Una tupla $e = \langle \sigma, p, t, i \rangle$ que representa una clase de efecto, parámetros (por ejemplo, IP de destino, método), marca de tiempo e ID del agente.
• Traza: Una secuencia finita de eventos.
• El Contrato ($C$): Una tupla que define:
  • Ámbito ($S$): Qué objetivos están autorizados.
  • Efectos Permitidos/Prohibidos ($E_{allow}, E_{forbid}$): Clases de acciones específicas permitidas o prohibidas.
  • Presupuestos ($B$): Límites de recursos (por ejemplo, máximo 10.000 solicitudes).
  • Políticas de Divulgación ($D$): Dónde pueden fluir los datos sensibles (vulnerabilidades, credenciales).
  • Costos y Flujos: Funciones de contabilidad para recursos y extracción de datos.

B. El Mecanismo de Aplicación

El sistema se basa en un Monitor de Referencia que opera bajo la Hipótesis de Observabilidad de Efectos (EOA):

1. Mediación: Todos los efectos externos deben pasar a través de una capa de mediación (por ejemplo, un envoltorio de herramientas tipado, proxy HTTP o gancho del kernel) antes de su ejecución.
2. Verificación de Admisibilidad: Para cada evento propuesto $e$ y el prefijo de traza actual $\tau$, el monitor verifica si se cumple $Adm(e, \tau, C)$. Esto implica verificar:
   • Que el objetivo esté dentro del ámbito.
   • Que el efecto esté permitido y no prohibido.
   • Que los presupuestos no se hayan excedido.
   • Que los flujos de divulgación estén autorizados.
3. Acción: Si es admisible, el evento se permite; de lo contrario, se deniega. El monitor opera puramente sobre datos observables, ignorando el razonamiento interno del LLM.

C. Fundamentos Formales

• Propiedad de Seguridad: El cumplimiento del contrato se define como una propiedad de seguridad sobre trazas finitas. Si se viola un contrato, existe un "prefijo malo" finito que testifica la violación.
• Mecanización: Los teoremas centrales se verifican utilizando Lean 4, un asistente de pruebas formales, asegurando la solidez lógica del marco.

3. Contribuciones Clave

1. Modelo Formal: Definición de Contratos de Alineación como tuplas sobre un alfabeto de efectos finito con semántica basada en trazas. El artículo demuestra la Propiedad de Testigo de Prefijo Malo Finito, asegurando que las violaciones sean detectables en tiempo finito.
2. Solidez de la Aplicación: Bajo la EOA, los autores demuestran que cualquier agente (incluso adversario, con inyección de prompts o con puertas traseras) produce únicamente trazas que satisfacen el contrato si sus efectos están completamente mediados. Esto traslada la confianza del LLM no confiable a la pequeña barrera de aplicación auditable.
3. Álgebra de Contratos:
   • Refinamiento ($C' \sqsubseteq C$): Un mecanismo para crear contratos más estrictos (ámbito más estrecho, presupuestos más ajustados) que preservan la solidez.
   • Composición Unidireccional: Reglas para combinar contratos (por ejemplo, fusionar la política organizacional con el ámbito del compromiso) con garantías de solidez demostradas.
   • Decidibilidad: El artículo establece que la verificación de admisibilidad es decidible y computacionalmente eficiente ($O(|Res|)$ en línea con almacenamiento en caché).
4. Esquema de Adaptación: Un marco para manejar cambios dinámicos del sistema (por ejemplo, creación de sub-agentes, intercambio de herramientas) definiendo reglas de adaptación "que preservan el contrato".
5. Resultados de Imposibilidad: El artículo delimita formalmente los límites del enfoque:
   • Indecidibilidad: El análisis estático previo a la admisión de si una herramienta alguna vez intenta un efecto prohibido es indecidible para lenguajes Turing-completos.
   • Límites de Bypass: Si una herramienta elude la capa de mediación (por ejemplo, mediante módulos del kernel o canales laterales), la garantía de solidez colapsa.
   • Límites de Observabilidad: Los canales encubiertos (esteganografía de carga útil, canales de tiempo) y los efectos no modelados están fuera del alcance del teorema.

4. Resultados y Evaluación

• Garantías Teóricas: El artefacto Lean 4 verifica que si el Monitor de Referencia se implementa correctamente y se cumple la EOA, el sistema es sólido. El comportamiento del LLM es irrelevante para la garantía; solo importa el efecto realizado.
• Estudio de Caso (Pruebas de Penetración Web): El marco se instanció para un escenario de pruebas de penetración web. Modeló con éxito restricciones como:
  • "Solo HTTP GET/HEAD en *.ejemplo.com".
  • "Sin operaciones en el sistema de archivos".
  • "Máximo 10.000 solicitudes".
  • "Informes solo al panel de control".
  • El monitor bloqueó correctamente los intentos de exfiltrar datos a evil.com o acceder a dominios no autorizados, incluso cuando el agente fue "inyectado con prompts" para hacerlo.
• Complejidad: Se demuestra que la verificación central de admisibilidad es de tiempo constante por evento en implementaciones prácticas (asumiendo conjuntos de recursos pequeños y fijos), lo que la hace viable para la aplicación en tiempo de ejecución.

5. Significado

Este artículo representa un cambio de paradigma en la seguridad de los agentes de IA:

• De la Intención al Efecto: Se aleja de intentar "alinear" la intención interna del LLM (lo cual es difícil y frágil) para enfocarse en hacer cumplir restricciones sobre efectos observables (lo cual es verificable).
• Confianza Formal: Al utilizar pruebas mecanizadas, proporciona una garantía matemáticamente rigurosa de que un agente no puede violar su contrato si la capa de mediación es segura. Esto reduce la Base de Computación Confiable (TCB) al monitor y a la frontera de mediación, excluyendo al LLM.
• Aplicabilidad Práctica: El marco está diseñado para flujos de trabajo reales de seguridad ofensiva, ofreciendo una manera de desplegar agentes autónomos potentes de forma segura sin temor a que causen daños colaterales o fugas de datos.
• Límites Claros: Al declarar explícitamente lo que el sistema no puede garantizar (por ejemplo, inspección del contenido de la carga útil, canales de tiempo), evita la sobreconfianza en la tecnología y guía los esfuerzos futuros de ingeniería hacia el cierre de esas brechas específicas.

En resumen, los Contratos de Alineación proporcionan el primer marco formal, decidible y mecánicamente verificado para garantizar que los sistemas de seguridad agénticos operen estrictamente dentro de los límites autorizados, transformando la "caja negra" del razonamiento del LLM en una "caja blanca" de restricciones de efectos aplicables.