Calculus grounds safer LLM agents and conversations
New research proposes LLMBDA, a formal model for Large Language Model (LLM) agents that interleave prompts, tool calls and code. It captures how prompt injection propagates and proves noninterference guarantees under clear conditions. The authors also show practical defences: quarantined sub-conversations, isolated generated code, and label-checked tool interfaces.
Agent frameworks now stitch together Large Language Model (LLM) calls, tool invocations and bits of generated code. That convenience creates a close coupling that attackers can exploit through prompt injection. We have patterns and patches, but not much in the way of first principles. A new paper offers exactly that: a formal calculus for agent conversations and their security properties.
What the calculus adds
The work introduces LLMBDA, an untyped call-by-value lambda calculus extended for prompt-response workflows and information-flow control (IFC). It models a primitive that calls an LLM by serialising a value into a prompt and parsing the response as a new term. Two further primitives, fork and clear, let an agent branch or quarantine conversation context. Every value and conversation carries confidentiality and integrity labels drawn from a join-semilattice, so the semantics can track what influences what.
The semantics makes conversations explicit. It uses functions to erase sensitive parts, serialise prompts, generate model outputs and parse them back into terms. A big-step relation maps an initial labelled conversation to an updated one and a labelled result, which is enough to reason about how injected content can steer later computation, trigger tool calls or corrupt final outputs. The model reproduces familiar planner loops and attack paths, including an example where a prompt injection subverts a tool-calling agent.
On the defensive side, the paper formalises patterns practitioners already reach for: quarantined sub-conversations, isolation of generated code and label-based checks at tool boundaries. A dual-LLM setup appears in the examples: a privileged model generates code, while a quarantined peer processes untrusted data. Dynamic label assertions on tool APIs prevent untrusted inputs from influencing trusted outputs. The authors also implement an interpreter in Python that follows the semantics and drives an LLM via the OpenAI Responses API, providing concrete runs of these patterns.
Why this matters
The central result is a termination-insensitive noninterference (TINI) theorem. In short, information at level m cannot affect observations at level n unless the label lattice permits that flow. That covers both confidentiality and integrity in the presence of LLM calls. There is a sharp caveat on label tests: a naive, low-level boolean test of a label breaks noninterference in multi-level lattices. The paper identifies safe routes instead, such as disallowing label tests, restricting to a single non-bottom label, or ensuring tests return results at a high enough level.
If this sounds abstract, it has a familiar ring. Early information-flow work gave operating systems a way to explain, not just enforce, isolation. The macro-virus era taught us to sandbox documents and to treat generated code as suspect until proven otherwise. LLMBDA brings that lineage to agents by turning conversation state into a first-class, labelled object and by making the LLM call an explicit point of policy.
There are limits. The model assumes deterministic LLM responses, which elides sampling noise and non-determinism. Tools and external data are represented inside the language rather than as arbitrary side effects. That keeps proofs manageable, but it also means performance, latency and messy real-world integrations sit outside the frame.
For security teams, the practical thread to pull is clear enough. Treat conversation history as a data flow to be contained. Use quarantined sub-conversations when handling untrusted inputs. Isolate generated code. Put label-aware assertions on tool interfaces. If you must test labels, do so in a way that preserves noninterference. The formalism gives you a way to justify these choices, not just hope they work.
As agents take on more autonomy, we will need probabilistic semantics and richer models of tools. For now, LLMBDA offers a workable foundation for threat modelling and a common language for designing guardrails that hold up under scrutiny.
Additional analysis of the original ArXiv paper
