Priority 1 under CHARTER §5. Sibling of #300 — different mechanism, same consequence: assert_no_egress passes over a run that was not contained.
The defect
The BPF prologue rejects a foreign architecture by allowing it. The comment says so in as many words:
// crates/flowproof-adapters/src/egress_linux.rs:182-189
// Prologue: reject a foreign arch (out of scope for v1 - a 32-bit compat
// call is a documented punt) by allowing it, then load the syscall nr.
let mut f = vec[
bpf_stmt(BPF_LD | BPF_W | BPF_ABS, OFF_ARCH),
bpf_jump(BPF_JMP | BPF_JEQ | BPF_K, AUDIT_ARCH, 1, 0),
bpf_stmt(BPF_RET | BPF_K, allow), // <-- foreign arch: ALLOW
bpf_stmt(BPF_LD | BPF_W | BPF_ABS, OFF_NR),
];A 32-bit x86 process on an x86_64 host therefore has unrestricted network egress: connect, sendto, sendmsg and listen are never trapped, EgressLog.blocked stays empty, and check_egress (crates/flowproof-cli/src/agent_flow.rs:852-855) finds nothing to fail on. The run reports containment: enforced (linux seccomp) and assert_no_egress passes.
Why "documented punt" understates it
Two separate problems with the current framing:
- It is not actually documented. The "Punts (v1)" list in
docs/agent-testing.md:876-884 names the loopback exemption and states the sandbox-not-a-jail framing, but does not mention the foreign-arch bypass. So the one place a reader would go to learn the limits does not carry it. Under CHARTER §5.6 that is a docs-accuracy defect in its own right.
- A punt should fail closed. Every other unmodelled case in this file denies rather than guesses — an unparseable sockaddr returns
EPERM "rather than guess" (egress_linux.rs:648-649), io_uring_setup and AF_PACKET are EPERM in BPF. Foreign arch is the only place the code resolves an unknown by permitting it, and it is the one with the widest blast radius.
Suggested fix
Change the prologue's foreign-arch action from SECCOMP_RET_ALLOW to SECCOMP_RET_ERRNO(EPERM).
This is the conservative direction and matches the rest of the filter. The cost is that a genuinely 32-bit agent under containment stops working — which is the correct outcome, because today it "works" by not being contained. If a real adopter needs it, that is a second filter for the compat arch, not a hole.
Worth deciding alongside: whether this should instead surface as capability-error ("this process is a foreign arch and cannot be contained") rather than a bare EPERM, so the operator learns why their agent's network died. That is the same reporting question as #300 and the two fixes may want to share a mechanism.
Test that proves it stays fixed
The existing unit test asserts the terminating instruction is SECCOMP_RET_ALLOW (egress_linux.rs:1162-1169) — that is the epilogue default and should stay. A new assertion should pin the prologue: a seccomp_data with a non-matching arch must resolve to the deny action, not the allow action. The filter is pure data, so this is testable without a kernel and without a Linux runner.
A red-path fixture for the falsifiability suite (M2 amendment criterion 6) would need a 32-bit binary on the Linux runner; if that is too heavy, the BPF-level assertion is the ratchet that matters.
Priority 1 under CHARTER §5. Sibling of #300 — different mechanism, same consequence:
assert_no_egresspasses over a run that was not contained.The defect
The BPF prologue rejects a foreign architecture by allowing it. The comment says so in as many words:
A 32-bit x86 process on an x86_64 host therefore has unrestricted network egress:
connect,sendto,sendmsgandlistenare never trapped,EgressLog.blockedstays empty, andcheck_egress(crates/flowproof-cli/src/agent_flow.rs:852-855) finds nothing to fail on. The run reportscontainment: enforced (linux seccomp)andassert_no_egresspasses.Why "documented punt" understates it
Two separate problems with the current framing:
docs/agent-testing.md:876-884names the loopback exemption and states the sandbox-not-a-jail framing, but does not mention the foreign-arch bypass. So the one place a reader would go to learn the limits does not carry it. Under CHARTER §5.6 that is a docs-accuracy defect in its own right.EPERM"rather than guess" (egress_linux.rs:648-649),io_uring_setupandAF_PACKETareEPERMin BPF. Foreign arch is the only place the code resolves an unknown by permitting it, and it is the one with the widest blast radius.Suggested fix
Change the prologue's foreign-arch action from
SECCOMP_RET_ALLOWtoSECCOMP_RET_ERRNO(EPERM).This is the conservative direction and matches the rest of the filter. The cost is that a genuinely 32-bit agent under containment stops working — which is the correct outcome, because today it "works" by not being contained. If a real adopter needs it, that is a second filter for the compat arch, not a hole.
Worth deciding alongside: whether this should instead surface as
capability-error("this process is a foreign arch and cannot be contained") rather than a bareEPERM, so the operator learns why their agent's network died. That is the same reporting question as #300 and the two fixes may want to share a mechanism.Test that proves it stays fixed
The existing unit test asserts the terminating instruction is
SECCOMP_RET_ALLOW(egress_linux.rs:1162-1169) — that is the epilogue default and should stay. A new assertion should pin the prologue: aseccomp_datawith a non-matchingarchmust resolve to the deny action, not the allow action. The filter is pure data, so this is testable without a kernel and without a Linux runner.A red-path fixture for the falsifiability suite (M2 amendment criterion 6) would need a 32-bit binary on the Linux runner; if that is too heavy, the BPF-level assertion is the ratchet that matters.