# VERDICT — DF-4268 (wb_rxeof double-fetch of the DMA'd RX status word)

**Status: not_reproduced — false positive** (on the audited artifact — the shipped X86_64_GENERIC
kernel, gcc 8.3/CCVER=gcc80) — **impact none; confidence certain** (static
proof, dynamically corroborated). The source-level pattern is real and the
fix is recommended hardening; it is validated to remove even the residual
flags/length double-fetch from the machine code.

## Why the claimed OOB read is unreachable in this binary

The finding's chain: `rxstat` snapshot at `:973`; length checks re-read the
device word at `:983` (`< 60`) and `:984` (`> 1536`); the length USE re-reads
it again at `:1004`; a device rewrite between `:984` and `:1004` yields
`total_len` up to 16383, and `m_devget` (uipc_mbuf.c:2235, chained
`m_getl`+`bcopy`, no cap) then copies up to 16381 bytes from the 4096-byte
`wb_rxbufs[0]` → ~12 KB OOB read into a received packet.

The shipped binary does not contain that chain. `wb_rxeof` @
0xffffffff808dae30 loads the device word exactly twice per iteration:

```
+0x1c  mov (%rax),%eax        ; :973 snapshot — feeds OWN/MIIERR/LASTFRAG/
                               ; RXCMP/RXERR flag tests (register reuse)
+0x44  mov (%rdx),%esi        ; ONE re-read — feeds the MERGED range check
+0x4d  shr $0x10,%esi         ;   (len-60) > 1476 unsigned  == :983 AND :984
+0x53  sub $0x3c,%edx / cmp $0x5c4,%edx / ja error
+0x86  and $0x3fff,%esi       ; the SAME +0x44 fetch feeds the USE
+0x8d  sub $0x2,%esi          ; total_len-4+2 folded
+0x98  callq m_devget
```

The value that reaches `m_devget` is the same fetch that was range-checked;
a device rewrite between "check" and "use" has no window — there is no
second length fetch. (GCC legally merged `:983`/`:984`/`:1004` because the
`-fno-strict-aliasing` kernel build still lets it keep one load across the
 intervening flag arithmetic.) `wb_intr` calls out to `wb_rxeof` — there is
no inlined second copy (checked). The only surviving double-fetch is
flags-vs-length (snapshot `:973` vs the single length load), which cannot
produce an out-of-range length: the length is self-consistent.

## Dynamic corroboration (production handler raced)

Rig: DF-4266 KLD dispatch method; "chip" simulated by rewriting
`rx_list[0].wb_status` between
GOOD = 0xC0400300 (OWN|RXCMP|LAST|FIRST, len 64) and
HUGE = 0xFFFF0300 (same flags, len 16383) — both OWN=1, i.e. exactly the
mid-write-back transient the stock inverted loop (DF-4266) wrongly accepts;
GOOD/HUGE 4:1 duty; toggler pinned to CPU 3 (`usched bsd4:8`), dispatch
pinned to CPU 0 (`usched bsd4:1`).

* Stock kernel, 250 dispatches (~17 s), 221 frames delivered:
  **maxplen=60, WON=0** (run.race_production.dmesg.log). The handler
  processed frames the whole time under an actively adversarial length
  field; no delivered length ever exceeded 1536.
* Earlier run with the toggle value mis-set to RXLEN 1023 (still legal):
  276 deliveries, maxplen 1019 — every length it delivered was one that
  passed the merged check at its own fetch (run.race_production_v1_...log).
* Control: an EXACT-SEMANTICS transcription of the source (four distinct
  volatile fetches at :973/:983/:984/:1004) raced identically also produced
  ZERO wins across ~130 000 dispatches (userland µs chip ×1, ×3 streams,
  and a kernel ns-rate toggle thread — run.race_ctl_*.log): a software
  writer cannot land a store inside the reader's ~tens-of-ns fetch window
  (the reader acquires the cache line once and completes its loads
  locally). Only an in-flight DMA write could split the fetches of code
  that actually fetches twice — and the shipped binary's length path
  fetches once. Note the control could not be made to win even
  theoretically-honestly, which is why it is supporting, not primary,
  evidence; the disassembly is the proof.

## Fix assessment

`fix.diff` (use `rxstat` for the checks and the use) is the right hardening:
on the rebuilt kernel (fix_validated.diff, kernel #1) the disassembly shows
exactly ONE `mov (%rax),%eax` per iteration (the snapshot) — the `:983/
:984/:1004` re-fetch no longer exists in machine code — and the race again
delivers 188 frames, maxplen 60, WON 0 (run.race_production_fixed.log).
Because no divergent behaviour exists on this build either before or after
the patch, there was no behavioural delta to A/B: fix_status is
**not_testable** in the strict sense (nothing broken to observe being
fixed); the machine-code delta (2 loads → 1 load) is recorded instead.

## Rig incidents (documented, not the finding)

1. v1 toggle thread exited via `lwkt_exit()` → run-queue corruption →
   `panic: assertion "(ntd->td_flags & TDF_RUNNING) == 0" failed in
   lwkt_switch` AFTER the race had completed and printed its result
   (panic_rig_v1_togglethread.txt). DFly lwkt_create()d threads are not
   meant to exit; replaced by a userland sysctl-driven chip.
2. A later never-exiting (parked) kernel toggle thread triggered the same
   assertion class from softclock after ~10 s of remote spinning — race
   data again captured first (run.race_ctl_kernel.log tail).
3. An earlier toggle constant was mis-computed (RXLEN 1023 instead of
   16383) — the run is kept as the mid-range-length datapoint.

None of these involve the code under test.

## 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.