False green: a broken egress supervisor passes assert_no_egress silently

[AminChirazi]

Priority 1 under CHARTER §5 — flowproof reports PASS where the truth is FAIL. Filed after tracing the containment path against the source; every claim below has a file:line and I have verified the two load-bearing ones directly.

The defect

Mechanism failures in the seccomp supervisor return EPERM without recording the attempt, while policy denials do record. Compare, inside handle_connect:

// crates/flowproof-adapters/src/egress_linux.rs:626-632
if !notif_id_valid(fd, req.id) {
    return errno_resp(libc::EPERM);          // no record()
}
let Ok(n) = read else {
    dbg_egress("connect: read_child FAILED -> EPERM");
    return errno_resp(libc::EPERM);          // no record()
};

// crates/flowproof-adapters/src/egress_linux.rs:643-645
dbg_egress(&format!("connect: DENIED by policy {ip}:{port}"));
record(log, spawn, &format!("{ip}:{port}"), "tcp");   // recorded
errno_resp(libc::ECONNREFUSED)

Same silent-EPERM shape at egress_linux.rs:824-827 (pidfd_getfd failure in perform_connect) and egress_linux.rs:774-776.

Why that becomes a green build

probe_containment only distinguishes "kernel too old" — it tests pidfd_getfd for ENOSYS and nothing else (egress_linux.rs:227-230). A host with yama/ptrace_scope >= 2, or a container without CAP_SYS_PTRACE, refuses process_vm_readv with EPERM/EACCES, not ENOSYS. So the probe returns Containment::Enforced and the run proceeds.

From there:

1. Every trapped connect fails the process_vm_readv read → silent EPERM.
2. EgressLog.blocked stays empty (record is never called — egress_linux.rs:1124-1134).
3. undeclared_destinations() is empty.
4. check_egress finds nothing to fail on and returns Ok (crates/flowproof-cli/src/agent_flow.rs:852-855).
5. assert_no_egress passes. The run reports containment: enforced (linux seccomp).

It is worst exactly where it matters

On replay the agent reaches flowproof at the model boundary over loopback, which AllowSet::allows short-circuits before consulting the list (crates/flowproof-adapters/src/egress.rs:154-156). So the agent runs completely normally, its outbound attempts fail invisibly, and CI goes green on a host where containment was never functioning.

The require_progress guard at agent_flow.rs:1267 does not catch this — the agent made progress. Nothing in the egress lane catches it, because the egress lane is empty by construction.

Also in scope: the sibling inconsistency

handle_sendmsg forwards to perform_sendmsg when the destination is unparseable, where handle_connect (:649-659) and handle_sendto (:702) both return EPERM. See the if let Some(Dest::Inet(..)) at egress_linux.rs:750-756 — None and Dest::Unix fall through to perform. Same deny-by-default posture, applied inconsistently.

Suggested fix

Two changes, both small:

1. Separate the buckets. Mechanism failures are not policy denials and must not share a silent path. Record them into a distinct field on EgressLog — the verdict for a run with a non-empty mechanism-failure bucket is capability-error, never pass. This is the same doctrine check_egress already applies to an unenforceable platform (agent_flow.rs:842-848); it just is not applied to a supervisor that installed and then could not function.
2. Make the probe prove the capability it needs, not merely that the kernel is new enough. A process_vm_readv against self is a cheap positive check; ENOSYS-only detection is not sufficient.

Plus: align handle_sendmsg with connect/sendto.

Test that proves it stays fixed

This belongs in the Milestone 2 falsifiability suite (amendment criterion 6 already names egress containment as needing a red-path proof). The finding sharpens what that fixture has to assert: not only "a blocked destination fails the run", but "a supervisor that cannot read child memory does not pass."

A fixture can force the condition without a hardened host — inject a read_child/notif_id_valid failure behind a test-only seam and assert the verdict is capability-error with a non-zero exit, not pass.

Note

CHARTER §2.10 and §8 apply if a fix would touch a committed cassette or the trace lane's shape; the change proposed here should need neither.