Repository navigation
Add CBMC memory-safety proofs for MQTTPropAdd UTF-8 property APIs - #385
Merged
AniruddhaKanhere merged 5 commits intoAug 18, 2026
Merged
AniruddhaKanhere merged 5 commits into
AniruddhaKanhere merged 5 commits into
Conversation
Adds a CBMC proof harness for MQTTPropAdd_AuthData, a public entry point into the file-local addPropUtf8 helper. The proof confirms the buffer bounds check reserves space for the full encoding (1 byte property ID + 2 byte UTF-8 length prefix + the string) and never writes past the property builder buffer.
Adds a CBMC proof harness for MQTTPropAdd_AuthMethod, a public entry point into the file-local addPropUtf8 helper. The proof confirms the buffer bounds check reserves space for the full encoding (1 byte property ID + 2 byte UTF-8 length prefix + the string) and never writes past the property builder buffer.
Adds a CBMC proof harness for MQTTPropAdd_ContentType, a public entry point into the file-local addPropUtf8 helper. The proof confirms the buffer bounds check reserves space for the full encoding (1 byte property ID + 2 byte UTF-8 length prefix + the string) and never writes past the property builder buffer.
Adds a CBMC proof harness for MQTTPropAdd_CorrelationData, a public entry point into the file-local addPropUtf8 helper. The proof confirms the buffer bounds check reserves space for the full encoding (1 byte property ID + 2 byte UTF-8 length prefix + the string) and never writes past the property builder buffer.
Adds a CBMC proof harness for MQTTPropAdd_ResponseTopic, a public entry point into the file-local addPropUtf8 helper. The proof confirms the buffer bounds check reserves space for the full encoding (1 byte property ID + 2 byte UTF-8 length prefix + the string) and never writes past the property builder buffer.
AniruddhaKanhere
force-pushed
the
add-mqttpropadd-utf8-proofs
branch
from
August 17, 2026 21:39
02c2beb to
1c70295
Compare
AniruddhaKanhere
enabled auto-merge (squash)
August 17, 2026 21:45
allanli4
approved these changes
Aug 17, 2026
kstribrnAmzn
approved these changes
Aug 18, 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 proofs for the remaining public
MQTTPropAdd_*APIs that serialize a UTF-8 string property through the file-localaddPropUtf8helper:MQTTPropAdd_AuthDataMQTTPropAdd_AuthMethodMQTTPropAdd_ContentTypeMQTTPropAdd_CorrelationDataMQTTPropAdd_ResponseTopicEach proof confirms the bounds check in
addPropUtf8reserves space for the full on-wire encoding (1 byte property ID + 2 byte UTF-8 length prefix + the string itself) and never writes past the end of the property builder buffer. This complements the existingMQTTPropAdd_ReasonStringproof, bringing per-API proof coverage to the full set of UTF-8 property builders.Each harness allocates a property builder backed by a buffer of exactly
bufferLengthbytes with a nondeterministiccurrentIndex, bounds the string length, and lets the string pointer be possibly NULL so the parameter-validation branches are also exercised.MQTTPropAdd_ResponseTopicadditionally usesmemchrto reject wildcard characters, so its proof links the existingstubs/memchr.c.Test Steps
Ran each proof locally with CBMC 6.9.0; all report
VERIFICATION SUCCESSFUL. Confirmed the proofs are non-trivial by temporarily reintroducing the off-by-one in theaddPropUtf8bounds check, which makes the proofs report an out-of-bounds write inaddPropUtf8.Checklist:
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.