# DF-0046 — Verdict

**Verdict: REPRODUCED (logic bug / POSIX non-compliance / local DoS). Fix VALIDATED.**

## Summary

The DragonFlyBSD SysV semaphore implementation never enforces the `SEMVMX`
(32767) upper bound that POSIX/SVID requires. `semval` is a `u_short`
(`sys/kern/sysv_sem.c:40`); three write sites mutate it without any check
against `SEMVMX`:

| Path        | Citation                       | Defect                                           |
|-------------|--------------------------------|--------------------------------------------------|
| `semop` +op | `sys/kern/sysv_sem.c:849`      | `semptr->semval += sopptr->sem_op;` — no bound   |
| `SETVAL`    | `sys/kern/sysv_sem.c:530`      | `semptr->semval = real_arg.val;` — `int`→`u_short` trunc, no bound |
| `semexit`   | `sys/kern/sysv_sem.c:1139`     | `semptr->semval += adjval;` — no bound           |

The negative-`sem_op` branch (`sys/kern/sysv_sem.c:827`) *does* have the
lower-bound analogue (`if (semptr->semval + sopptr->sem_op < 0)`), confirming
the upper-bound omission is the bug, not an intentional design. The in-tree
comment at `sys/kern/sysv_sem.c:160` itself admits `"SEMVMX unused - user param"`.

## Mechanism (trigger → primitive → effect)

1. **Trigger** — unprivileged user calls `semget(IPC_PRIVATE, ...)` then
   `semop` with large positive `sem_op` values (each ≤ 32767, the `short`
   range). No privilege check beyond the set's IPC mode bits.
2. **Primitive** — the positive-op branch at `:849` does
   `semptr->semval += sopptr->sem_op` with no `SEMVMX` check. Four `+32767`
   ops accumulate `0 + 4×32767 = 131068`, which wraps the `u_short` to
   `131068 mod 65536 = 65532`. The wrap is silent (no `ERANGE`).
3. **Effect (demonstrated two ways)**:
   - **POSIX violation**: `semval = 65532 > SEMVMX (32767)` with no `ERANGE`.
     A POSIX-compliant kernel would have returned `ERANGE` at the second op.
   - **Wrap-to-0 breaks mutual exclusion**: `+32767 + +32767 + +2 = 65536`
     wraps `semval` to exactly 0 (logical value 65536). A process blocked in
     `semop(0)` (wait-for-zero, `semzcnt` waiter) is spuriously released —
     the PoC's forked child exits with code 42 (released) where it should
     have blocked indefinitely. This breaks SysV semaphore mutual exclusion
     for any consumer that relies on the zero state.

## Impact

IPC-state integrity / POSIX non-compliance / local DoS via broken SysV
semaphore synchronization. **No kernel memory corruption** — the wrap stays
inside the self-contained `u_short` field; there is no write primitive, no
adjacent-object corruption, no escalation path. Rated **Low** (matches the
finding's severity). The wrap-to-0 spurious-release is the most
security-relevant consequence (broken cross-process mutual exclusion), but
it requires a victim process sharing the semaphore set and using
wait-for-zero semantics.

## Exploit chain

**none** — this is a pure logic/integer bug with no memory-corruption
primitive. `semval` is a self-contained `u_short`; the wrap does not corrupt
adjacent kernel memory. There is no write primitive to convert to control
flow, no slab grooming, no function pointer to hijack. The realistic impact
ceiling is the wrap-to-0 spurious wakeup demonstrated in observation [2],
which is a synchronization-integrity / local-DoS issue.

## PoC changes

The original `sem_wrap.c` made a "rollback leaves non-zero" claim that does
not hold (u_short arithmetic is closed under mod 65536, so symmetric
add/subtract in the rollback returns to the original value — the rollback
correctly lands at 0). I replaced that false claim with a sharper, more
security-relevant demonstration: the **wrap-to-0 spurious release** of a
wait-for-zero child, which is the actual broken-mutual-exclusion primitive.
Also added a supplementary `fix_test.c` that exercises both the positive-op
and SETVAL paths for use on the patched kernel.

## Fix validation (Phase 8)

Authored `fix.diff` adding `SEMVMX` enforcement at all three write sites:

1. **positive-op** (`:849`): `if ((int)semptr->semval + sopptr->sem_op > seminfo.semvmx) { eval = ERANGE; lwkt_relpooltoken(semptr); goto done; }` — matches the finding's proposed pattern and the existing negative-branch style.
2. **SETVAL** (`:530`): `if (real_arg.val < 0 || real_arg.val > seminfo.semvmx) { eval = ERANGE; break; }` — also catches the `int`→`u_short` truncation case (e.g. `val = 70000` would have stored `70000 & 0xffff = 4464`).
3. **semexit** (`:1139`): clamp to `SEMVMX` (semexit cannot fail; the process is exiting). Defense-in-depth — once semop and SETVAL are bounded, semexit's input state is always ≤ SEMVMX, so the clamp is a backstop.

**Before/after (clean comparison on the same guest):**

| Kernel | `sem_wrap` observation [1] (4×+32767) | `sem_wrap` observation [2] (wrap-to-0) | `fix_test` SETVAL `=SEMVMX+1` |
|--------|---------------------------------------|----------------------------------------|-------------------------------|
| `#0` unpatched baseline | `semval = 65532`, no ERANGE (**BUG**) | child **RELEASED** (broken mutex) | n/a (would store 4464) |
| `#1` patched (fix.diff) | `op2` returns **ERANGE** (**FIXED**) | unreachable (op2 fails first) | returns **ERANGE** (**FIXED**) |

Patched kernel: `DragonFly 6.5-DEVELOPMENT #1: Sun Jul 12 23:47:04 UTC 2026`,
`sha256(/boot/kernel/kernel) = 425bca4973a730ceafb4cda4a71b64cd26e10c45d41e26eb55e26e171243619e`.
Smoke test (normal `-1` op) still works (`semval=32766`), no regression.

## Recommended fix

`fix.diff` **supersedes** the finding markdown's proposal (which only patched
the positive-op branch). The verified fix covers all three write sites
(positive-op, SETVAL, semexit) for a complete bound enforcement. The finding
markdown's `## Recommended fix` only showed the positive-op hunk and noted
"and the analogous check at SETVAL :530 and semexit :1139" — `fix.diff`
implements exactly that, with semexit using a clamp (not ERANGE) since it
cannot fail.
