AeonBox: Logical Guardrails for Agents by Alcides Fonseca

AeonBox: Logical Guardrails for Agents

In this post I will explain why current permissions in agents are not sufficient, why that can cause the lethal trifecta issue, and how liquid types as a sandbox mechanism can address this limitation.

Permissions and Agents

The most powerful feature of agents is also its downfall for many critical applications: access to the terminal, files, your computer or the internet.

Whenever you use an agent for coding, you are always prompted for permission for every single terminal command it wants to execute — of course! it could run rm -rf / or delete your production database. But this does not last for long, as we know from several decades of research. If security compromises the productivity of users, they use all the tricks to reduce that barrier.

So in practice, your agent shows you 5 harmless commands that you accept, and as the gains of agents become limited by the need for you to babysitting it, you switch to --dangerously-skip-permissions or --yolo mode, removing any constraint on permissions.

Data suggests that manual review can become habitual: users approve 97% of permission prompts in Claude Code. While most prompts are likely for safe, routine commands, an approval rate that high suggests many users are clicking through reflexively rather than reviewing each command.

— Anthropic

Anthropic and other companies noticed this and have worked on a compromise: now whether or not it shows the user a permission request is driven by another LLM classifying whether each external call should be allowed or a permission requested.

However, this guardian LLM is not guaranteed to always work, as it is probabilistic in nature. Worse, because it shares the same training data (and maybe similar architectural blocks) with the agent, it shares the same bias and it is probable that it fails in the same cases where the agent LLM also failed in generating the wrong command.

As such, we cannot 100% trust this guardrail system. Which might be okay for developing your personal webpage, but not okay when dealing with critical data, such as healthcare, defense or even something as simple sharing your proprietary data.

Lethal Trifecta

Most modern agents are prone to a type of attack called the lethal trifecta. This attack surface occurs when you have three things:

Access to (your) private data

Exposure to untrusted content (i.e., reads internet information)

The ability to send information to the outside

Let’s say your Claude agent has access to your GitHub account, where you have both public and private repos. You it to be able to read information from repos in the internet (open source projects), your public repos (so it can contribute to open-source) and your private repos (so it helps you on your day job). But when all these permissions are put together, it can: search for something on the internet (that you cannot control), and it comes back with instructions to read from your private repo (it has permissions) and publish all its code in one of your public repos.

This is not just a fantasy scenario. Microsoft leaked customer emails. Claude Cowork also exfiltrated files.. Microsoft Copilot Cowork also exfiltrated private information. Supabase MCP exfiltrated all their database. Simon Willison keeps track of several of these reports.

The main point here is that our current guardrails are either very granular (per-request permission), or too coarse (per-application/agent) permissions. We need more. We need behavioral permissions.

Liquid Types as behavioral permissions

I have been looking into Liquid Types during the last 8 years. My original idea is that we can model extra information in the type-system, rejecting programs not only for passing an integer where a string was expected, but also to use objects in invalid states. As the saying goes, "You should make invalid states unrepresentable" (attributed to Yaron Minsky according to my google research).

I have worked on three systems with Liquid Types (aeon, LiquidJava and ROSpec). I will use aeon as an example:

def divide (x:Int) (y:Int | y != 0) { ?implementation }

If you call divide 4 0 you will get a compiler error because divide only accepts a second argument different than 0. If you call let z = read_input in divide 4 z it will fail, because read_input returns an integer and there is no proof that it is different than zero. Because there is a chance of it being zero, the program is rejected. Now you could do something like let z = read_input in if z = 0 then 0 else divide 4 z, it will work because on the else branch, we know z to be different than 0, so we can build a proof.

Liquid Types is the type theory that allows us to write these refinements on types, and to reason about programs. If you have heard of Lean, Liquid Types are not as powerful (they stay in the decidable logic), but they use SMT solvers to generate the proof while in Lean you (or...