mollusk/pixelpass
1
1
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

host/taint: close the inverse asymmetric leak; strengthen contracts (Codex round 3)

Browse Source 
Round 3 was the second verification round. One real leak, one accepted
narrowing of Codex's own suggested fix, two contract strengthenings, and
a test-gap fix.

F1 (P1, real leak, fixed): the inverse of round-1 finding 4. A tainted
reader that is itself *unbounded* (client.id only, daemon PID suppressed)
whose re-emitting leg carried an *unmatched* strong key left that leg
"bounded" and Eligible. An unbounded reader cannot be positively related
to any output, so a strong key that does not match it back proves nothing.

  Two-tier backstop. A bounded tainted reader excludes only unbounded
  outputs (a differently-keyed output is provably a different owner). An
  unbounded tainted reader also excludes daemon-owned outputs — but NOT
  ordinary apps.

  ⚠️ Deliberately narrower than Codex's suggested "exclude every output".
  An unbounded reader is necessarily daemon-owned (a real app has its own
  PID, which is a usable key, so it would be bounded), so its sibling is
  another daemon leg, never an app. Sweeping in real apps would lose the
  round-1 "blast radius stays small" guarantee for no safety gain. When
  the daemon PID is unknown the app/leg distinction collapses and the rule
  degrades to Codex's exclude-all. Both directions are pinned by tests,
  and the over-aggressive variant fails the spares-real-apps test.

F2 (contract, strengthened): `session_device` is documented as a positive
high-confidence phase-3 classification, not `device.id`+`device.api`
(measured insufficient — a card filter can carry both; node.physical is
null on the real ALSA nodes so it is not a discriminator). Fail closed:
unknown ⇒ false. Documented why a mis-classified filter still does not
leak in practice — its legs share a link-group (strong-key bridge) and an
unbounded reading leg trips the two-tier backstop.

F5 (P2, test gap): a mutation keeping only PID fingerprints survived all
49 tests. Added a strong-key (pulse.module.id) new-connection fixture.

Mutation-verified 3/3 including the over-aggressive counter-mutation.

Still OWED to round 3, carried to round 4 for adjudication: finding 3
(a not-ready epoch can persist provisional owner *fusion* as sticky
over-exclusion). It is over-exclusion, never an echo leak, and closing it
needs a readiness/provenance model decision rather than a local patch —
see the round-4 handoff. 53 tests.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
mollusk
2026-07-21 17:40:24 -04:00
co-authored by Claude Opus 4.8
parent 31084edcfa
commit f35bab0379
3 changed files with 280 additions and 28 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/host/taint/mod.rs
+57 -12
View File
@@ -361,7 +361,8 @@ pub fn evaluate(
let mut changed = false;
changed |= propagate_links(&edges.edges, &mut taint);
changed |= propagate_owner_bridge(&keys, &components, &edges, &mut taint);
changed |= propagate_unresolved_owner(snapshot, &keys, &edges, &mut taint);
changed |=
propagate_unresolved_owner(snapshot, ctx.pipewire_pulse_pid, &keys, &edges, &mut taint);
if !changed {
break;
}
@@ -662,28 +663,72 @@ fn propagate_owner_bridge(
/// carry a real `application.process.id` and are bounded, so they are
/// never swept up; in practice only daemon-owned keyless module streams
/// are.
/// - ⚠️ **Removed (Codex round 1): the source no longer has to be unbounded
/// itself.** Properties can be asymmetric — a reader carrying a
/// `node.link-group` whose re-emitting leg carries none is *bounded* while
/// its sibling is not findable — and requiring an unbounded source let
/// exactly that shape through as Eligible.
/// - ⚠️ **The source does not have to be unbounded** (Codex round 1): a
/// reader carrying a `node.link-group` whose re-emitting leg carries none
/// is *bounded* while its sibling is not findable, and requiring an
/// unbounded source let exactly that shape through.
///
/// **Two tiers, because a tainted reader we cannot bound is a bigger
/// unknown than one we can** (Codex round 3 — the mirror image of the
/// round-1 case):
///
/// - A *bounded* tainted reader has a strong key or a usable PID, so its
/// siblings are exactly the output legs sharing that key. Any output leg
/// that is *itself* bounded by a **different** key is provably a different
/// owner and stays eligible; only unbounded output legs are its possible
/// siblings. → exclude unbounded outputs.
/// - An *unbounded* tainted reader has nothing that identifies its owner, so
/// its re-emitting leg could carry a strong key we cannot match back to
/// it. But it cannot be *anything*: a reader with no usable owner key is
/// necessarily **daemon-owned** — a real application has its own PID,
/// which is a usable key, so it would be bounded. Its sibling is therefore
/// another daemon-owned output, never an ordinary app. → also exclude the
/// daemon-owned outputs (bounded by a strong key or not); leave outputs
/// carrying a real, non-daemon PID eligible, because a real app is
/// provably a different owner from a daemon module leg.
///
/// ⚠️ This is deliberately **narrower than Codex round 3's suggested
/// "exclude every output"**, which would make an ordinary app unshareable
/// whenever any keyless module forwarder reads the call — losing the
/// round-1 "blast radius stays small" guarantee for no safety gain, since
/// a real app cannot be the sibling of a daemon leg. When the daemon PID
/// is *unknown* the distinction collapses (we cannot tell a real app from
/// a module leg) and the rule degrades to Codex's: exclude everything.
fn propagate_unresolved_owner(
snapshot: &GraphSnapshot,
ctx_pulse_pid: Option<u32>,
keys: &owner::OwnerKeyIndex,
edges: &Edges,
taint: &mut BTreeMap<Serial, Reason>,
) -> bool {
let tainted_reader = snapshot.nodes().any(|node| {
!node.props.session_device
let mut has_tainted_reader = false;
let mut has_unbounded_tainted_reader = false;
for node in snapshot.nodes() {
let is_tainted_reader = !node.props.session_device
&& edges.receivers.contains(&node.serial)
&& taint.get(&node.serial).is_some_and(|r| r.propagates())
});
if !tainted_reader {
&& taint.get(&node.serial).is_some_and(|r| r.propagates());
if is_tainted_reader {
has_tainted_reader = true;
has_unbounded_tainted_reader |= !keys.is_bounded(node.serial);
}
}
if !has_tainted_reader {
return false;
}
let mut changed = false;
for node in snapshot.nodes() {
if node.role == MediaRole::StreamOutput && !keys.is_bounded(node.serial) {
if node.role != MediaRole::StreamOutput {
continue;
}
// A real, non-daemon PID proves the node is an ordinary app, not a
// module leg — the one thing an unbounded daemon reader's sibling
// cannot be. Unknown daemon PID ⇒ cannot prove it ⇒ swept in.
let is_real_app = matches!(
(node.props.process_id, ctx_pulse_pid),
(Some(pid), Some(daemon)) if pid != daemon
);
let swept_by_unbounded = has_unbounded_tainted_reader && !is_real_app;
if !keys.is_bounded(node.serial) || swept_by_unbounded {
changed |= raise(taint, node.serial, Reason::UnresolvedOwner);
}
}