# DF-0243 — VERDICT: NOT REPRODUCED / FALSE POSITIVE

## One-line verdict

The size_t subtraction at `sys/kern/imgact_shell.c:126` **does** underflow when
`argv[0]` is longer than `interpreter + fname`, but the wrap is **mathematically
harmless**: pointer arithmetic is modular, so `begin_envv`/`endp` land at the
*correct* intended offset, and `space` (truncated back to `int`) also ends up
correct. There is **no wild pointer, no memory corruption, and no panic**.
Reproduced-as-panic: **no**. Classification: **false positive** (reviewer error
in modular-arithmetic reasoning).

## Evidence (decisive)

Running the supplied trigger (`trigger.c`, exec'ing `#!/bin/sh` with a long
`argv[0]`) at every length from 256 B up to 262 140 B (~`ARG_MAX`) — the kernel
**never** panicked, never logged a warning, and the guest stayed up. The script
ran `/bin/sh` and printed `DF0243_SCRIPT_RAN` every time:

```
$ ./trigger 256
DF0243_SCRIPT_RAN
DF0243_CHILD_EXIT code=0
DF0243_NO_PANIC: script executed normally -- underflow did not crash
```

(Same result for 1024, 4096, 32768, 131072, 262140.)

`math_proof.c` in this folder reproduces the exact arithmetic of
`imgact_shell.c:117-129` and shows the "buggy" path produces byte-for-byte the
same `begin_envv`, `endp`, and `space` as the intended signed semantics:

```
field        buggy-path      intended        expected        verdict
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.
```

## Mechanism walkthrough (why the reviewer was wrong)

The finding's claim hinges on this block (`sys/kern/imgact_shell.c:117-129`):

```c
offset += strlen(imgp->args->fname) + 1;     /* :117 */
length = strlen(imgp->args->begin_argv) + 1; /* :118 */

if (offset > imgp->args->space + length)     /* :120 */
    return (E2BIG);

bcopy(imgp->args->begin_argv + length, imgp->args->begin_argv + offset,
      imgp->args->endp - (imgp->args->begin_argv + length));  /* :123-124 */

offset -= length;                             /* :126 -- UNDERFLOW (size_t) */
imgp->args->begin_envv += offset;             /* :127 */
imgp->args->endp += offset;                   /* :128 */
imgp->args->space -= offset;                  /* :129 */
```

For `argv[0]` = 256 'A's, `#!/bin/sh`, fname `/tmp/df0243_s`:
- `offset` = 8 (interp) + 14 (fname+1) = **22**
- `length` = **257**
- `offset -= length` → 22 − 257 wraps to **`0xFFFFFFFFFFFFFF15`** (`SIZE_MAX − 234`).

The reviewer stopped here and concluded the wrapped value corrupts the pointers.
But:

### (1) `begin_envv` / `endp` are pointers — modular arithmetic saves them

Both are `char *` (`sys/sys/imgact.h:42-44`). Adding `0xFFFFFFFFFFFFFF15` to a
pointer is equivalent, mod 2⁶⁴, to **subtracting 235**:

```
begin_envv_new = begin_envv + (SIZE_MAX − 234)
               = (buf + 257) − 235
               = buf + 22          ← correct, well inside the ARG_MAX buffer
```

This is *exactly* what the code is trying to compute: the script's argument
buffer shrank from 257 bytes (old `argv[0]`) to 22 bytes
(`/bin/sh\0/tmp/df0243_s\0`), so `begin_envv`/`endp` must move **back** by
`length − offset = 235` bytes. The wrap produces precisely that result.

### (2) `space` is `int` — truncation also saves it

`space` is declared `int` (`sys/sys/imgact.h:46`). The expression
`space -= offset` evaluates `(size_t)space − offset` and truncates back to
`int`. The magnitude of the correction is `|length − offset|`, bounded by
`ARG_MAX + PAGE_SIZE ≈ 266 KB` — comfortably inside `int` range. Result:

```
space_new = 261887 + 235 = 262122   (== ARG_MAX − 22, exactly correct)
```

### (3) The E2BIG guard at `:120` is irrelevant to the crash claim

The finding notes the guard cannot prevent the underflow. That's true — but the
underflow itself is harmless per (1) and (2), so the guard being a no-op for
this case is fine.

### Why exec_copyout_strings also doesn't blow up

After imgact returns 0, `kern_exec.c:exec_copyout_strings` uses
`ARG_MAX − imgp->args->space` to size the copyout (`kern_exec.c:1166, 1220`)
and walks `argc` NUL-terminated strings from `begin_argv`
(`kern_exec.c:1231-1236`). With the corrected pointers above:
- `ARG_MAX − space = 262144 − 262122 = 22` → copies exactly
  `/bin/sh\0/tmp/df0243_s\0` to the user stack.
- `argc = 2` → walks two strings, matching the 22 bytes.

The new process gets `argv = ["/bin/sh", "/tmp/df0243_s"]` — the intended,
correct behavior. The leftover `AAAA...` bytes that were in `buf[22..256]` are
never read because `endp` correctly bounds the live region at `buf+22`.

## Why the "Recommended fix" in the finding is unnecessary

The proposed if/else rewrite:

```c
if (offset >= length) {
    size_t net = offset - length;
    imgp->args->begin_envv += net; ...
} else {
    size_t net = length - offset;
    imgp->args->begin_envv -= net; ...
}
```

…is **semantically identical** to the existing code. It computes the same
pointer deltas and the same `space` value. It is arguably more readable
(defense-in-depth / clarity), but it does **not fix a bug** because there is
no bug: the original modular arithmetic already produces the correct result in
both branches. A purely cosmetic hardening patch could be entertained for
readability, but no security fix is warranted.

## Files in this evidence pack

| File             | Purpose                                                       |
|------------------|---------------------------------------------------------------|
| `trigger.c`      | supplied PoC (unchanged): exec `#!/bin/sh` with long argv[0]  |
| `setup.sh`       | supplied: creates `/tmp/df0243_s`                             |
| `math_proof.c`   | **new**: proves the wrap == signed op for all 3 fields         |
| `build.sh`       | exact build commands                                          |
| `run.sh`         | exact run command (sweeps several argv[0] lengths)            |
| `build.log`      | full compiler output, final successful build                  |
| `run.log`        | full decisive run (256 B) + length sweep                       |
| `env.txt`        | guest uname, cc version, kern.argmax                           |
| `manifest.json`  | machine-readable catalog                                      |

No `panic.txt` (no panic occurred). No `fix.diff` (pure false positive — no code
change warranted).