# VERDICT — DF-4007

**Status: inconclusive at runtime (no GPU on the audit guest); source-certain;
control flow model-verified on the guest.**

## What is proven, and how

1. **Source (kernel tree):** the second loop of `eb_move_to_gpu`
   (`i915_gem_execbuffer.c:1860-1875`) returns at `:1867` when
   `i915_vma_move_to_active()` fails, after having unreserved entries [0, i)
   via the BY-VALUE `__eb_unreserve_vma(vma, flags)` (`:1870`, `:427-435`) and
   `i915_vma_put()` for `__EXEC_OBJECT_HAS_REF` (`:1873`) — **without clearing
   those bits in `eb->flags[i]** and with `eb->exec` still set (`eb->exec = NULL`
   happens only at `:1876`). The ioctl error path `i915_gem_do_execbuffer`
   `:2442-2444` therefore calls `eb_release_vmas()` (`:857-879`), which
   unreserves (`:873-874`) and puts (`:876-877`) every entry whose flags still
   claim `HAS_PIN`/`HAS_REF` — a second drop of the same pin/fence/reference.
   The drops are raw decrements (`__i915_vma_unpin` = `vma->flags--`,
   `i915_vma.h:323-326`; `__i915_vma_unpin_fence` = `vma->fence->pin_count--`,
   `:392-396`; `i915_vma_put` = `i915_gem_object_put`, `:222`), guarded only by
   no-op GEM_BUG_ONs in non-DEBUG builds (`i915_gem.h:60-62`) → underflow →
   premature unbind / premature GEM object free → UAF class.
2. **Trigger is unprivileged but narrow:** `i915_vma_move_to_active` fails with
   `-ENOMEM` from `active_instance()`'s rbtree kmalloc (`i915_vma.c:981-989`),
   which requires (a) the vma already active from a different context
   (last_active cache miss — attacker arranges by sharing one BO across two
   contexts) and (b) the small DRM-slab alloc to fail (memory-pressure/slab
   exhaustion spray). Not deterministic, but a standard pressure primitive.
3. **Model verification on the guest** (`model_df4007.c`, run.log): exact
   replication of the two functions with mock refcounts. BASELINE with the
   failure injected at entry 1 → entry 0 `pin=-1 fence=-1`; failure at entry 2 →
   additionally the cmdparser shadow (the only HAS_REF user, `:1963-1965`)
   `objrefs=1 < floor 2` (object-ref underflow). Control (no failure) and
   PATCHED (fix.diff applied) runs are perfectly balanced — including the subtle
   part the model caught: clearing only `__EXEC_OBJECT_RESERVED` is NOT enough;
   `HAS_REF` must also be cleared or the shadow ref is still double-put.
4. **Runtime:** `poc_df4007.c` builds cleanly on the guest but `/dev/dri` does
   not exist (virtio-only GPU, env.txt) → exit 77 per DF-3634 conventions. The
   ioctl-level trigger needs real Intel hardware.

## Upstream status

The DragonFly file matches torvalds/linux **v4.19** `i915_gem_execbuffer.c`
byte-for-byte in this control flow (fetched and compared during verification).
Upstream eliminated the class later: the v5.2 ww-mutex rework restructured the
loop (unreserve unconditional) and v5.6 made `i915_vma_move_to_active()` void,
removing the mid-loop error return entirely.

## Fix validation

`fix.diff` (by-ref `eb_unreserve_vma(vma, &eb->flags[i])` + HAS_REF clear):
model-verified balanced; applied to guest /usr/src together with the fiji fixes,
full nativekernel rebuild completed (fix_build.log), reverted after validation.

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