Tier-B provenance guarantees taint, not containment: a merged external can address arbitrarily far from a caller pointer

[0xGeorgii]

Problem

core/wasm-linker's Tier-B admission proves an address-provenance (taint) property — every memory address derives from a caller-supplied parameter — and is documented as such (provenance.rs, record_access: "a param + N effective address still varies with the caller's pointer and can never reach a caller-independent host location"). That statement is true.

It is, however, not containment. Nothing establishes that an admitted access stays inside the region the caller actually granted, and the analysis cannot establish it: it carries no sizes. Every one of these links today:

store at p + const 1048576                           ACCEPT
store at p + q   (both params, no const)             ACCEPT
store at p + p   (= 2p)                              ACCEPT
loop: ptr = p; { store ptr; ptr += 4 }               ACCEPT

p + q and 2p reach arbitrarily far from the caller's pointer with no constant at all. Param + Param is a deliberate, test-pinned MUST-ACCEPT (provenance/tests.rs, a6/a13), so this is by design, not an oversight.

Why this matters now

Today the main module declares a single fixed 64 KiB page, so an out-of-region reach traps at runtime. That is an accidental backstop, not a guarantee. Configurable linear memory (#210/#221, folded into #363) removes it: the same reaches become live, in-bounds writes into another module's region or into the shadow stack — and the emitted Rocq obligations for the main module assume its frames are intact.

Why the cheap fix does not work

Bounding the constant displacement on a Param was designed and adversarially reviewed twice. It fails three ways:

1. It buys no containment. The cheapest bypass (p + q) uses no constant, and is a MUST-ACCEPT.
2. It is unsound at call boundaries. ParamMask is a bitset recording which parameters, never how many times. root(p){ f(p+40000) } with f(q){ store(q+q, 0) } folds the entry displacement once while the value contains it twice — modelled 40000, actual 2p + 80000. A second variant cancels outright: f(p+70000, p-70000) with a select folds to displacement 0.
3. It destroys honest code. Any displacement bound widens the canonical caller-buffer walk (ptr = p; loop { store ptr; ptr += 4 }) to unbounded and rejects it, removing every iterating shared-memory external — memcpy, memset, strlen, sort.

What a real solution needs

• A numeric/interval abstract domain over addresses, replacing (or layering over) the current three-point taint lattice, tracking occurrence multiplicity so a repeated parameter cannot fold away.
• Declared pointee sizes for external fn parameters, threaded from the type checker into the linker, so "inside the caller's region" is expressible at all. Related: linker/type-checker: mut on external fn parameters as a linker-verified write-set declaration #333, which proposes mut on external parameters as a linker-verified write-set and would share the channel.

Known blocker

core/inference/src/wasm_link/validate.rs lowers TypeNode::Array { .. } and TypeNode::Custom(_) to a bare I32. A (param i32) therefore carries no declared pointee at all, and every in-tree Tier-B fixture is of that shape — so requiring a declared size would reject the entire existing Tier-B corpus. The channel has to be built before the analysis can consume it.

Acceptance

A merged external that addresses outside its caller's declared region is rejected, while the iterating caller-buffer idiom still links; the guarantee is stated in the linker's contract docs and pinned by adversarial repros (a green suite is not evidence for this class).

Refs: #363 (linker envelope, where this surfaced and where the documentation-only mitigation lands), #333, #210, #221.