The LLMbda Calculus: AI Agents, Conversations, and Information Flow
Zac Garby, Andrew D. Gordon, David Sands
Why It Matters
What makes this one worth your time
This work is relevant for AI engineers and researchers focused on enhancing the security and reliability of LLM agents, particularly in environments where data provenance and information flow are critical.
LLMbda offers a novel calculus for secure LLM agent interactions with dynamic information-flow control.
Summary
The paper introduces LLMbda, an untyped call-by-value lambda calculus designed to enhance the security of large language model (LLM) agents by incorporating provenance-based defenses and dynamic information-flow control. It presents a probabilistic noninterference theorem and demonstrates the effectiveness of LLMbda on a banking benchmark, showing comparable utility to existing defenses while maintaining security.
Key contributions
- Introduction of LLMbda, a lambda calculus for secure LLM agent interactions.
- Development of a probabilistic noninterference theorem applicable to code-generating agents.
- Demonstration of LLMbda's effectiveness on a banking benchmark with strong security guarantees.
Notable insights
- The use of an untyped call-by-value lambda calculus to express provenance-based defenses.
- Incorporation of dynamic information-flow control with labeled values for enhanced security.
Possible limitations
- Not stated in the abstract
Abstract
arXiv:2602.20064v2 Announce Type: replace-cross Abstract: Large language models are increasingly deployed as agents: they plan, call tools, read untrusted data, and act on the results. This exposes them to prompt injection: data meant only to be read is obeyed as an instruction. The most principled defences replace content inspection with provenance: classifying data by source and keeping trusted and untrusted apart through a separation of duty (the dual-LLM pattern) and information-flow control. Yet the leading systems are hard to fully trust: flow tracking is easy to get wrong, deliberate relaxations are hard to audit, and the dual-LLM pattern is hard-wired into the architecture. We present LLMbda, an untyped call-by-value lambda calculus that makes provenance-based defence both expressible and provably sound, without committing to an architecture. It adds the operational core of agentic systems as first-class constructs: prompt-response conversations that can be forked and cleared, code generation, and dynamic information-flow control in which every value carries a label that every reduction propagates. Isolation becomes a policy a program expresses, and reclassification an explicit, auditable construct. Our central result is a termination-insensitive probabilistic noninterference theorem over the whole calculus, including code-generating agents, with an insulated variant that holds even when the attacker chooses all untrusted inputs. The verified interpreter is itself the harness that calls the model, to our knowledge the first LLM agent harness whose executable is the subject of machine-checked security theorems, so every agent inherits the guarantee. On the AgentDojo banking benchmark, an agent built within LLMbda, enforcement always on, matches the utility of CaMeL, a leading dual-LLM defence, run without its policy checks (which halve its utility), and resists all but two of 1296 attacked runs. Our harness and all proofs are in Lean.