test(adapters): Windows containment, proved against a real kernel - #343
Merged
Conversation
The series built identity, logon, filters, capture and the audit lane, and every one of them was verified by reading and by cross-compiling. Nothing had ever asked the kernel whether the filters actually block. So: two oracles bound in the test process, a probe run as the per-run identity, and three independent witnesses on the result. The destination either accepted a connection or did not. The audit lane either names the drop or does not. And a DECLARED destination must still be reachable — without that, a child that never started passes every other assertion. The polarity is inverted from the spike this is ported from. That test deliberately never failed, because a red job truncates the evidence a feasibility study exists to produce. There is nothing left to discover here; there is a claim to keep true, so it goes red. The negative control is the part that matters. `an_undeclared_ destination_is_refused` would pass just as happily if the probe never executed — nothing connected, zero sightings, green. So the same probe runs again with the undeclared port added to the allow list, and must connect. That inversion is what makes the first test mean anything, and it is the falsifiability fixture CHARTER Milestone 2 criterion 6 asks for. A host that cannot enforce is a fact about the host, not a failure — but CI runs elevated, so an unready host THERE is asserted rather than skipped. A silent loss of elevation would otherwise turn this whole file green while testing nothing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XdXrbksFKirm7yW6EDunur
There was a problem hiding this comment.
Pull request overview
Adds a Windows-only end-to-end test that validates egress containment is actually enforced by the kernel (WFP), using independent in-process TCP “oracles”, the audit lane, and a positive/negative control pair to prevent vacuous passes.
Changes:
- Introduces a Windows containment E2E test that runs a contained
powershell.exeprobe against declared vs undeclared loopback destinations. - Asserts containment using three witnesses: destination connection counts, audit-lane blocked destinations, and a positive control that must still connect.
- Adds host-readiness gating that reports and returns locally, but hard-fails on CI if enforcement isn’t possible.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+74
to
+91
| fn bind() -> std::io::Result<Self> { | ||
| let listener = TcpListener::bind("127.0.0.1:0")?; | ||
| let port = listener.local_addr()?.port(); | ||
| let seen = Arc::new(AtomicUsize::new(0)); | ||
| let counter = seen.clone(); | ||
| std::thread::spawn(move || { | ||
| for stream in listener.incoming().flatten() { | ||
| // Read the byte the probe writes, so a bare SYN cannot be | ||
| // mistaken for a completed connection. | ||
| let mut buf = [0u8; 8]; | ||
| let mut stream = stream; | ||
| let _ = stream.set_read_timeout(Some(Duration::from_secs(2))); | ||
| let _ = stream.read(&mut buf); | ||
| counter.fetch_add(1, Ordering::SeqCst); | ||
| } | ||
| }); | ||
| Ok(Self { port, seen }) | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The series built identity, logon, filters, capture and the audit lane. Every one was verified by reading and by
cargo check --target x86_64-pc-windows-msvc. Nothing had ever asked the kernel whether the filters actually block.Three witnesses, because one is not evidence
A client-side connect error is consistent with containment and with a wrong port, a dead listener, or a typo in the test file. So each run is judged by:
TcpListeneroracles bound in the test process, counting connections that actually arrived. An independent witness, not a restatement of the child's own opinion.Outcome.blockedmust name the undeclared destination. An agent that was stopped but cannot be shown to have been stopped is a weaker claim than flowproof makes.The probe is
powershell.exerather than a helper binary flowproof would have to ship: it lives in System32 whereUsersalready holds read+execute, so the per-run identity can start it without this test also having to get a directory ACL right — a second mechanism whose failure would look exactly like a containment failure.Loopback is deliberate and was checked on a real runner: the spike found WFP's ALE layer classifies and drops loopback connects, with
loopback=trueon the drop record.The polarity is inverted from the spike
spike/windows-containment/tests/spike.rsdeliberately never fails — a red job truncates the run at the first interesting finding and hides everything after it, and negative results carried equal weight in a feasibility study. There is nothing left to discover here. There is a claim to keep true, so it goes red.The negative control is the point
an_undeclared_destination_is_refused_and_a_declared_one_is_notwould pass just as happily if the probe never executed: nothing connected to the undeclared oracle, therefore zero sightings, therefore green. That is a vacuous test, and a vacuous containment test is worse than none.So
the_same_probe_connects_when_the_destination_is_declaredruns the identical probe with the undeclared port added to the allow list, and asserts it connects. That inversion is what demonstrates the suite can tell contained from uncontained — and it is the falsifiability fixtureCHARTER.mdMilestone 2 criterion 6 asks for.The skip that isn't a skip
A host that cannot enforce is a fact about the host, not a failure, so it reports and returns. Except on CI, where the runner is elevated by definition and an unready host means something regressed — there it asserts. Without that clause a silent loss of elevation would turn this entire file green while testing nothing, which is the false green CHARTER §5 ranks first. No
#[ignore], noskip; the ratchets confirm both counts unchanged.Verification
cargo check -p flowproof-adapters --features sap-com --all-targets --target x86_64-pc-windows-msvc— clean, zero warningscargo test --workspace --all-features(Linux) — green; the file is#[cfg(windows, …)]so it compiles to nothing herecargo fmt --check— cleandiff size 289 <= 400, tests771 -> 773,#[ignore] 0 -> 0,skip/xfail 1 -> 1This has never executed. It typechecks for Windows and that is all I can prove from Linux. The
full-cilabel is what turns this from a well-argued file into a result — and if it goes red, that is the PR working.Two follow-ups, deliberately not here
Containment::command_flow()on Windows still says "egress containment is not implemented on Windows yet". It is implemented, as of feat(adapters): a Windows run reaches the containment that exists #342. The trace lane is correct (check_egressresolves the run's tier before callingcontainment_tag), but the CLI prints the predicted tier to stdout and into--jsonbefore the run starts, so a Windows run that WAS enforced is reported as uncontained. Threading the achieved tier out ofrecord/replayis a behaviour change with its own tests and its own PR.egress_windows's module doc still opens "Still installs no WFP filter and launches nothing." Stale since fix(adapters): Select typed the option name when the option did not exist #331. Goes with the above.No CHANGELOG entry yet — it ships when a Windows job has actually run this green.
Generated by Claude Code