# DF-0745 — PoC evidence pack

**Finding:** Dead `callout_active` guard + callback-owns-free design causes
double-free / TAILQ corruption race in `l2cap_request_free`.
**File:** `sys/netbt/l2cap_misc.c:168-173` (free) and `:190` (callback).
**Severity:** High (CWE-415 double-free, CWE-362 race).

## Reachability on this guest

The runtime netbt L2CAP path (`BTPROTO_L2CAP` socket + RTX timeout) is
**unreachable on this KVM guest**: there is no Bluetooth radio, and although
`/boot/kernel/netbt.ko` is installed as a loadable module, `BLUETOOTH` is not
in `X86_64_GENERIC` (`sys/conf/files:1614` marks `netbt/l2cap_misc.c` as
`optional bluetooth`), so the code is not in the running kernel and no real
L2CAP request/RTX timer ever fires here. This is the same harness-precedent
cluster as DF-0393/0594/0616/0732/0733 (wifi/netgraph/bt-unreachable).

The **primary proof is the deterministic userspace harness** (`harness.c`)
that transcribes the two racing threads verbatim from the audited source,
with a poisoned allocator and a fixed schedule that forces the SMP
interleaving the kernel source permits.

## Files

| file | what |
|------|------|
| `harness.c`        | Deterministic race transcription (BUGGY). Two pthreads model Thread A (softclock dispatching the RTX callout, whose callback calls `l2cap_request_free`) and Thread B (a concurrent external caller). Includes a faithful model of `_callout_cancel_or_stop` (clears ACTIVE unconditionally; recursive callback returns immediately; non-recursive blocks in `ssleep`), a poisoned `vm_zone` zalloc/zfree, TAILQ macros from `queue.h`, and a slab-reuse step. Prints `DOUBLE-FREE CONFIRMED` + `TAILQ CORRUPTION CONFIRMED`. |
| `harness_fixed.c`  | Same harness transcribing the **fix** (callback no longer frees; `l2cap_request_free` drains). Prints `FIXED: no double-free / no corruption`. |
| `build.sh`         | `cc -O2 -pthread -Wall -Wextra -o harness harness.c` |
| `run.sh`           | `./harness` |
| `build.log`        | Full build output (final). |
| `run.log`          | Full decisive BUGGY run (both scenarios CONFIRMED). |
| `run.2.log`,`run.3.log` | Stress repeats (deterministic). |
| `fix.diff`         | `git apply`-able unified diff against `sys/netbt/l2cap_misc.c`. |
| `fix_build.log`    | Full `make` of `netbt.ko` with the fix applied (clean, 0 errors). |
| `fix_run.log`      | Full FIXED-harness run (both scenarios clean). |
| `env.txt`          | Guest uname, kern.version, cc version, kernel-config / module notes. |
| `VERDICT.md`       | Full narrative analysis. |
| `manifest.json`    | Machine-readable artifact catalog. |

## Reproduce

```sh
ssh dfbsd-maxx /bin/sh      # unprivileged user (uid 1001)
cd poc/DF-0745
./build.sh && ./run.sh          # BUGGY: prints DOUBLE-FREE CONFIRMED etc.
cc -O2 -pthread -o harness_fixed harness_fixed.c && ./harness_fixed
                                # FIXED: prints "FIXED (clean)" for both scenarios
```

## Expected

| | BUGGY transcription | FIXED transcription |
|---|---|---|
| Scenario 1 (no reuse) | `DOUBLE-FREE CONFIRMED` (zfree count=2, `ZONE_ERROR_ALREADYFREE`) | `FIXED: no double-free` (zfree count=1) |
| Scenario 2 (slab reuse) | `TAILQ CORRUPTION CONFIRMED` + `FREE-OF-LIVE-OBJECT CONFIRMED` (live req on g_link2 unlinked) | `FIXED: no TAILQ corruption` (zfree count ≤ 1) |

## Fix validation (Phase 8)

1. `fix.diff` applies cleanly to `/usr/src` (`patch -p1` / `git apply --check`).
2. `cd /usr/src/sys/netbt && make` builds `netbt.ko` with the fix — **0 errors,
   0 warnings**; `l2cap_misc.o` now references `callout_drain` and no longer
   references `callout_stop`/`callout_active`.
3. The fixed-logic harness transcribes the same fix and shows the race is
   eliminated (see `fix_run.log`).

The runtime path needs Bluetooth hardware (absent), so the kernel cannot be
exercised live here; the harness transcription + module compile is the
validation. See `VERDICT.md` for the complete analysis.