# DF-4671 — VERDICT (verify run, 2026-10-15)

## Verdict

**NOT REPRODUCED as a fault-time race on this rig** — the mechanism is
**source-proven** (and every instrumentation confounder was hunted down
and eliminated, which is itself the bulk of this evidence pack), but the
unsynchronized window between `kmem_free(old bigbuf)` and
`bktr->bigbuf = buf` (bktr_core.c:1669-1672) proved empirically too
narrow to catch with a userspace faulter across ~1,700 kernel-verified
grow windows and roughly 10⁴ genuine first-fault `d_mmap`
re-executions. Two important DISCOVERIES about the surrounding
machinery are documented below; one of them (the held-mapping orphan
alias) is a deterministic, race-free manifestation of the same missing
buffer-lifetime bug and is reproduced (`holdcheck`).

## What is source-proven (traced line by line this run)

- The device pager re-executes `d_mmap` on the **first fault of every
  page index** of a cdev: device_pager.c:348-390 `old_dev_pager_fault`
  → `dev_dmmap` → `bktr_mmap` (bktr_os.c:656-685).
- `bktr_mmap` reads `alloc_pages` (bktr_os.c:680) and `bigbuf` (:683)
  with no lock; the METEORSETGEO grow block mutates both with no lock
  (bktr_core.c:1664-1681; `video_ioctl` contains no locking at all —
  verified by reading the whole function).
- During the window, `vtophys(old KVA)` still resolves: `kmem_free` →
  `vm_map_remove` → `vm_map_delete` (vm_map.c:3300-3370) performs **no
  `pmap_remove`** for the object-less `VM_MAPTYPE_NORMAL` entry and no
  page release (vm_map_entry_delete: unlink+dispose only), so the
  `pmap_kenter`'d PTEs survive until another `contigmalloc` reuses the
  KVA — a fault in the window maps the orphaned page. KVA reuse was
  observed directly (grow #32 reallocating the original RIG_INIT KVA
  `0xfffff80118aa0000`; per-grow KVA/PA traces in race_diag.log).

## Why it could not be caught here (measured, not hand-waved)

Two confounders had to be *proven* first — both invalidated naive rigs
and both are interesting in their own right:

1. **The old-style device pager's fake-page cache survives munmap**
   (`--seqcheck`, no concurrency at all): markers written into buffer
   generation 0 were re-served **64/64 pages** after munmap + 10 purely
   sequential grows. Consequence: a page fault only executes the
   driver's `d_mmap` for a pindex **never faulted before on that cdev**;
   every later fault is served from the cached fake page with a stale
   `phys_addr` and never re-queries. All "catches" from early rig
   versions (race2/race3: 464 events) were exactly this artifact and
   were disqualified. (This also *narrows the finding's premise*: the
   "re-queried on every fault" model holds only per first fault of a
   pindex.)
2. **`SETEORSETGEO` returns success without growing** when the requested
   geometry is not strictly larger, so a userspace epoch counter
   over-counts; fixed by keying all generation accounting on the
   kernel's `alloc_pages` (monotonic, changes only on real grows).

The final protocol (race11/race12): production grow path hammered by
1-2 grower threads (each grow kernel-verified via STATUS), 4 faulter
threads faulting only **never-faulted pindex groups** across 8 rig
cdevs (fresh pager objects per cdev → genuine `d_mmap` executions),
per-run nonces, marker generations sampled *after* faults (so
`marker.gen < pre-fault alloc_pages` can only mean the fault resolved a
page of an already-freed buffer — false-positive-proof). Result across
all hardened runs: **0 catches**. The window (the duration of one
`kmem_free` + two stores, sub-µs to low-µs) against a first-fault rate
of a few thousand per second and a per-buffer marked-page fraction of
1/8–1/4 gives an expected catch count of order 1 per several runs; we
ran out of practical amplification (leaked memory budget, serial
console spam from `contigmalloc` failures, faulter iteration cost)
before landing one.

## What IS deterministically demonstrated (consequence, not the race)

`--holdcheck` (no race, no threads): an RW mapping established on the
live buffer stays a **live, writable alias onto the orphaned pages**
after the grow path `kmem_free`s the buffer beneath it (64/64 marker
pages intact and a test store read back after 10 grows). The device
pager pins nothing, so with the stock code (pages never freed — DF-4672)
a held mapping is a permanent RW window onto orphaned kernel pages; on
real hardware the 0444 node limits an unprivileged holder to PROT_READ
(vm_mmap.c:368-371 denies PROT_WRITE without FWRITE), i.e. a persistent
read alias onto the old frame-buffer pages after they conceptually
ceased to exist. (With the contigfree() fix applied, those pages instead
return to the free queues while still aliased — see the residual note
in fix.diff; a complete fix needs pager-referenced buffer lifetimes.)

## Rig fidelity

Same as DF-4672/4673 (production `video_ioctl` grow path, production
`get_bktr_mem`/contigmalloc/kmem_free; `bktr_mmap` verbatim copy — the
only delta is the softc lookup, and the dropped minor-number decode on
the rig's video-function node).

## Honest classification

Per the audit table: expected marker absent, run exits 0, guest stays
up → **not_reproduced**, reproduced=0, impact=none *for the race claim
as filed*. The finding remains source-certain (CWE-367 TOCTOU is real in
the code); the practical severity hinges on a sub-microsecond window and
on the first-fault-only re-query behavior, both now measured. The
deterministic held-mapping alias above is the strongest demonstrated
consequence and belongs to the same root cause cluster (no buffer
lifetime tied to mappings).

## Files

| File | Purpose |
|---|---|
| `poc_race.c` | hardened race PoC + `--seqcheck` + `--holdcheck` modes |
| `race2.log`,`race3.log` | disqualified runs (pager-cache artifact, 464 events) |
| `race4.log`,`race5.log`,`race6.log`,`race_diag.log` | post-fix zero-catch runs, KVA/PA traces |
| `race11.log`,`race12.log` | final amplified protocol (8 cdevs, 4 faulters, dual growers), zero catches |
| `run.log` | consolidated record incl. seqcheck/holdcheck transcripts |
| `bktr_mmap_race.c` | original pass-1 hardware PoC (kept for reference) |
| `fix.diff` | consistent-sampling + fail-closed bktr_mmap hardening (validated to build; race not catchable so behavioral A/B limited to DF-4672/4673 aspects) |
| `env.txt`, `manifest.json`, `verdict.json` | environment + machine records |

## Fix status (batch validation)
Applied with the 36 sibling fix.diffs of this batch in findings/poc/_batch41/all_fixes.patch; single in-guest `make -j6 nativekernel KERNCONF=X86_64_GENERIC` completed RC=0 with zero errors under -Werror (full log: findings/poc/_batch41/fix_build8.log). Behavior A/B intentionally skipped for this Info-tier item.