An AI agent checking a confidential contract may also need a browser or messaging tool. That combination creates a security question: can the computing environment prevent sensitive information reaching an unauthorised destination, even if the agent’s own reasoning goes wrong? A new university project will try to enforce that boundary independently of the model.[1]
The University of Surrey announced on 15 October that a team involving Surrey, Sheffield and Melbourne had secured more than £3.2 million from the UK's Advanced Research and Invention Agency (ARIA). Its Agentic-seL4 project aims to construct a rigorously verified sandbox for autonomous agents. The project is part of ARIA's Safeguarded AI programme; eight projects share £22 million in the relevant cybersecurity track.[1]
Rules enforced by the environment
Formal verification tries to establish mathematically that a system obeys specified rules. That is different from testing a model with thousands of hostile prompts and finding no obvious failure. The Surrey team wants security guarantees about what agents can access, which actions they can take and how permissions can be revoked while work is underway.[1]
One example described by the researchers is an agent that has read sensitive information. Its future external communications could be blocked outright or permitted only through a trusted sanitisation step. This is an information-flow problem, not simply a question of whether the agent intends to comply. The controls must remain in force even when the agent can generate code, open files or chain together tool calls in unexpected ways.[1]
Three distinct controls an agent environment needs
| Layer | Question it answers | Why a prompt is insufficient |
|---|---|---|
| Identity and access | Which tools and files may the agent use? | The model can be mistaken about its permissions |
| Information flow | Can data reach unapproved destinations? | A prohibited disclosure can be indirect |
| Revocation and mediation | Can permission be withdrawn during execution? | An ongoing tool call may outlive its original authority |
A proof covers specified properties under stated assumptions. Its protection depends on the running system matching the verified design, including the components trusted to mediate access. This makes the size and clarity of that trusted boundary central to the project.[1]
Why permission revocation is unusually hard
An agent may start a long workflow with access that is justified at the beginning and unsafe later. Revoking permission must therefore work across processes and active tasks, not merely before the next user prompt. Another challenge is mediation: every path from confidential input to external output has to pass through the boundary. One forgotten tool, log stream or external endpoint can undermine a neatly designed policy.[1]
Trusted sanitisation is a particularly demanding part of the proposal. Blocking a direct file transfer is different from deciding which details may safely appear in a summary. The policy must identify what can leave the environment and which component is trusted to make that decision.[1]
What the funding buys now
The funding supports a proof-of-concept reference design and assessment against realistic agent-escape scenarios. Those are planned research outputs. The announcement establishes the consortium, funding and technical approach; implementation and published tests will establish the protection achieved.[1]
The proposed change is practical: organisations would grant an agent a bounded workspace whose permissions remain enforceable while it acts. Its usefulness will depend on whether the team can express a valuable security rule, prove it for the design and preserve it in the running system.
Sources & further reading
- Surrey leads £3.2m project to develop provably secure sandbox for AI agents University of Surrey · 15 Oct 2026 · Accessed 26 Oct 2026