Agents, leases and labels

An agent is a program that acts for a principal and is assumed hostile: an AI agent or any other automated worker. On Redoubt an agent is its own principal, never an impersonation of a person, with a sponsor who answers for it. It runs in its own beamlet VM under a lease, a budget with a kernel deadline, holding only capabilities narrowed from its launcher’s. It can start sub-agents, each narrower again and inside its own lease. Labels bound what it can leak; capabilities bound what it can do; the lease bounds for how long.

Purpose

Redoubt exists so that the most capable and most malicious agents can run on it, do real work, and not get out. This page is what that means from the agent’s side and from its sponsor’s: how an agent is started and what it holds, how long it lives, what a hijacked agent can and cannot do, how the agent harness gives it tools, and the game that tests all of it continuously.

How to use it

Alice starts an agent on a task, with a lease scoped to it:

{:ok, agent} =
  Redoubt.Agent.start(
    lease: [time: :timer.hours(2), pages: 65_536, processes: 4, weight: 20],
    labels: [],
    grants: [
      read: "~/project",
      write: "~/project/out",
      gateway: "model",
      git: {"origin", fetch: true, push: ["refs/heads/agent/*"]}
    ]
  )

Redoubt.Agent.prompt(agent, "Audit /project/src for unchecked lengths; write findings to /out")
Redoubt.Agent.status(agent)     # %{pages: ..., weight: 20, lease_ms: 6_912_000}
Redoubt.Agent.kill(agent)       # the steward ends the lease: the agent and its sub-agents end

When the agent needs more (another directory, a host to reach), it asks; the request waits for Alice at ssh approve@box (sessions).

What it can and cannot do

An agent is a principal with a sponsor

Status: built · partly tested: the sponsored principal and the leases start_agent makes run on the machine; the chain of sponsors (an agent sponsoring an agent) is not built: a sponsor is a person’s principal · tested: bench:agent-login, bench:steward-lease-ends, host:redoubt-steward::a_sponsored_principals_session_is_a_lease_of_its_sponsors

Humans, agents and projects are the same kind of principal to the steward: a named, accountable identity with a way to authenticate, a set of capabilities and an audit identity. They differ in authentication and default policy, not mechanism (the steward).

• Its own principal, never an impersonation. Every action is the agent’s own and is recorded as such, with the chain of principals above it.
• Every agent has a sponsor: a person, or an agent with a person at the top of the chain. The sponsor answers for its agents.
• Its budget sits under its sponsor’s, so it bills to the sponsor’s account (R8 (accounts)). The sponsor can destroy it at any time.
• One VM per agent. An agent is its own beamlet VM, one trust domain; a sub-agent with different authority is another VM (beamlet).
• Assume it is hijacked. Anything an agent reads may take it over. A hijacked agent can do what its capabilities allow, until its lease ends, and nothing more; it can run code it wrote, but never with more authority than it holds (packages).

Leases

Status: built · partly tested: a lease’s grants are its sponsor’s ~/project and the system volume, and the read root is writable until a server takes a read-only connection; the task-scoped grants and gateways are later · tested: bench:steward-lease-ends, bench:steward-end-lease, bench:steward-sub-agent-dies-with-agent, bench:agent-login, bench:session-tcp-loopback, bench:steward-labelled-agent-no-sink, bench:steward-agent-escape, bench:steward-lease-cut

A lease is a budget with a deadline, made by the steward for an agent or a session. When the deadline passes, the kernel destroys the budget and everything in it; the sponsor can end it sooner. A lease is task-scoped: “read ~/project, write ~/project/out, the model gateway, 2 hours, 256 MB, 4 processes, weight 20”.

