Relative safety of LLM Agent prompt injection: mechanized definitions, defenses, and judgments

Brijesh Dongol's paper proposes the PlanTERS framework, which defines the safety of an LLM Agent against prompt injection relative to a reference Agent: the reference Agent executes the same plan under the same runtime monitoring, but the model it uses never complies with untrusted content; an Agent is called relatively safe if every leak of that Agent is a leak that the reference Agent already has. The paper gives a fencing theorem proving that revoking injectable tools upon the first read of untrusted content and never restoring them makes all plans in finite runs relatively safe at the event level; this conclusion holds under the conditions that each injection is a single call and that the model complies according to a pre-fixed schedule, and can be extended to possibly infinite runs under a fairness condition. The authors prove or disprove the relative safety of Agents with fencing, budgets, approvals, loops, and dual LLMs in Isabelle/HOL.