Liquid Types para Sandboxing de Agentes LLM: Seguridad Comportamental en Sistemas Distribuidos

La proliferación de agentes basados en Large Language Models (LLM) en entornos de desarrollo y operación introduce un desafío fundamental en la seguridad de sistemas distribuidos: cómo otorgar a estos agentes la capacidad de interactuar con recursos externos (terminal, sistema de archivos, red) sin comprometer la integridad y confidencialidad de los datos. Los mecanismos de permisos actuales, ya sean granulares (solicitudes por comando) o gruesos (por aplicación), han demostrado ser insuficientes. La fatiga de aprobación del usuario y la naturaleza probabilística de los LLM de 'guardia' llevan a una vulnerabilidad conocida como la 'trifecta letal', donde la combinación de acceso a datos privados, exposición a contenido no confiable y la capacidad de exfiltrar información puede ser explotada. Este problema no es nuevo; los sistemas operativos han lidiado con la gestión de privilegios y el aislamiento de procesos durante décadas. La propuesta es elevar el nivel de abstracción de las políticas de seguridad, pasando de permisos reactivos a un control comportamental proactivo, utilizando sistemas de tipos avanzados como los Liquid Types para garantizar la seguridad en tiempo de compilación, antes de la ejecución de cualquier acción potencialmente dañina.

La necesidad de este enfoque se agudiza con la creciente autonomía de los agentes. A medida que los LLM evolucionan de herramientas de asistencia a componentes activos en pipelines de software, su capacidad para generar y ejecutar código arbitrario requiere un marco de seguridad que vaya más allá de la supervisión humana o de otro LLM. La naturaleza no determinista de los LLM hace que las soluciones basadas en clasificación probabilística sean inherentemente frágiles para casos de uso críticos. Por lo tanto, se busca una garantía formal, similar a las que ofrecen los sistemas de tipos estáticos en el desarrollo de software tradicional, pero extendida para razonar sobre el comportamiento y el flujo de información.

Arquitectura del Sistema

La solución propuesta se centra en la integración de Liquid Types en el entorno de ejecución de agentes, ejemplificado por AeonBox. En lugar de permitir que el agente genere código arbitrario para un shell o un SDK sin restricciones, AeonBox restringe la interacción del agente a un SDK específico (ej. GitHub SDK) que ha sido instrumentado con Liquid Types. Este SDK se define en un lenguaje que soporta tipos refinados, como Aeon. Los Liquid Types permiten añadir predicados lógicos a los tipos de datos, que son verificados por un SMT solver en tiempo de compilación. Por ejemplo, una función divide(x:Int)(y:Int | y != 0) solo aceptará un segundo argumento que se demuestre no ser cero.

Para la seguridad de los agentes, se introduce el concepto de Session como un tipo lineal. Los tipos lineales, inspirados en la lógica lineal, aseguran que un recurso (la sesión) solo tenga una referencia activa en un momento dado, evitando el uso de estados obsoletos y forzando una gestión explícita del ciclo de vida del recurso. La Session tiene una 'medida' o 'refinamiento' booleano sessionTainted, que indica si la sesión ha interactuado con datos privados. Funciones como repoRead actualizan este estado: si se lee un repositorio privado, sessionTainted se vuelve true. Crucialmente, funciones sensibles como createIssuePublic (para crear un issue público) requieren una Session con sessionTainted = false. Si el agente intenta crear un issue público después de leer un repositorio privado (lo que 'contamina' la sesión), el compilador de AeonBox, utilizando el SMT solver, rechazará el programa porque la precondición de createIssuePublic no se cumple. Este mecanismo proporciona una garantía formal de que ciertos flujos de información (ej. de privado a público) son imposibles a nivel de tipo, sin depender de decisiones en tiempo de ejecución o de la inferencia de otro LLM.

def divide (x:Int) (y:Int | y != 0) { ?implementation }

linear type Session
def sessionTainted : (s: Session) -> Bool := uninterpreted
def freshSession (_: Unit) : {s:Session | sessionTainted s = false} := native "..."
def repoRead (1 s: Session) (r: Repo) : {s2:Session | sessionTainted s2 = (repoPrivate r || sessionTainted s)} := native "..."
def createIssuePublic (1 s: {s:Session | sessionTainted s = false}) (r: {r:Repo | repoPrivate r = false}) (title: {t:String | t != ""}) (body: String) : Issue := native "..."
def closeSession (1 s: Session) : Unit := native "..."

Fundamentos Teóricos

La idea de extender los sistemas de tipos para expresar propiedades más allá de la validez estructural de los datos tiene raíces profundas en la teoría de tipos y la verificación formal. Los Liquid Types son una forma de tipos dependientes, donde los tipos pueden depender de valores. Este concepto se remonta a trabajos como los de Per Martin-Löf sobre la teoría de tipos intuicionista en los años 70, que sentaron las bases para lenguajes de prueba como Coq y Agda. Sin embargo, los Liquid Types, popularizados por Ranjit Jhala y sus colaboradores (ej. LiquidHaskell), buscan un equilibrio entre expresividad y decidibilidad, utilizando SMT (Satisfiability Modulo Theories) solvers para automatizar la verificación de los refinamientos. Esto los diferencia de sistemas de prueba más potentes como Lean, donde las pruebas a menudo requieren ser escritas explícitamente por el usuario o el agente.

El principio subyacente de 'hacer que los estados inválidos sean irrepresentables' (You should make invalid states unrepresentable), atribuido a Yaron Minsky, es una máxima fundamental en el diseño de software robusto. Los Liquid Types aplican este principio al nivel de comportamiento y flujo de información, permitiendo que el sistema de tipos rechace programas que, aunque sintácticamente correctos, violarían invariantes de seguridad o privacidad. La aplicación de tipos lineales para la gestión de recursos y el control de efectos laterales también tiene un fuerte precedente académico, derivado de la lógica lineal de Jean-Yves Girard, y se ha explorado en lenguajes como Rust para garantizar la seguridad de la memoria sin un recolector de basura. La combinación de estos conceptos académicos proporciona un marco riguroso para abordar los desafíos de seguridad en los sistemas de agentes LLM, trasladando la verificación de la seguridad de la ejecución probabilística a la verificación formal en tiempo de compilación.