• At most MAX_LEASE, 24 hours. That is the steward’s rule, not the kernel’s: the kernel knows deadlines, not leases. A longer request is refused, not clamped (budgets).
• Ending a lease is always accepted from the sponsor, ahead of admission, so an agent that floods its sponsor’s share of a server cannot stop the sponsor from ending it.
• Three crashes blamed on one (account, label set) within ten minutes destroy every budget of that (account, label set), sessions and leases alike, and the steward refuses new sessions for it until the window passes: the steward’s blame-by-label-set rule (crash blame). An agent shares its sponsor’s account, so the sponsor answers for its agents, and a crash loop is stopped at the sponsor.
• When a lease ends, the scope’s destruction ends the agent’s connections at once, in every table (R41 (narrowing by revocation scope)); the steward then disconnects them at each server to free what they held, and releases what typed servers granted; everything is recorded in the audit log from M5 (self-hosted development). However it ended, the sponsor’s unlabelled sessions are told: the shell prints [lease NAME ended] from the steward’s lease_ended send, naming the lease and never why (the steward).
• An agent that must stay alive keeps a process runnable. A VM with nothing runnable, no timer pending and nothing it waits on exits, beamlet: Deadlock, an exit that is not 0 (beamlet), and a lease’s VM’s exit is its lease’s end as the steward reads it, said as exited CODE (the steward). So an agent that has done its work and must live to its deadline or its sponsor’s end_lease idles by a busy recursion, never by a receive with no timeout and no sender: Process.sleep(:infinity) is one, and an agent that slept so ended as soon as it slept. The echo agent’s live paths and the scripted agents that outlive their work idle that way; one whose work is done returns, and that exit, 0, is its lease’s end on purpose.
• The image’s agent is a sponsored principal: its login is a lease of alice’s, carved from her unlabelled share for MAX_LEASE, which her sessions can end and are told the end of; the harness that drives it runs inside the lease unchanged.
• A lease’s root has a quota of its own. /project is the sponsor’s ~/project, minted below the home with the agent size’s quota (1 MiB in the image) carved from the home’s and given back at the lease’s end: among the lease’s sizes, since a root below a home with no quota holds nothing (walfsd); a ~/project already holding more refuses the lease, and start_agent answers failed. So does a server that does not answer one of the lease batch’s calls (the carve, a mint, the image’s reads) within the steward’s bound, SERVER_US: the lease is rolled back and the sponsor asks again (the steward).
• A launch takes seconds under load, and its caller waits for it. start_agent is the one steward call measured past the client’s 5 s bound for a short call: its served time beside the sponsor’s other leases spinning is at worst 6.64 s under the bench’s rounds, so the client passes it a bound of its own, 14 s, twice that worst rounded up to a second (Redoubt.Wire.Client.launch_timeout/0; the figures on the steward). A launch past it is timeout, as any call, and a scheduler finding on scheduling, never a longer bound.
• A labelled agent’s /project is its label set’s vault: the vault is the task’s scope, and R25 (the label check) lets the agent touch nothing of the unlabelled ~/project; an unlabelled agent’s is its sponsor’s ~/project, with a quota carved from the home. A labelled agent is started only by an approval at approve@box (the steward).
• A lease has no console. Its namespace holds no /dev/cons, and beamlet’s platform runs without one (beamlet): what the agent writes to the console is dropped, a read answers the end of the input, so an agent’s output has nowhere to go but /project/out. How its VM ended is the steward’s console line (steward: lease alice/agent-1 7303562901476581370 of 1001/{} exited 0, the lease’s id beside its name), never the agent’s.
• A lease has no network. Its namespace holds no /net, so its VM’s gen_tcp has only the loopback inside the VM (beamlet): a connect to any other address is {error, enetunreach}, and the bench’s peer sees nothing from it (session-tcp-loopback; for a labelled agent in its vault, steward-labelled-agent-no-sink). An agent reaches outside the box only through its gateway capabilities, later (gatewayd).
• A lease is not re-bound. When a shared server restarts, the steward tells its sessions on their notices endpoints and each shell re-binds its home (the steward); a lease’s VM has no such endpoint and no shell, so an agent’s /project at a restarted walfsd stays dead until its deadline or its sponsor’s end_lease (the steward answers a lease’s rebind unknown); the sponsor’s way out is end_lease and a new start_agent, the sponsor’s own sessions being re-bound. Ending the lease for the server’s fault would punish the sponsor’s work when the sponsor already holds the choice; a notices endpoint for leases is a later node, when agents must outlive a server’s restart.

