Skip to content

tcpip: verify UDP checksums within the declared datagram length - #2

Merged
ScottMoore0 merged 1 commit into
ScottMoore0:mainfrom
EpsilonPhoenix:t3/udp-checksum-surplus-bytes
Nov 3, 2026
Merged

ScottMoore0 merged 1 commit into
ScottMoore0:mainfrom
EpsilonPhoenix:t3/udp-checksum-surplus-bytes

Conversation

@EpsilonPhoenix

Copy link
Copy Markdown
Contributor

Valid checksummed UDP datagrams with trailing bytes in the IPv4 payload were dropped because receive verification included the surplus area in both the checksum and pseudo-header length. For example, a length-11 datagram carrying hi! stops verifying when one surplus byte is appended.

Validate the UDP length (at least eight bytes and no longer than the received buffer), then trim to that length before checksum verification. Continue to accept absent IPv4 checksums and discard truncated or corrupt datagrams. This follows RFC 768 and RFC 9868 sections 7–9; surplus bytes are ignored without implementing UDP options.

Preserve the existing universal packet-receive law and update its proof and generator. Add 86 independently constructed Python wire/checksum cases to the reference runner; 18 fail before the fix and all pass afterward.

Validation with Bend 2.0.39 and Lean 4.34.0:

  • scripts/check.sh tcpip and VERDICT=1 scripts/check.sh tcpip
  • scripts/deps.sh tcpip and python3 scripts/internals.py tcpip
  • python3 ref/gen_packet.py --check from tcpip/
  • 100 TCP model cases (6,671 trace lines) and 86 UDP receive cases match. Linux TAP integration is skipped because this VM lacks the required namespace/TAP setup.

Independent GPT-6.1-Terra medium review using review-agent returned no findings.

@ScottMoore0
ScottMoore0 merged commit e0e59ed into ScottMoore0:main Nov 3, 2026
@EpsilonPhoenix
EpsilonPhoenix deleted the t3/udp-checksum-surplus-bytes branch November 3, 2026 17:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants