Cbmc proof coverage expansion#375
Open
AniruddhaKanhere wants to merge 12 commits into
Open
Conversation
…essIncomingPacketTypeAndLength, DeserializeConnAck
…ect,Pingreq,Ack}PacketSize
…d CBMC proof MQTT_GetSubscribePacketSize did not validate pPacketSize before calling calculateSubscriptionPacketSize(), which writes through it. A caller passing pPacketSize == NULL would trigger a NULL-pointer write. The sibling MQTT_GetUnsubscribePacketSize already performs this check. Add the matching guard and a CBMC memory-safety proof (now VERIFICATION SUCCESSFUL) that covers the NULL parameter case.
handleIncomingPublish (PUBLISH) and handleIncomingAck (PINGRESP) handed a
partially-initialized MQTTDeserializedInfo_t to the application callback, leaving
pReasonCode indeterminate. Zero-initialize all such locals (matching the existing
'= { 0 }' usage in the disconnect/keep-alive paths) so every field is defined
before crossing the public callback boundary. Also applied to handlePublishAcks
and handleSubUnsubAck for consistency.
…ransmits,StatefulQoS,Connect}, SerializePublishHeaderWithoutTopic, UpdateDuplicatePublishFlag
…te proof addRecord() indexed records[ recordCount - 1U ] before any zero-count check. Calling MQTT_ReserveState (a public API) for QoS1/QoS2 on a context where the publish-record array was never configured (records == NULL, recordCount == 0, e.g. MQTT_InitStatefulQoS not called) made ( recordCount - 1U ) wrap to SIZE_MAX, an out-of-bounds read. Guard the compaction check with recordCount > 0U; the subsequent loop already no-ops for count 0, returning MQTTNoMemory. Add a CBMC proof for MQTT_ReserveState (now VERIFICATION SUCCESSFUL).
archigup
previously approved these changes
Jul 1, 2026
AniruddhaKanhere
force-pushed
the
cbmc-proof-coverage-expansion
branch
from
c264063 to
77e36ed
Compare
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
2 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
Test Steps
Checklist:
Related Issue
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.