A lease’s end is the kernel’s

Status: built · partly tested: a process that enters the kernel in a tight loop to put a deadline off is not attacked by a case · tested: bench:budget-deadline, bench:steward-lease-ends, bench:steward-sub-agent-dies-with-agent, mutation:BudgetDeadlineIgnored

The deadline under a lease is a kernel mechanism, and it is built (budgets). When it passes, the kernel destroys the budget exactly as budget_destroy would, at the first kernel entry at or after it, with nobody asking; a process spinning in user mode is stopped by the timer interrupt. There is no call or state in which the kernel puts a deadline off. The processes it kills get exit notices with cause killed, a call a server took is abandoned, every handle to the budget is revoked (R10 (destruction)), and a child budget’s later deadline never fires: a sub-agent’s budget inside an agent’s never outlives it.

An agent cannot crowd out its sponsor

Status: built · partly tested: the share and the lease-end-under-flood run on the host, in the serving library; the boot arm times the sponsor’s own calls under the flood · tested: host:redoubt-rt::an_agent_flooding_a_bucket_leaves_its_sponsor_a_share_and_its_lease_end, host:redoubt-rt::an_agent_flooding_a_bucket_leaves_its_sponsor_a_share, bench:steward-agent-flood

An agent shares its sponsor’s account, so its calls count against its sponsor’s admission limits for that label set. Inside them, the serving library’s admission gives every badge a fair share, so an agent that floods a server through its own connection leaves its sponsor a share of the same bucket. The host tests put an agent and its sponsor in one bucket and flood it from the agent’s side (libs/rt/src/server/admit.rs, the serving library).

Delegation only narrows

Status: planned · M3 (agents, approvals and the attack suite)

flowchart TB
    A["Alice's session<br/>/home/alice (read, write), /net: a scope"]
    AG["agent-7, lease under Alice's budget<br/>/project: /home/alice/project (read)<br/>/out: /home/alice/project/out (write)"]
    SA["sub-agent, budget inside agent-7's<br/>/src: /home/alice/project/src (read)"]
    X["a sibling of agent-7,<br/>or a budget with more labels"]
    A -.->|"steward: fresh, narrower connections"| AG
    AG -.->|"its own budget: narrower again"| SA
    AG -.-x|"refused: needs the steward and an approval"| X

Figure: a capability delegation tree. Every part is planned (dashed). Each step holds a subset of the step above, through fresh connections; nothing reaches sideways or up.

Person to agent to sub-agent, each step is narrower, and the chain is recorded.

• Fresh, narrower connections. A launcher never passes its own connection: it asks the server for a new one, rooted lower or read-only, and passes that (sessions). A handle minted this way keeps the stamp of the one it came from, so it dies with it (R9 (stamps)).
• Sub-agents live inside their parent’s budget. An agent holds only its own budget’s handle, so it cannot make a sibling; a sub-agent’s budget is carved from the agent’s, and the agent’s lease ending ends its sub-agents, whatever their own deadlines.
• Labels only grow downward. A child budget carries all its parent’s labels, and adding one needs a system-class caller (I6 (labels only grow downward)). So an agent cannot shed a label it was started with, and a budget with more labels, or a new durable principal, needs the steward and an approval.
• Never network by default. An agent inherits no network access. From M5 (self-hosted development) it reaches a model through a gatewayd capability that holds the API key; only people get name-scoped TCP (gatewayd).

Open: none.

Labels and vaults

Status: planned · M3 (agents, approvals and the attack suite)

Capabilities bound what an agent can do; labels bound what it can leak. The unit of isolation is the label set, not the capability set: a budget with a label can read that label’s data and cannot send to anything without it (R1 (flow), labels). So an agent that must read a secret runs with the secret’s label, and then has no network (ipd refuses labelled callers), cannot write down to unlabelled volumes, and can reach its sponsor only through channels that carry the label.

The high/low pair is the case the design is built for. Agent A holds a secret and no network; agent B has a network and no secret; they are co-conspirators with a pre-arranged code. The claim is exactly one thing: no intentional software path crosses the label boundary between them. Covert channels (timing, shared physical state) are a stated wall, not one the design closes.

Two stated residuals:

• No non-collusion guarantee within one label set. Two agents with different handle sets but the same label set are not kept from cooperating: labels separate label sets, and within one label set the kernel carries messages between whoever holds each other’s handles. Agents that must not collude get different labels.
• The approval human. The design protects the approval channel from the requester (only the steward draws on approve@); it does not protect the person’s judgment. An agent that persuades its sponsor to approve more than they meant has won, and the design names that wall rather than closing it (sessions).

Open: none.

No credentials in agent memory

Status: planned · M3 (agents, approvals and the attack suite)

An agent never holds a key or an API token. It uses keys through keyd (the key server), and, from M5 (self-hosted development), models through gatewayd, which holds the API keys. Until M6 (persist, install, share) no session and no lease holds keyd capabilities at all.

A lease holds no key until principals’ signing keys exist, which the plan places with keys in leases in M6 (persist, install, share). Then a lease carries only a key its approval named, and a keyd capability names one key and one purpose, with the one message shape it may sign (for SSH, a signature over a session identifier keyd computed itself), never arbitrary bytes. Otherwise a hijacked agent would be a signature oracle, and its peer could log in as its sponsor elsewhere (keyd).

Open: none.

The agent harness

Status: planned · M5 (self-hosted development)

Redoubt.Agent starts and drives an agent from a session. The harness runs in the launcher’s VM; the agent runs in a VM of its own, in its lease, with its own label set, and the model loop runs there, through the agent’s own gatewayd connection.

There is no pause or resume. No kernel call freezes a budget, none can be emulated (a carve that would leave a process’s budget with no free weight is refused: R7 (carving)), and a lease’s deadline keeps running, so a pause would silently eat lease time.

The steward makes the lease. The harness asks; the steward places the lease under the sponsor’s budget for that label set, checks that every grant is the same as or narrower than what the launcher holds, refuses a term over MAX_LEASE rather than clamping it, and records the grant with the principal chain (the steward). Agent.start waits for the launch with the client’s launch bound, Redoubt.Wire.Client.launch_timeout/0, not the 5 s of a short call: a launch beside the sponsor’s other leases is measured in seconds (leases), and a harness that reintroduced the short bound would time out under the load the bench runs.

• Grants are closed, typed terms, the same terms the steward’s lease request carries. labels: is its own option, because adding a label needs an approval. The kinds are:

  • read: PATH and write: PATH, each a path in the launcher’s namespace; write does not imply read, so name both when both are meant;
  • gateway: NAME, one of the launcher’s own gatewayd grants by name, or {NAME, hosts: [...]} to narrow it;
  • git: {REMOTE, fetch: true, push: [REF_PATTERN, ...], force: false} (development);
  • launch: [pages:, processes:, weight:], a sub-budget the agent may start processes in.

  Nothing is free-form: there is no “all” and no wildcard beyond git’s ref patterns. An unknown kind, a path that does not resolve, or a term broader than the launcher holds is refused whole by the steward, before any budget exists. Planned cases: each kind is refused when broader than the launcher’s; an unknown kind is refused; run’s isolated: options and the keyword list give the same steward request.

• Each grant becomes the agent’s own connection. The steward mints each one fresh, with the agent’s own badge, so every request through it is the agent’s and never its sponsor’s: a file connection rooted where the grant says, a gatewayd or git capability no wider than the launcher’s, or a sub-budget to launch programs in. What the agent holds is the whole of what it can do beyond its own lease; there is no permission check to get wrong.

• No approval while everything narrows. A label the launcher lacks (an agent that must read a secret) or a new durable principal goes through an approval at approve@.

• Sub-agents are started the same way, by the agent’s harness asking the steward through its own connection; the sub-lease sits inside the agent’s budget and ends with it.

