Decision: containment is Linux-only, and the reach we differentiate on is Windows

[AminChirazi]

needs-human under CHARTER §8 — a strategic scope decision. Filed so it is decided deliberately rather than discovered in a pilot.

The mismatch

The differentiator flowproof sells is reach: the agent's decisions and the enterprise systems it drives — SAP GUI, Windows desktop, Citrix. The strongest guarantee flowproof makes is egress containment, and it exists on Linux only.

Those two sets barely overlap. The systems flowproof uniquely reaches are precisely the ones where the strongest claim is unavailable.

Current state:

• run_against_contained on non-Linux is run_against with an empty EgressLog — no filter, no error (crates/flowproof-adapters/src/agent_runner.rs:674-685).
• Containment::command_flow() on non-Linux returns NotContained("egress containment is Linux-only; this platform is not contained") (crates/flowproof-adapters/src/egress.rs:74-79).
• assert_no_egress hard-errors as a capability error on those platforms, with no bypass flag (crates/flowproof-cli/src/agent_flow.rs:842-848). This behaviour is correct and this issue does not propose changing it.
• Windows was started and is unfinished: spike/windows-containment is deliberately excluded from the workspace (Cargo.toml:11-28) and its LOG.md:1-3 reads "Status: in progress". There is no WFP code in crates/.

The honest consequence today

A flow that declares allow_egress without an assert_no_egress step still passes on macOS and Windows, uncontained, reaching whatever it likes. check_egress only gates on plan.assert_no_egress, so nothing forces the operator to notice. The tier line printed on stdout is the only signal, and a green build is not a place people read tier lines.

That is not a false green in the strict sense — no assertion claimed containment — but it is the shape of thing that becomes one in a customer's pipeline.

The decision

1. Is Windows containment on the roadmap, or is Linux-only the answer? If the pilot motion is SAP on Windows, "we contain on Linux" is a weak answer to the question a pilot will actually ask. If the answer is Linux-only for the foreseeable future, that should be said plainly on the page rather than being discoverable only from a tier line.
2. Cheap interim, independent of 1: should allow_egress without assert_no_egress on an uncontained platform warn loudly — or refuse? Declaring an allow-list is a statement of intent; silently not enforcing it is the gap most likely to bite. This one is small and does not require deciding the roadmap question.

Related coverage note

