tcpip: verify UDP checksums within the declared datagram length

tcpip/README.md

@@ -35,7 +35,8 @@ bend-osdev-netheaders; byte strings are bend-osdev-bytes' `Octets`.
   default ISN function; see Extension points);
 * RFC 791, Internet Protocol (version 4), with fragmentation and reassembly;
 * RFC 792, Internet Control Message Protocol;
-* RFC 768, User Datagram Protocol;
+* RFC 768, User Datagram Protocol; [RFC 9868](https://www.rfc-editor.org/rfc/rfc9868.html)
+  sections 7–9 for the surplus area outside the UDP length and checksum;
 * RFC 826, An Ethernet Address Resolution Protocol (the packet reception
   algorithm);
 * RFC 1122, Requirements for Internet Hosts: Communication Layers (ARP cache
@@ -293,6 +294,14 @@ bend-osdev-bytes' laws of take, drop and append on Octets.
 
 ## Tests
 
+`ref/gen_udp.py` independently constructs UDP wire bytes and checksums using
+Python `struct`. Its receive regressions cover odd/even and empty payloads,
+surplus bytes, corruption inside the datagram, absent checksums, truncated
+headers/data, and invalid lengths. `ref/run.sh` runs these alongside the TCP
+model tests. The receiver validates length before checking only the declared
+UDP datagram; surplus bytes are ignored, without processing UDP options.
+
+
 * `check.bend`: five TCP walk-throughs through `sim.bend` (the three-way
   handshake, data both ways and both closes with TIME-WAIT; a segment lost
   three times, with the RTO doubling from 1 s to 2 s to 4 s; segments out of
@@ -343,6 +352,13 @@ values (`LAWS.bend`) and the order of `Nat` and words (`LAWS_order.bend`).
 
 ## Status
 
+2026-10-31: Bend 2.0.39 / Lean 4.34.0: `scripts/check.sh tcpip` and
+`VERDICT=1 scripts/check.sh tcpip` pass (all three proof files, runtime
+examples, 100 TCP model cases / 6671 trace lines, and 86 UDP cases).
+`scripts/deps.sh tcpip`, the public-interface audit, and the packet proof
+generator's `--check` pass. Linux TAP integration is skipped on this VM
+(no usable namespace/TAP setup).
+
 Bend 2.0.39 (2026-10-26, native, three packages at a time): `PROOF.bend`
 (2 s, 0.35 GB peak; `--verdict` 5 s, 0.41 GB peak), `PROOF_packet.bend`
 (3 s, 0.35 GB peak; `--verdict` 5 s, 0.40 GB peak) and `PROOF_stream.bend`

tcpip/VERSION

@@ -1 +1 @@
-0.1.0.0
+0.1.0.1

tcpip/ref/.gitignore

@@ -1,3 +1,5 @@
 cases.bend
 expected.txt
 __pycache__/
+udp_cases.bend
+udp_expected.txt

tcpip/ref/gen_udp.py

@@ -0,0 +1,78 @@
+#!/usr/bin/env python3
+"""UDP receive vectors from Python's struct and RFC 768 Internet checksum.
+
+Generate wire bytes independently of netheaders, including surplus area bytes
+(RFC 9868 sections 7-9), corruption, absent checksums and invalid lengths.
+"""
+from pathlib import Path
+import struct
+
+
+def checksum(data):
+    data += b"\0" * (len(data) % 2)
+    total = sum(struct.unpack("!%dH" % (len(data) // 2), data))
+    while total >> 16:
+        total = (total & 65535) + (total >> 16)
+    return (~total) & 65535
+
+
+def datagram(payload, length=None, zero=False):
+    length = 8 + len(payload) if length is None else length
+    wire = struct.pack("!HHHH", 1234, 53, length, 0) + payload
+    if not zero:
+        pseudo = struct.pack("!IIBBH", 1, 2, 0, 17, len(wire))
+        ck = checksum(pseudo + wire) or 65535
+        wire = wire[:6] + struct.pack("!H", ck) + wire[8:]
+    return wire
+
+
+def octets(data):
+    return "B.Octets.of_list([%s])" % ", ".join(map(str, data))
+
+
+cases = []
+for size in range(6):
+    payload = bytes(range(65, 65 + size))
+    for surplus in (b"", b"\1", b"\1\2", b"\0\0\xff"):
+        for zero in (False, True):
+            wire = datagram(payload, zero=zero) + surplus
+            cases.append((wire, payload))
+            if not zero:
+                bad = bytearray(wire)
+                bad[8 if payload else 0] ^= 1
+                cases.append((bytes(bad), None))
+# Invalid lengths must fail even with an absent checksum.
+for length in (0, 1, 7, 12, 65535):
+    cases.append((datagram(b"hi!", length, zero=True), None))
+# A truncated header, and a checksum-bearing truncated datagram.
+for size in range(8):
+    cases.append((datagram(b"hi!")[:size], None))
+cases.append((datagram(b"hi!")[:-1], None))
+
+source = """import Base
+import ../../bytes/bytes.bend as B
+import ../udp.bend as U
+
+def matches(actions: List<&2, U.UdpAction>, want: Maybe<&2, B.Octets>) -> Bool:
+  match actions want:
+    case Nil{} None{}:
+      True{}
+    case Con{U.UdpDeliver{tag, src, sport, dport, data}, Nil{}} Some{expected}:
+      Bool.and(U32.is_eq(tag, 9), Bool.and(U32.is_eq(src, 1), Bool.and(U32.is_eq(sport, 1234), Bool.and(U32.is_eq(dport, 53), B.Octets.is_eq(data, expected)))))
+    case _ _:
+      False{}
+
+def received(wire: B.Octets) -> List<&2, U.UdpAction>:
+  st = Pair.fst(U.UdpState, List<&2, U.UdpAction>, U.Udp.bind(U.UdpState.new(2), 53, 9))
+  Pair.snd(U.UdpState, List<&2, U.UdpAction>, U.Udp.recv(st, 1, 2, wire))
+
+def main() -> IO(Unit):
+  do IO<Unit>:
+"""
+for wire, payload in cases:
+    want = "None{}" if payload is None else "Some{%s}" % octets(payload)
+    source += "    IO.print(Bool.show(matches(received(%s), %s)))\n" % (octets(wire), want)
+root = Path(__file__).resolve().parent
+(root / "udp_cases.bend").write_text(source)
+(root / "udp_expected.txt").write_text("True\n" * len(cases))
+print(len(cases))

tcpip/ref/run.sh

@@ -18,6 +18,13 @@ if [ "$got" != "$(cat expected.txt)" ]; then
   exit 1
 fi
 model="model: $n match"
+u=$(python3 gen_udp.py) || exit 1
+got=$("${bend[@]}" udp_cases.bend 2>&1)
+if [ "$got" != "$(cat udp_expected.txt)" ]; then
+  diff <(cat udp_expected.txt) <(printf '%s\n' "$got") | head -20
+  exit 1
+fi
+model="$model; UDP: $u match"
 if unshare -rn true 2> /dev/null && [ -c /dev/net/tun ] && command -v ip > /dev/null && command -v ping > /dev/null; then
   tmp=$(mktemp -d)
   trap 'rm -rf "$tmp"' EXIT

tcpip/udp.bend

@@ -113,10 +113,27 @@ def Udp.recv.go(ok: Bool, +st: UdpState, +src: U32, +dst: U32, +dg: B.Octets) ->
     case True{}:
       Udp.recv.header(NU.UdpHeader.parse(dg), st, src, dst, dg)
 
-# a datagram arrives: its checksum must verify (or be zero) and its length
-# field fit
+def Udp.recv.trim_length(ok: Bool, +st: UdpState, +src: U32, +dst: U32, +dg: B.Octets, n: Nat) -> List<&2, UdpAction>:
+  match ok:
+    case False{}:
+      Nil{}
+    case True{}:
+      +trimmed = B.Octets.take(n, dg)
+      Udp.recv.go(NU.UdpHeader.verify_ipv4(src, dst, trimmed), st, src, dst, trimmed)
+
+def Udp.recv.trim_header(r: Result<&2, &2, N.NetError, NU.UdpHeader>, +st: UdpState, +src: U32, +dst: U32, +dg: B.Octets) -> List<&2, UdpAction>:
+  match r:
+    case Fail{e}:
+      Nil{}
+    case Done{NU.UdpHeader{sp, dp, len, ck}}:
+      +n = U32.to_nat(len)
+      Udp.recv.trim_length(Bool.and(Nat.is_ge(n, 8n), Nat.is_le(n, B.Octets.len(dg))), st, src, dst, dg, n)
+
+# RFC 768: the checksum covers only the declared UDP length. The IPv4
+# payload may contain a surplus area (RFC 9868 sections 7-9); validate the
+# length before trimming, so take cannot hide a truncated datagram.
 def Udp.recv(+st: UdpState, +src: U32, +dst: U32, +dg: B.Octets) -> Pair(UdpState, List<&2, UdpAction>):
-  (st, Udp.recv.go(NU.UdpHeader.verify_ipv4(src, dst, dg), st, src, dst, dg))
+  (st, Udp.recv.trim_header(NU.UdpHeader.parse(dg), st, src, dst, dg))
 
 # Sending: the header, with its checksum over the pseudo-header from our
 # address to dst; at most 65507 bytes of data fit an IPv4 packet