Decision: nothing stops an agent deleting a file — containment is network-only

[AminChirazi]

needs-human under CHARTER §8 — this is a public-API decision and a scope question, not a defect to fix. Filed for a decision, not for a loop to take.

The gap

The promise the product is marketed on — most plainly on automators.ai/flowproof, and in the README as of #298 — is that a bot "only ever does the job it was given, and never deletes, sends or approves the thing it must not."

Containment today is network only. The BPF filter traps connect, sendto, sendmsg, sendmmsg, listen, plus EPERM on io_uring_setup and socket(AF_PACKET). Everything else returns SECCOMP_RET_ALLOW (crates/flowproof-adapters/src/egress_linux.rs:190-215). open, write, unlink, rename, execve are untouched. There is no Landlock, no chroot, no mount namespace — verified by absence across crates/.

So an agent under full containment on Linux can delete any file its uid can reach. It can also execve freely; children inherit the network filter under NO_NEW_PRIVS but nothing constrains what they do to disk.

The mcp: stand-in covers declared tools only, and is convention-dependent rather than mechanism-enforced (see the separate concern below).

Why this needs a human

Three reasons it is not a loop task:

1. Net-new public API. Any answer adds surface — an allow_fs:, an assert_no_fs_write, or a new lane in the trace. CHARTER DECIDE 5 caps net new public API precisely so this kind of thing is deliberate.
2. It is a positioning decision, not only a technical one. There is a legitimate answer that says no — flowproof is "a testing sandbox, not a jail" (egress_linux.rs:10-11, docs/agent-testing.md:883-884), and the honest move is to make the marketing narrower rather than the mechanism wider. That is a founder call.
3. It interacts with the containment/behaviour split, which is the page's load-bearing copy rule.

The options, as I see them

A. Narrow the claim. Keep containment network-only; make the docs and the page say "network" wherever they currently say "can't". Cheapest, entirely honest, and gives up the line that most resonates with the buyer.

B. Detection without prevention. No filesystem lock, but a red-path proof that a destructive filesystem action is observed and fails the run. Fits the existing "record it, then assert over it" model, needs no new containment machinery, and is a behaviour claim — so it belongs in the outlined panel, not the filled one.

C. Real filesystem containment. Landlock (kernel ≥ 5.13) is the natural fit and composes with the existing NO_NEW_PRIVS + seccomp install path. Strongest, most work, and inherits every platform limit that already applies to egress.

My read: B is the best value and the smallest lie-surface. It matches what flowproof actually is, it is testable in the falsifiability suite alongside the other red-path proofs, and it does not promise a jail. C is a real product if filesystem risk is what pilots actually ask about — which is worth knowing before building it.

Related, same decision family

The mcp: stand-in currently sits in the page's containment ("it can't") block, but it is bypassable by misconfiguration: flowproof injects FLOWPROOF_MCP_SERVER_<NAME> (crates/flowproof-cli/src/agent_flow.rs:276-280) and the agent's own config has to point at it. If it points at the real server instead, flowproof is out of the path. The guards at agent_flow.rs:410-425 detect the empty lane after the fact — that is a guard, not a barrier.

Under the page's own hard copy rule (a behaviour claim written as a containment claim is the one mistake a security-minded reader will not forgive), that placement is hard to defend as-is. It either needs qualifying in place or moving. Same decision, so noted here rather than filed separately.

[AminChirazi]

Design: detect, don't prevent

Direction chosen: option B — no filesystem lock; destructive filesystem actions are observed, and can fail a run.

Posting a design rather than a PR, because this needs new public API and a new trace lane, and CHARTER §8 puts both behind a human. The direction is settled; the shape below is what needs signing off.

The mechanism, and why it is nearly free

The seccomp supervisor already exists and already traps syscalls. Add unlink, unlinkat, rmdir, rename, renameat, renameat2 and truncate to the filter — but reply SECCOMP_USER_NOTIF_FLAG_CONTINUE rather than performing them.

That flag is exactly what the egress path refuses to use, and the reason why is the whole argument here. On CONTINUE the kernel re-reads the child's memory after we decide, so a sibling thread can rewrite the path between our read and the kernel's. For enforcement that race is fatal — it is why perform_connect dups the child's socket and connects from a verified copy. For observation it is acceptable: the worst case is a recorded path that is stale, which weakens the evidence but cannot let anything through, because nothing was being stopped.

That asymmetry is precisely why this is a behaviour claim and not a containment one, and it should be stated in the code rather than inferred. A future reader who "upgrades" this path to denial without switching off CONTINUE would create a containment claim with a TOCTOU hole in it.

The API

steps:
  - prompt: Tidy up the old exports.
  - assert_no_file_delete            # nothing under the run's cwd was unlinked

Open questions on shape — this is the part I would not decide alone:

1. One assertion or a scoped one? assert_no_file_delete is the narrow, honest version. assert_no_fs_write: /etc/** is more useful and much more surface (glob semantics, symlink resolution, relative-path normalisation against the child's cwd). I lean narrow first: the demo that sells this is "the agent must not delete the customer", not a policy language.
2. Does it belong in control:? It should — a rule with a stable id is the point — but that means it lands in the flowproof audit map and the --since gate, which is a bigger surface than the assertion itself.
3. Path resolution. unlinkat(dirfd, "x") needs readlink /proc/<pid>/fd/<dirfd> to render an absolute path. Cheap, but it is another thing that can fail — and per False green: a broken egress supervisor passes assert_no_egress silently #300's doctrine, a failure to resolve must be a fault, not a silently-empty lane.

Trace and schema

A new fs lane beside egress, carrying the observed operations. Per CLAUDE.md this means docs/trace-format.md and crates/flowproof-trace/schema/ in the same commit, enforced by the adversary ratchets.

Written only when the feature is engaged, exactly as the egress lane is, so an unrelated flow serialises byte-identical to today.

Sequencing

#	What	Size
1	Trap + observe + record into an FsLog, reported on stdout. No assertion, no trace lane.	~250 lines
2	The trace lane + schema + docs/trace-format.md.	~200 lines
3	assert_no_file_delete, the grammar, and the red-path fixture.	~250 lines

Step 1 is independently useful — it makes destructive filesystem work visible in a report — and it is the step that proves the CONTINUE approach behaves before any API is committed to.

Where this lands on the page

The outlined panel, not the filled one. It is "it didn't", checked every commit — never "it can't". The panel's footnote already says the lock is network-only as of automators-com/automators-website#392, so this adds to the behaviour side without disturbing that.

The mcp: half of this issue

Resolved separately and already shipped: automators-com/automators-website#392 keeps the mcp: stand-in in the containment block but states its precondition, rather than moving it. It genuinely prevents the real tool from running; it does so because flowproof is the process the agent talks to, and that is now said out loud.

---

Generated by Claude Code