# DF-0743 — struct greip/mobip_h overlay assumes ip_hl == 5

The GRE input handlers in `sys/netinet/ip_gre.c` overlay `struct greip` /
`struct mobip_h` at `mtod(m)` and dereference the GRE/mobile fields at FIXED
byte offsets (20/22/24/28) that correspond to a 20-byte (`ip_hl==5`) IP
header. When the outer encapsulating IP header carries IP options
(`ip_hl > 5`), those fixed offsets land on the IP-OPTION bytes, not the GRE /
mobile header → deterministic misparse.

Sibling of DF-0740 / DF-0741 / DF-0742 (same `if_gre` module), but an
**orthogonal** bug: DF-0742's missing-`m_pullup` fix does NOT close it
(contiguity is irrelevant — the overlay reads the wrong offset regardless).

## Files

| file | purpose |
|------|---------|
| `harness.c` | **PRIMARY proof** — deterministic userspace harness replicating the kernel's exact struct-overlay derefs; shows every field is misread when `ip_hl > 5`. |
| `live_trigger.c` | live in-kernel discriminator: sends GRE packets with/without IP options to a configured gre0. |
| `live_run.sh` | sets up gre0, runs tcpdump on gre0, injects A+B, reports capture count (1=buggy, 2=fixed). |
| `build.sh` / `run.sh` | build & run the harness. |
| `fix.diff` | standalone `git apply`-able fix (compute overlay ptr from `ip_hl*4`). |
| `VERDICT.md` | full narrative. |
| `run.log` | harness output (the misparse proof). |
| `live_run_buggy.log` | live discriminator on the BUGGY baseline (1 capture). |
| `fix_baseline.txt` / `fix_patched.txt` | before/after live discriminator. |
| `fix_build.log` | single-fix if_gre module build (`-Werror`, rc=0). |
| `env.txt` | guest environment. |
| `manifest.json` | artifact catalog. |

## Reproduce

### Primary (deterministic harness — no privilege, no setup)
```
./build.sh && ./run.sh
```
Expected: `VERDICT: MISPARSE PROVEN (vulnerable)` — every overlay field
mismatches the correct `ip_hl*4`-aware read; accept/drop and checksum
decisions diverge.

### Live in-kernel discriminator (needs root)
```
cc -O2 -Wall -o live_trigger live_trigger.c
./live_run.sh
```
Expected on the **buggy** kernel: `1 packet captured` (packet B with
`ip_hl=7` dropped by the misparse).
Expected on the **fixed** kernel: `2 packets captured` (packet B
decapsulated; `id 48059` / 0xBBBB appears in the tcpdump).

## Impact
Read-class misparse / DoS (+ possible inner-src/dst rewrite in mobile mode).
No memory-corruption write primitive → no escalation.