Search papers, labs, and topics across Lattice.
The paper introduces a lambda calculus, named LLMbda Calculus, designed to model and analyze the behavior and security vulnerabilities of AI agents that interact with LLMs through prompt-response conversations. This calculus incorporates dynamic information-flow control and primitives for representing LLM calls, enabling the formalization of prompt injection attacks and potential defenses. The authors prove a termination-insensitive noninterference theorem, demonstrating the calculus's ability to provide integrity and confidentiality guarantees for safe agentic programming.
Formalizing LLM-based agent conversations with a lambda calculus reveals vulnerabilities like prompt injection and enables rigorous reasoning about defenses.
A conversation with a large language model (LLM) is a sequence of prompts and responses, with each response generated from the preceding conversation. AI agents build such conversations automatically: given an initial human prompt, a planner loop interleaves LLM calls with tool invocations and code execution. This tight coupling creates a new and poorly understood attack surface. A malicious prompt injected into a conversation can compromise later reasoning, trigger dangerous tool calls, or distort final outputs. Despite the centrality of such systems, we currently lack a principled semantic foundation for reasoning about their behaviour and safety. We address this gap by introducing an untyped call-by-value lambda calculus enriched with dynamic information-flow control and a small number of primitives for constructing prompt-response conversations. Our language includes a primitive that invokes an LLM: it serializes a value, sends it to the model as a prompt, and parses the response as a new term. This calculus faithfully represents planner loops and their vulnerabilities, including the mechanisms by which prompt injection alters subsequent computation. The semantics explicitly captures conversations, and so supports reasoning about defenses such as quarantined sub-conversations, isolation of generated code, and information-flow restrictions on what may influence an LLM call. A termination-insensitive noninterference theorem establishes integrity and confidentiality guarantees, demonstrating that a formal calculus can provide rigorous foundations for safe agentic programming.