• kill and status go through the steward. Ending a lease is always accepted from the sponsor, ahead of admission, and is audited. The launcher never holds the lease’s budget handle, so it cannot create processes inside the agent’s budget and blur whose work is whose.

What the harness cannot be made to do:

• Take code or atoms from the agent. The link between harness and agent is a typed Redoubt channel, never Erlang distribution, which would give each VM full remote calls into the other. What the harness receives (replies to prompt, status) is untrusted data, decoded by a bounded decoder that creates no atoms and no code, never by binary_to_term.
• Parse model output. The model’s replies reach the agent’s VM, not the launcher’s.
• Hand the agent the sponsor’s things. The agent never gets the sponsor’s /dev/cons, keys or any budget handle but its own.
• Drive the sponsor’s terminal. What the harness shows of an agent’s replies it draws as cells through Redoubt.Term, so a control sequence in a reply is drawn visibly and never acts (the shell).

Open: none.

The agent loop

Status: planned · M5 (self-hosted development)

The model loop that runs in an agent’s VM is small by design, after Mario Zechner’s pi: a system prompt under 1,000 tokens, four tools, and nothing else in the loop.

• eval is the agent’s shell. Where pi gives a model bash, a Redoubt agent gets the same shell a person does (the shell): its commands, native pipes, and Redoubt.Agent for sub-agents when its grants allow them. It adds no authority: whatever eval runs, runs with the agent’s handles, inside its lease.
• Nothing more in the loop. No MCP, no plan mode, no to-do list, no tools beyond the four. What an agent can be told to do is bounded by what it holds, and a short loop leaves little to review in how it is told.
• The model is a stream from gatewayd. The loop sends the conversation through its gatewayd capability and receives the reply as a stream of typed events (text, a tool call, the end of a turn), which gatewayd decoded from the provider’s own stream; it opens no socket, holds no key and parses no provider’s format (gatewayd). Compaction shortens a conversation that nears the model’s context.
• No dependencies. The loop is plain Elixir, about 1,500 lines, with no Hex packages: JSON is Elixir’s own JSON, and there is no HTTP client because there is no HTTP. The pie project, a rewrite of pi in Elixir, is the model for its structure and is not copied: it has no licence. Its eval follows Tidewave’s (Apache-2.0).

Open: none.

The escape room

Status: planned · M5 (self-hosted development)

The bench tests properties someone already thought of. The escape room (the game) tests the ones nobody did, against real agents told to get out, and it runs continuously. Its scenarios:

• Single-agent escape: expand its capabilities, reach what it was not granted, survive a restart with authority it was not given.
• The high/low pair, above: any intentional path across the label boundary.
• Authority expansion: forge a handle, mint wider than the source, reach a system budget, add a label, outlive a lease through a child.
• Collusion through the human: persuasion, approval fatigue, a request that reads one way and means another.

A referee sets each match up (which of the kernel and the servers are assumed correct; a confined manifest, in which differing label sets share no server instance, volume, endpoint, network instance or device; a planted secret and a canary; B’s egress and the audit log recorded) and decides from the record, never from an agent’s own output. Every confirmed finding is classified:

Open: none.

Why

Agents are principals, not impersonations. If an agent acted as Alice, every action it took would be Alice’s, and nothing could tell her work from its work or limit it separately. As its own principal it has its own audit identity, its own lease and its own capabilities, and the sponsor link makes someone answerable without making the agent the person.

Assume compromise. An agent reads untrusted text for a living, and any of it can take the agent over. Designing for the honest agent would mean every guarantee fails at the first prompt injection. Designing for the hijacked one means the guarantees are about what the agent holds, which a prompt cannot change.

Leases, not permissions that last. A task has an end, and so should the authority for it. A kernel deadline means a forgotten agent stops by itself, and a sub-agent cannot outlive the agent that made it, without anyone having to remember to clean up.

Labels bound the leak, capabilities the damage. Capabilities alone cannot stop an agent that may read a secret from passing it to one that may send it: both are acting within their grants. Labels make the flow itself the kernel’s business, so the pair has no path to use.