The seccomp runtime is proven only on Linux CI and only behind RUN_EGRESS_E2E=1 (.github/workflows/ci.yml:167; the test is #[cfg(target_os = "linux")] at crates/flowproof-cli/tests/egress_e2e.rs:14 with an enabled() early-return). On a dev machine without that variable the E2E silently no-ops. Not a defect, but worth knowing when weighing how much of the containment path is routinely exercised.

Context

Filed alongside #300 and #301 (two Priority-1 false greens in the Linux containment path) and #302 (containment is network-only). Those three are about whether containment works where it exists; this one is about where it exists at all.

[AminChirazi]

Scope: Windows egress containment

Direction given: implement it. Scoping first, because the spike changes what "implement" means here.

This is not green-field

spike/windows-containment/LOG.md is 1,232 lines of nine-iteration spike log ending in a VERDICT of "Build it", with the kill criterion (gui.q1.drives-own-gui-app) MET across two consecutive windows-latest runs. The mechanism is measured, not hypothesised:

• a declared destination is reachable and the destination oracle sees the payload;
• an undeclared destination is refused WSAEACCES (10013) and the oracle sees nothing;
• a grandchild through cmd.exe is refused identically — the escape that makes app-id filtering useless is closed by the per-run identity;
• the drop record carries remote address, port, protocol, run-identity SID and filter id;
• filters are gone after the supervisor is killed outright, verified through a fresh engine handle;
• with the block filter removed, every one of those inverts — the failure path is exercised, not assumed.

So the remaining work is engineering a proven harness into flowproof-adapters, not research. spike/windows-containment is currently in the root Cargo.toml exclude list, deliberately (iteration 7), and Cargo.lock is committed so a re-run resolves the same versions.

Six constraints the spike already found, each of which shapes the design

These are the reason this needs a scope rather than a "port it" ticket. Every one of them is a negative finding that would otherwise be discovered late:

1. assert_no_egress on Windows must be implemented against the audit lane, never against client errors. UDP containment is invisible to the contained process — send_to returns success on a datagram the kernel drops. A client-side implementation would pass vacuously.
2. Net-event collection cannot be enabled from a dynamic WFP session. The spike's audit lane worked only because collection happened to be on already. Shipping needs a second non-dynamic handle to enable and restore it — and if that fails, the run is not contained, not silently unaudited.
3. The raw-socket/promiscuous filter must not be used as written — it denies the contained identity every socket, declared included. Raw sockets are closed by the run identity being unprivileged instead, which is sturdier because it cannot be got wrong.
4. Administrator is required on every run. Linux gets containment unprivileged; Windows does not. This has to be said in the same breath as the claim, every time.
5. CreateProcessAsUserW needs SeAssignPrimaryTokenPrivilege, which GitHub's elevated RID-500 Administrator does not grant. The CreateProcessWithLogonW fallback needs the Secondary Logon service and cannot be used from LocalSystem — so a flowproof runner installed as a Windows service needs this arranged deliberately.
6. Cross-identity GUI control is impossible. Every fused flow must launch its GUI application inside the boundary. That changes what an adopter has to do, not just what flowproof does.

Proposed sequencing

Each step is a PR under the 400-line cap. Steps 1–3 are the feature; 4 is what makes it trustworthy.

#	What	Verifiable where
1	Containment::command_flow() gains a Windows arm: probe for Administrator, SeAssignPrimaryTokenPrivilege, Secondary Logon, and net-event collection. Returns Enforced or a named NotContained reason. No filters yet.	Linux (cargo check --target x86_64-pc-windows-msvc) + full-ci
2	Port identity.rs + wfp.rs + launch.rs into flowproof-adapters behind #[cfg(windows)], wired to AllowSet. The Linux AllowSet is reused unchanged — the allow-list grammar is already platform-neutral.	full-ci
3	The audit lane: netevents readback populates EgressLog.blocked, and a failure to enable collection populates EgressLog.faults (the channel #306 adds). Constraint 1 falls out of this for free.	full-ci
4	The E2E, ported from tests/spike.rs, with its polarity inverted. The spike deliberately never fails ("a red job truncates the evidence"); a shipping containment test must fail loudly. Its negative control becomes the falsifiability fixture M2 criterion 6 asks for.	full-ci

Two things a human should decide before step 1

• The Administrator requirement is a product fact, not an implementation detail. "Kernel-enforced, and needs Administrator on every run" is a materially different adoption story from Linux's unprivileged filter, and it will be the first question a Windows pilot asks. It belongs on the page and in the docs, decided rather than discovered.
• Constraint 6 changes the adopter's flow shape — the GUI app must be launched inside the boundary. That is the fused SAP claim's real cost and it should be written down before anyone builds against it.

Honest limit, restated

The spike's own closing section says the sentence it still cannot say is "this agent drove SAP GUI and provably touched nothing else" — not because containment failed, but because Notepad is a fair proxy for the identity boundary and a poor one for SAP. Closing that needs the same harness run on a licensed SAP GUI host, per the re-run instructions in iteration 7. Steps 1–4 deliver contained Windows agents and contained Windows desktop apps; they do not by themselves deliver the fused SAP claim.

Also worth surfacing

Negative finding 7 in the verdict is an escalation unrelated to the mechanism: the adversary gate refuses any pull request over ~128 KiB and reports a tooling failure as a review refusal. That is a protected path under the constitution, so a human has to fix it — and it will bite this work, because a WFP port is exactly the kind of change that gets large.

I can start on step 1 whenever you want. I cannot compile-verify against a real Windows kernel from here, but cargo check --target x86_64-pc-windows-msvc typechecks the whole Windows path on Linux in seconds (iteration 1's finding), and the full-ci label is what proves the rest.

---

Generated by Claude Code