Add CBMC proofs for additional receive-path parsing functions - #1360
Merged
AniruddhaKanhere merged 2 commits intoAug 20, 2026
Merged
Conversation
Adds minimal-assumption CBMC proof harnesses for previously-unproven functions that parse untrusted network input: - BitConfig byte readers (init, read_8/16/32, read_uc, peek_last) - DNS answer record parsing (parseDNSAnswer) - TCP header option parsing (prvSingleStepTCPHeaderOptions, prvReadSackOption) - DHCPv6 option handling (sub-option, status code, option-length validation) - IPv4 packet acceptance (prvAllowIPPacketIPv4) - ICMP echo reply handling (prvProcessICMPEchoReply) Buffers are allocated to exactly their modeled length with nondeterministic contents so any over-read surfaces as a genuine out-of-bounds access.
AniruddhaKanhere
enabled auto-merge (squash)
August 20, 2026 15:58
cookpate
approved these changes
Aug 20, 2026
allanli4
approved these changes
Aug 20, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Adds CBMC memory-safety proof harnesses for several receive-path parsing
functions that previously lacked proof coverage. Each harness follows the
existing proof conventions and uses minimal assumptions: input buffers are
allocated to exactly their modeled length with nondeterministic contents, so
any over-read is reported as a genuine out-of-bounds access.
New proofs:
xBitConfig_init,ucBitConfig_read_8,usBitConfig_read_16,ulBitConfig_read_32,xBitConfig_read_uc,pucBitConfig_peek_last_index_ucparseDNSAnswerprvSingleStepTCPHeaderOptions,prvReadSackOptionprvDHCPv6_subOption,prvDHCPv6_handleStatusCode,prvIsOptionLengthValidprvAllowIPPacketIPv4prvProcessICMPEchoReplyTest Steps
Run via
test/cbmc/proofs/run-cbmc-proofs.py. All added proofs verify successfully.Checklist