# DF-0243 — PoC evidence pack

**Finding:** size_t underflow in `exec_shell_imgact` when `argv[0]` is longer
than `interpreter + fname` → alleged kernel panic.
**File:** `sys/kern/imgact_shell.c:117-129`
**Severity claimed:** High (local DoS / kernel panic).

## Result: NOT REPRODUCED — FALSE POSITIVE

The size_t subtraction at `imgact_shell.c:126` **does** wrap when
`strlen(argv[0]) > strlen(interp) + strlen(fname)`, but the wrap is
**mathematically equivalent to the intended signed subtraction**:

- `begin_envv` / `endp` are `char *` — adding `SIZE_MAX − K` to a pointer is
  identical (mod 2⁶⁴) to subtracting `K+1`, which is the correct intended
  delta. The pointer lands safely inside the `ARG_MAX + PATH_MAX` args buffer.
- `space` is `int` — `(int)((size_t)space − wrapped_offset)` truncates back to
  the correct value because `|length − offset| ≤ ARG_MAX + PAGE_SIZE ≪ INT_MAX`.

Result: no wild pointer, no memory corruption, no panic. The script runs
`/bin/sh /tmp/df0243_s` normally and prints `DF0243_SCRIPT_RAN`.

See **`VERDICT.md`** for the full line-by-line mechanism walkthrough.

## How to reproduce

```sh
./build.sh    # cc trigger.c, cc math_proof.c, create /tmp/df0243_s
./run.sh      # prints the math proof, then sweeps argv[0] lengths
```

### Expected on the audited master DEV kernel

```
=== math proof ===
begin_envv   0x1016   0x1016   0x1016   ALL MATCH
endp         0x1016   0x1016   0x1016   ALL MATCH
space        262122   262122   262122   ALL MATCH
=> the size_t wrap is mathematically equivalent to the signed op.

=== argv[0] length = 256 (and 1024, 4096, 32768, 131072, 262140) ===
DF0243_SCRIPT_RAN
DF0243_NO_PANIC: script executed normally -- underflow did not crash
```

No panic at any length. The guest stays up.

## Why no fix.diff

This is a pure false positive — the cited code is not actually vulnerable. The
finding's proposed if/else rewrite is semantically identical to the existing
modular arithmetic (it computes the same pointer deltas and same `space`).
A purely cosmetic readability patch *could* be entertained, but no security
fix is warranted and the instructions direct that pure false-positives omit
`fix.diff`.

## Files

| File            | Purpose                                                       |
|-----------------|---------------------------------------------------------------|
| `trigger.c`     | supplied PoC (unchanged)                                      |
| `setup.sh`      | supplied: creates `/tmp/df0243_s`                             |
| `math_proof.c`  | NEW: arithmetic proof that wrap == signed op for all 3 fields |
| `build.sh`      | exact build commands                                          |
| `run.sh`        | exact run command (math proof + argv[0] length sweep)         |
| `build.log`     | full final build (clean)                                      |
| `run.log`       | full decisive run                                             |
| `env.txt`       | guest environment                                             |
| `VERDICT.md`    | full narrative analysis                                       |
| `manifest.json` | machine-readable catalog                                      |