Un cálculo lambda que prueba la resistencia de los agentes a la inyección

¿De qué se trata?

La mayoría de las defensas contra la inyección de prompts son empíricas: un clasificador, una barrera, un filtro que intenta detectar la entrada maliciosa. Funcionan hasta que un atacante encuentra la formulación que se les escapa. Un artículo de Zac Garby, Andrew D. Gordon y David Sands toma otro camino. Publicado en arXiv en febrero de 2026 y reanunciado en una versión actualizada el 13 de julio de 2026, introduce un pequeño lenguaje formal — un cálculo lambda — para lo que realmente son los agentes de IA modernos: código que entrelaza llamadas a LLM, invocaciones de herramientas y más cómputo, construyendo una conversación a medida que se ejecuta.

La ventaja de un cálculo es que permite demostrar propiedades. En lugar de sostener que una defensa probablemente ayuda, los autores definen con precisión qué significa un programa de agente y luego prueban un teorema sobre qué entradas pueden influir en qué salidas. Es un trabajo de fundamentos, no un exploit: ofrece a quienes diseñan marcos de agentes una forma rigurosa de razonar por qué una inyección puede o no alcanzar una acción peligrosa.

Cómo funciona

La idea central consiste en tratar al LLM como una primitiva ordinaria de un lenguaje de programación. El cálculo extiende el cálculo lambda no tipado con una operación que invoca un modelo: serializa un valor, lo envía al LLM como prompt y analiza la respuesta para convertirla en un nuevo término que el programa sigue evaluando. Como la salida del modelo reingresa al programa en forma de código y de datos, el acoplamiento estrecho entre razonamiento y acción se hace explícito en vez de quedar oculto en el marco.

Sobre esa base, el lenguaje añade dos familias de primitivas. La primera gestiona las conversaciones como objetos de primera clase: se puede extender la conversación actual, hacer fork de una subconversación nueva que no hereda el contexto previo, o clear del historial acumulado. La segunda rastrea el flujo de información: los términos pueden etiquetarse y consultarse, de modo que la semántica registra de dónde procede un valor y qué tiene permitido influir.

Con las conversaciones y las etiquetas dentro de la semántica, defensas que suelen ser informales se vuelven precisas. Una subconversación en cuarentena es un fork cuyo contenido no confiable queda aislado, de modo que no puede reescribir las instrucciones del padre. El aislamiento del código generado significa que la salida producida por el modelo no puede ejecutarse con la autoridad del código de confianza. Y las restricciones de flujo de información limitan lo que puede llegar a una llamada al LLM en primer lugar: un dato no confiable puede leerse, pero no se le permite dirigir una decisión privilegiada. El resultado central del artículo es un teorema de no interferencia insensible a la terminación: bajo estas restricciones, una entrada de baja integridad no puede corromper una salida de alta integridad, y los valores confidenciales no pueden filtrarse hacia canales que no deberían verlos. Es la misma propiedad de integridad y confidencialidad que persigue la seguridad clásica por flujo de información, ahora enunciada y probada para conversaciones de agentes.

Por qué importa

La inyección de prompts persiste porque las defensas habituales razonan sobre cadenas de texto — ¿parece malicioso este texto? — mientras que el fallo real trata sobre la autoridad: un dato no confiable termina influyendo en una acción de confianza. Un cálculo que separa ambas cosas permite al autor de un marco enunciar la propiedad que desea («nada de lo que un agente lee en la web puede desencadenar un pago») y verificar que su diseño la impone, en lugar de esperar que un filtro atrape cada formulación.

También ofrece un vocabulario común. Patrones que los equipos reinventan caso por caso — la división dual-LLM, la cuarentena de las salidas de herramientas, la ejecución de código con capacidades acotadas — se reducen a las mismas primitivas subyacentes de fork de conversación y etiquetado de flujo. Poder nombrarlos y componerlos es lo que convierte mitigaciones dispersas en una arquitectura, y lo que permite comparar dos sistemas por algo más que impresiones. Para quienes construyen agentes de código, asistentes RAG y flujos multiherramienta, la lección es que la resistencia a la inyección puede ser una garantía de diseño, y no solo un parche en tiempo de ejecución.

Conviene enunciar los límites con claridad. Una prueba vale para el modelo que describe: el teorema restringe los programas escritos en el cálculo, y un despliegue real solo hereda la garantía en la medida en que su runtime implemente fielmente esa semántica — etiquetas propagadas con honestidad, forks realmente aislados, código generado efectivamente privado de autoridad. El cálculo no hace que el LLM rechace una mala instrucción; asegura que el contenido no confiable nunca obtenga el rango necesario para emitir una.

Defensas

Haga de la procedencia, y no de la formulación, el punto de control. Etiquete los datos según su origen y exija que las fuentes no confiables no puedan influir en llamadas a herramientas privilegiadas, reflejando las restricciones de flujo de información que formaliza el artículo.

Aísle el trabajo no confiable en subconversaciones en cuarentena. Cuando un agente deba leer una página web, un documento o el resultado de una herramienta de confianza desconocida, procéselo en un contexto aislado que no pueda reescribir las instrucciones de la conversación padre, y devuelva solo un resultado verificado y mínimo.

Niegue al código generado la autoridad del código de confianza. Todo lo que el modelo produzca y usted luego ejecute debe correr con capacidades reducidas y concedidas de forma explícita — nunca con los privilegios ambientales del host del agente.

Prefiera diseños cuya propiedad de seguridad pueda enunciar. Si no puede escribir qué entradas tienen permitido afectar a qué acciones, no puede saber si un filtro cierra la brecha o solo la estrecha. Use las primitivas del cálculo — aislamiento de conversaciones y etiquetado de flujo — como lista de verificación al revisar la arquitectura de un agente.

Estado

Elemento	Detalle
Publicación	Preprint de arXiv, febrero de 2026; versión actualizada anunciada el 13 de julio de 2026
Autores	Zac Garby, Andrew D. Gordon, David Sands
Naturaleza	Fundamentos formales / investigación defensiva — sin vulnerabilidad, sin exploit, sin CVE
Resultado clave	Teorema de no interferencia insensible a la terminación para conversaciones de agentes (integridad + confidencialidad)
Primitivas	Término de llamada al LLM; gestión de conversación (extender, fork, clear); etiquetas de flujo de información
Contexto	Charla COPLAS, Universidad de Copenhague