diff --git a/cbmc/include/mqtt_cbmc_state.h b/cbmc/include/mqtt_cbmc_state.h index ed11579c..2f9d44f6 100644 --- a/cbmc/include/mqtt_cbmc_state.h +++ b/cbmc/include/mqtt_cbmc_state.h @@ -50,6 +50,9 @@ MQTTPacketInfo_t * allocateMqttPacketInfo( MQTTPacketInfo_t * pPacketInfo ); * @param[in] pPacketInfo #MQTTPacketInfo_t object to validate. * * @return True if the #MQTTPacketInfo_t object is valid, false otherwise. + * + * @note A NULL object is a valid object. This is for coverage of the NULL + * parameter checks in the function under proof. */ bool isValidMqttPacketInfo( const MQTTPacketInfo_t * pPacketInfo ); @@ -68,6 +71,9 @@ MQTTPublishInfo_t * allocateMqttPublishInfo( MQTTPublishInfo_t * pPublishInfo ); * @param[in] pPublishInfo #MQTTPublishInfo_t object to validate. * * @return True if the #MQTTPublishInfo_t object is valid, false otherwise. + * + * @note A NULL object is a valid object. This is for coverage of the NULL + * parameter checks in the function under proof. */ bool isValidMqttPublishInfo( const MQTTPublishInfo_t * pPublishInfo ); @@ -86,6 +92,9 @@ MQTTConnectInfo_t * allocateMqttConnectInfo( MQTTConnectInfo_t * pConnectInfo ); * @param[in] pConnectInfo #MQTTConnectInfo_t object to validate. * * @return True if the #MQTTConnectInfo_t object is valid, false otherwise. + * + * @note A NULL object is a valid object. This is for coverage of the NULL + * parameter checks in the function under proof. */ bool isValidMqttConnectInfo( const MQTTConnectInfo_t * pConnectInfo ); @@ -96,7 +105,7 @@ bool isValidMqttConnectInfo( const MQTTConnectInfo_t * pConnectInfo ); * * @return NULL or allocated #MQTTFixedBuffer_t memory. */ -MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pBuffer ); +MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pFixedBuffer ); /** * @brief Validate a #MQTTFixedBuffer_t object. @@ -104,7 +113,35 @@ MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pBuffer ); * @param[in] pBuffer #MQTTFixedBuffer_t object to validate. * * @return True if the #MQTTFixedBuffer_t object is valid, false otherwise. + * + * @note A NULL object is a valid object. This is for coverage of the NULL + * parameter checks in the function under proof. */ -bool isValidMqttFixedBuffer( const MQTTFixedBuffer_t * pBuffer ); +bool isValidMqttFixedBuffer( const MQTTFixedBuffer_t * pFixedBuffer ); + +/** + * @brief Allocate an array of #MQTTSubscribeInfo_t objects. + * + * @param[in] pSubscriptionList #MQTTSubscribeInfo_t object information. + * @param[in] subscriptionCount The amount of #MQTTSubscribeInfo_t objects to allocate. + * + * @return NULL or allocated #MQTTSubscribeInfo_t array. + */ +MQTTSubscribeInfo_t * allocateMqttSubscriptionList( MQTTSubscribeInfo_t * pSubscriptionList, + size_t subscriptionCount ); + +/** + * @brief Validate an array of #MQTTSubscribeInfo_t objects. + * + * @param[in] pSubscriptionList #MQTTSubscribeInfo_t object information. + * @param[in] subscriptionCount The length of #MQTTSubscribeInfo_t objects in the pSubscriptionList. + * + * @return True if the #MQTTSubscribeInfo_t is valid. + * + * @note A NULL object is a valid object. This is for coverage of the NULL + * parameter checks in the function under proof. + */ +bool isValidMqttSubscriptionList( MQTTSubscribeInfo_t * pSubscriptionList, + size_t subscriptionCount ); #endif /* ifndef MQTT_CBMC_STATE_H_ */ diff --git a/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c b/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c index e13fdb3c..e9042686 100644 --- a/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c +++ b/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c @@ -28,11 +28,11 @@ void harness() { - MQTTPacketInfo_t * pIncomingPacket = NULL; + MQTTPacketInfo_t * pIncomingPacket; uint16_t * pPacketId; bool * pSessionPresent; - pIncomingPacket = allocateMqttPacketInfo( pIncomingPacket ); + pIncomingPacket = allocateMqttPacketInfo( NULL ); __CPROVER_assume( isValidMqttPacketInfo( pIncomingPacket ) ); MQTT_DeserializeAck( pIncomingPacket, diff --git a/cbmc/proofs/MQTT_DeserializeAck/Makefile b/cbmc/proofs/MQTT_DeserializeAck/Makefile index 0a2dda63..95bca32b 100644 --- a/cbmc/proofs/MQTT_DeserializeAck/Makefile +++ b/cbmc/proofs/MQTT_DeserializeAck/Makefile @@ -11,7 +11,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(PROOFDIR)/../../sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c include ../Makefile.common diff --git a/cbmc/proofs/MQTT_DeserializeAck/README.md b/cbmc/proofs/MQTT_DeserializeAck/README.md index 9bf14d42..0446710d 100644 --- a/cbmc/proofs/MQTT_DeserializeAck/README.md +++ b/cbmc/proofs/MQTT_DeserializeAck/README.md @@ -5,6 +5,6 @@ This directory contains a memory safety proof for MQTT_DeserializeAck. To run the proof. * Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer - to your path -* Run "make" + to your path. +* Run "make". * Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c b/cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c index 341ce348..bee97511 100644 --- a/cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c +++ b/cbmc/proofs/MQTT_DeserializePublish/MQTT_DeserializePublish_harness.c @@ -29,14 +29,14 @@ void harness() { - MQTTPacketInfo_t * pIncomingPacket = NULL; - MQTTPublishInfo_t * pPublishInfo = NULL; + MQTTPacketInfo_t * pIncomingPacket; + MQTTPublishInfo_t * pPublishInfo; uint16_t packetId; - pIncomingPacket = allocateMqttPacketInfo( pIncomingPacket ); + pIncomingPacket = allocateMqttPacketInfo( NULL ); __CPROVER_assume( isValidMqttPacketInfo( pIncomingPacket ) ); - pPublishInfo = allocateMqttPublishInfo( pPublishInfo ); + pPublishInfo = allocateMqttPublishInfo( NULL ); __CPROVER_assume( isValidMqttPublishInfo( pPublishInfo ) ); /* This function grabs the topic name, the topic name length, the diff --git a/cbmc/proofs/MQTT_DeserializePublish/Makefile b/cbmc/proofs/MQTT_DeserializePublish/Makefile index f2494070..f6b921e4 100644 --- a/cbmc/proofs/MQTT_DeserializePublish/Makefile +++ b/cbmc/proofs/MQTT_DeserializePublish/Makefile @@ -11,7 +11,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(PROOFDIR)/../../sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c include ../Makefile.common diff --git a/cbmc/proofs/MQTT_DeserializePublish/README.md b/cbmc/proofs/MQTT_DeserializePublish/README.md index 624d15ac..f8962309 100644 --- a/cbmc/proofs/MQTT_DeserializePublish/README.md +++ b/cbmc/proofs/MQTT_DeserializePublish/README.md @@ -5,6 +5,6 @@ This directory contains a memory safety proof for MQTT_DeserializePublish. To run the proof. * Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer - to your path -* Run "make" + to your path. +* Run "make". * Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/MQTT_GetIncomingPacketTypeAndLength_harness.c b/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/MQTT_GetIncomingPacketTypeAndLength_harness.c index 75664ba4..138fba49 100644 --- a/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/MQTT_GetIncomingPacketTypeAndLength_harness.c +++ b/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/MQTT_GetIncomingPacketTypeAndLength_harness.c @@ -36,9 +36,9 @@ void harness() /* MQTT_GetIncomingPacketTypeAndLength() will set only the remainingLength * field in the input MQTTPacketInfo_t structure. */ - MQTTPacketInfo_t * pIncomingPacket = NULL; + MQTTPacketInfo_t * pIncomingPacket; - pIncomingPacket = allocateMqttPacketInfo( pIncomingPacket ); + pIncomingPacket = allocateMqttPacketInfo( NULL ); __CPROVER_assume( isValidMqttPacketInfo( pIncomingPacket ) ); MQTT_GetIncomingPacketTypeAndLength( NetworkInterfaceReceiveStub, diff --git a/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/Makefile b/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/Makefile index 0d1e176b..b0b25ade 100644 --- a/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/Makefile +++ b/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/Makefile @@ -7,8 +7,8 @@ REMOVE_FUNCTION_BODY += UNWINDSET += getRemainingLength.0:5 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(PROOFDIR)/../../sources/mqtt_cbmc_state.c -PROOF_SOURCES += $(PROOFDIR)/../../stubs/network_interface_stubs.c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/stubs/network_interface_stubs.c PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c include ../Makefile.common diff --git a/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/README.md b/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/README.md index 42110341..209750fb 100644 --- a/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/README.md +++ b/cbmc/proofs/MQTT_GetIncomingPacketTypeAndLength/README.md @@ -5,6 +5,6 @@ This directory contains a memory safety proof for MQTT_GetIncomingPacketTypeAndL To run the proof. * Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer - to your path -* Run "make" + to your path. +* Run "make". * Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_GetPacketId/Makefile b/cbmc/proofs/MQTT_GetPacketId/Makefile index ad741b3d..c2f2b1ec 100644 --- a/cbmc/proofs/MQTT_GetPacketId/Makefile +++ b/cbmc/proofs/MQTT_GetPacketId/Makefile @@ -8,7 +8,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(PROOFDIR)/../../sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c include ../Makefile.common diff --git a/cbmc/proofs/MQTT_GetPacketId/README.md b/cbmc/proofs/MQTT_GetPacketId/README.md index 036a7051..4fb49643 100644 --- a/cbmc/proofs/MQTT_GetPacketId/README.md +++ b/cbmc/proofs/MQTT_GetPacketId/README.md @@ -5,6 +5,6 @@ This directory contains a memory safety proof for MQTT_GetPacketId. To run the proof. * Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer - to your path -* Run "make" + to your path. +* Run "make". * Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_Init/MQTT_Init_harness.c b/cbmc/proofs/MQTT_Init/MQTT_Init_harness.c index 94bad146..dd7faccd 100644 --- a/cbmc/proofs/MQTT_Init/MQTT_Init_harness.c +++ b/cbmc/proofs/MQTT_Init/MQTT_Init_harness.c @@ -29,10 +29,10 @@ void harness() { - MQTTContext_t * pContext = NULL; - TransportInterface_t * pTransportInterface = NULL; - MQTTApplicationCallbacks_t * pCallbacks = NULL; - MQTTFixedBuffer_t * pNetworkBuffer = NULL; + MQTTContext_t * pContext; + TransportInterface_t * pTransportInterface; + MQTTApplicationCallbacks_t * pCallbacks; + MQTTFixedBuffer_t * pNetworkBuffer; pContext = mallocCanFail( sizeof( MQTTContext_t ) ); pTransportInterface = mallocCanFail( sizeof( MQTTContext_t ) ); diff --git a/cbmc/proofs/MQTT_Init/Makefile b/cbmc/proofs/MQTT_Init/Makefile index 60fe4da0..b987e303 100644 --- a/cbmc/proofs/MQTT_Init/Makefile +++ b/cbmc/proofs/MQTT_Init/Makefile @@ -8,7 +8,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(PROOFDIR)/../../sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt.c include ../Makefile.common diff --git a/cbmc/proofs/MQTT_Init/README.md b/cbmc/proofs/MQTT_Init/README.md index 754f91b5..f0f4cf31 100644 --- a/cbmc/proofs/MQTT_Init/README.md +++ b/cbmc/proofs/MQTT_Init/README.md @@ -5,6 +5,6 @@ This directory contains a memory safety proof for MQTT_Init. To run the proof. * Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer - to your path -* Run "make" + to your path. +* Run "make". * Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_SerializeAck/MQTT_SerializeAck_harness.c b/cbmc/proofs/MQTT_SerializeAck/MQTT_SerializeAck_harness.c new file mode 100644 index 00000000..54bf9e97 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeAck/MQTT_SerializeAck_harness.c @@ -0,0 +1,39 @@ +/* + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +/** + * @file MQTT_SerializeAck_harness.c + * @brief Implements the proof harness for MQTT_SerializeAck function. + */ +#include "mqtt.h" +#include "mqtt_cbmc_state.h" + +void harness() +{ + MQTTFixedBuffer_t * pFixedBuffer; + uint8_t packetType; + uint16_t packetId; + + pFixedBuffer = allocateMqttFixedBuffer( NULL ); + __CPROVER_ASSUME( isValidMqttFixedBuffer( pFixedBuffer ) ); + + MQTT_SerializeAck( pFixedBuffer, packetType, packetId ); +} diff --git a/cbmc/proofs/MQTT_SerializeAck/Makefile b/cbmc/proofs/MQTT_SerializeAck/Makefile new file mode 100644 index 00000000..09385c39 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeAck/Makefile @@ -0,0 +1,17 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY=harness +HARNESS_FILE=MQTT_SerializeAck_harness + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c + +include ../Makefile.common diff --git a/cbmc/proofs/MQTT_SerializeAck/README.md b/cbmc/proofs/MQTT_SerializeAck/README.md new file mode 100644 index 00000000..028c8f2a --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeAck/README.md @@ -0,0 +1,10 @@ +MQTT_SerializeAck proof +============== + +This directory contains a memory safety proof for MQTT_SerializeAck. + +To run the proof. +* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer + to your path. +* Run "make". +* Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_SerializeAck/cbmc-batch.yaml b/cbmc/proofs/MQTT_SerializeAck/cbmc-batch.yaml new file mode 100644 index 00000000..7eeb12ad --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeAck/cbmc-batch.yaml @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# The contents of this file will be generated by continuous integration. diff --git a/cbmc/proofs/MQTT_SerializeAck/cbmc-viewer.json b/cbmc/proofs/MQTT_SerializeAck/cbmc-viewer.json new file mode 100644 index 00000000..a69c3ae7 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeAck/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "MQTT_SerializeAck", + "proof-root": "libraries/standard/mqtt/cbmc/proofs" +} diff --git a/cbmc/proofs/MQTT_SerializeConnect/MQTT_SerializeConnect_harness.c b/cbmc/proofs/MQTT_SerializeConnect/MQTT_SerializeConnect_harness.c index a34b3ea3..56838231 100644 --- a/cbmc/proofs/MQTT_SerializeConnect/MQTT_SerializeConnect_harness.c +++ b/cbmc/proofs/MQTT_SerializeConnect/MQTT_SerializeConnect_harness.c @@ -28,35 +28,43 @@ void harness() { - MQTTConnectInfo_t * pConnectInfo = NULL; - MQTTPublishInfo_t * pWillInfo = NULL; - size_t remainingLength = 0; - MQTTFixedBuffer_t * pBuffer = NULL; - size_t packetSize = 0; + MQTTConnectInfo_t * pConnectInfo; + MQTTPublishInfo_t * pWillInfo; + size_t remainingLength; + MQTTFixedBuffer_t * pFixedBuffer; + size_t packetSize; MQTTStatus_t status = MQTTSuccess; - pConnectInfo = allocateMqttConnectInfo( pConnectInfo ); + pConnectInfo = allocateMqttConnectInfo( NULL ); __CPROVER_assume( isValidMqttConnectInfo( pConnectInfo ) ); - pWillInfo = allocateMqttPublishInfo( pWillInfo ); + pWillInfo = allocateMqttPublishInfo( NULL ); __CPROVER_assume( isValidMqttPublishInfo( pWillInfo ) ); - pBuffer = allocateMqttFixedBuffer( pBuffer ); - __CPROVER_assume( isValidMqttFixedBuffer( pBuffer ) ); + pFixedBuffer = allocateMqttFixedBuffer( NULL ); + __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) ); /* Before calling MQTT_SerializeConnect() it is up to the application to make - * sure that the information in MQTTConnectInfo_t and MQTTPublishInfo_t can - * fit into the MQTTFixedBuffer_t. It is a violation of the API to call - * MQTT_SerializeConnect without first calling MQTT_GetConnectPacketSize(). */ + * sure that the information in MQTTConnectInfo_t and MQTTPublishInfo_t can + * fit into the MQTTFixedBuffer_t. It is a violation of the API to call + * MQTT_SerializeConnect() without first calling MQTT_GetConnectPacketSize(). */ if( pConnectInfo != NULL ) { - status = MQTT_GetConnectPacketSize( pConnectInfo, pWillInfo, &remainingLength, &packetSize ); + /* The output parameter pPacketSize of the function MQTT_GetConnectPacketSize() + * must not be NULL. packetSize returned is not used in this proof, but + * is used normally by the application to verify the size of their + * MQTTFixedBuffer_t. MQTT_SerializeConnect() will use the remainingLength + * to recalculate the packetSize. */ + status = MQTT_GetConnectPacketSize( pConnectInfo, + pWillInfo, + &remainingLength, + &packetSize ); } if( status == MQTTSuccess ) { /* For coverage, it is expected that a NULL pConnectInfo will reach this * function. */ - MQTT_SerializeConnect( pConnectInfo, pWillInfo, remainingLength, pBuffer ); + MQTT_SerializeConnect( pConnectInfo, pWillInfo, remainingLength, pFixedBuffer ); } } diff --git a/cbmc/proofs/MQTT_SerializeConnect/Makefile b/cbmc/proofs/MQTT_SerializeConnect/Makefile index 931f40fa..6ffa0339 100644 --- a/cbmc/proofs/MQTT_SerializeConnect/Makefile +++ b/cbmc/proofs/MQTT_SerializeConnect/Makefile @@ -11,7 +11,7 @@ REMOVE_FUNCTION_BODY += UNWINDSET += encodeRemainingLength.0:3 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROOF_SOURCES += $(PROOFDIR)/../../sources/mqtt_cbmc_state.c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c include ../Makefile.common diff --git a/cbmc/proofs/MQTT_SerializeConnect/README.md b/cbmc/proofs/MQTT_SerializeConnect/README.md index 7536a0ea..f2be3428 100644 --- a/cbmc/proofs/MQTT_SerializeConnect/README.md +++ b/cbmc/proofs/MQTT_SerializeConnect/README.md @@ -5,6 +5,6 @@ This directory contains a memory safety proof for MQTT_SerializeConnect. To run the proof. * Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer - to your path -* Run "make" + to your path. +* Run "make". * Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_SerializeDisconnect/MQTT_SerializeDisconnect_harness.c b/cbmc/proofs/MQTT_SerializeDisconnect/MQTT_SerializeDisconnect_harness.c new file mode 100644 index 00000000..595b9b47 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeDisconnect/MQTT_SerializeDisconnect_harness.c @@ -0,0 +1,37 @@ +/* + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +/** + * @file MQTT_SerializeDisconnect_harness.c + * @brief Implements the proof harness for MQTT_SerializeDisconnect function. + */ +#include "mqtt.h" +#include "mqtt_cbmc_state.h" + +void harness() +{ + MQTTFixedBuffer_t * pFixedBuffer; + + pFixedBuffer = allocateMqttFixedBuffer( NULL ); + __CPROVER_ASSUME( isValidMqttFixedBuffer( pFixedBuffer ) ); + + MQTT_SerializeDisconnect( pFixedBuffer ); +} diff --git a/cbmc/proofs/MQTT_SerializeDisconnect/Makefile b/cbmc/proofs/MQTT_SerializeDisconnect/Makefile new file mode 100644 index 00000000..6e3e8dc6 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeDisconnect/Makefile @@ -0,0 +1,17 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY=harness +HARNESS_FILE=MQTT_SerializeDisconnect_harness + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c + +include ../Makefile.common diff --git a/cbmc/proofs/MQTT_SerializeDisconnect/README.md b/cbmc/proofs/MQTT_SerializeDisconnect/README.md new file mode 100644 index 00000000..3de68214 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeDisconnect/README.md @@ -0,0 +1,10 @@ +MQTT_SerializeDisconnect proof +============== + +This directory contains a memory safety proof for MQTT_SerializeDisconnect. + +To run the proof. +* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer + to your path. +* Run "make". +* Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_SerializeDisconnect/cbmc-batch.yaml b/cbmc/proofs/MQTT_SerializeDisconnect/cbmc-batch.yaml new file mode 100644 index 00000000..7eeb12ad --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeDisconnect/cbmc-batch.yaml @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# The contents of this file will be generated by continuous integration. diff --git a/cbmc/proofs/MQTT_SerializeDisconnect/cbmc-viewer.json b/cbmc/proofs/MQTT_SerializeDisconnect/cbmc-viewer.json new file mode 100644 index 00000000..858f3ae8 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeDisconnect/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "MQTT_SerializeDisconnect", + "proof-root": "libraries/standard/mqtt/cbmc/proofs" +} diff --git a/cbmc/proofs/MQTT_SerializePingreq/MQTT_SerializePingreq_harness.c b/cbmc/proofs/MQTT_SerializePingreq/MQTT_SerializePingreq_harness.c new file mode 100644 index 00000000..38bc2885 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePingreq/MQTT_SerializePingreq_harness.c @@ -0,0 +1,37 @@ +/* + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +/** + * @file MQTT_SerializePingreq_harness.c + * @brief Implements the proof harness for MQTT_SerializePingreq function. + */ +#include "mqtt.h" +#include "mqtt_cbmc_state.h" + +void harness() +{ + MQTTFixedBuffer_t * pFixedBuffer; + + pFixedBuffer = allocateMqttFixedBuffer( NULL ); + __CPROVER_ASSUME( isValidMqttFixedBuffer( pFixedBuffer ) ); + + MQTT_SerializePingreq( pFixedBuffer ); +} diff --git a/cbmc/proofs/MQTT_SerializePingreq/Makefile b/cbmc/proofs/MQTT_SerializePingreq/Makefile new file mode 100644 index 00000000..75460383 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePingreq/Makefile @@ -0,0 +1,17 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY=harness +HARNESS_FILE=MQTT_SerializePingreq_harness + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c + +include ../Makefile.common diff --git a/cbmc/proofs/MQTT_SerializePingreq/README.md b/cbmc/proofs/MQTT_SerializePingreq/README.md new file mode 100644 index 00000000..5723a640 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePingreq/README.md @@ -0,0 +1,10 @@ +MQTT_SerializePingreq proof +============== + +This directory contains a memory safety proof for MQTT_SerializePingreq. + +To run the proof. +* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer + to your path. +* Run "make". +* Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_SerializePingreq/cbmc-batch.yaml b/cbmc/proofs/MQTT_SerializePingreq/cbmc-batch.yaml new file mode 100644 index 00000000..7eeb12ad --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePingreq/cbmc-batch.yaml @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# The contents of this file will be generated by continuous integration. diff --git a/cbmc/proofs/MQTT_SerializePingreq/cbmc-viewer.json b/cbmc/proofs/MQTT_SerializePingreq/cbmc-viewer.json new file mode 100644 index 00000000..4e487fbe --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePingreq/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "MQTT_SerializePingreq", + "proof-root": "libraries/standard/mqtt/cbmc/proofs" +} diff --git a/cbmc/proofs/MQTT_SerializePublish/MQTT_SerializePublish_harness.c b/cbmc/proofs/MQTT_SerializePublish/MQTT_SerializePublish_harness.c new file mode 100644 index 00000000..0c892a00 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePublish/MQTT_SerializePublish_harness.c @@ -0,0 +1,67 @@ +/* + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +/** + * @file MQTT_SerializePublish_harness.c + * @brief Implements the proof harness for MQTT_SerializePublish function. + */ +#include "mqtt.h" +#include "mqtt_cbmc_state.h" + +void harness() +{ + MQTTPublishInfo_t * pPublishInfo; + uint16_t packetId; + size_t remainingLength; + size_t packetSize; + const MQTTFixedBuffer_t * pFixedBuffer; + MQTTStatus_t status = MQTTSuccess; + + pPublishInfo = allocateMqttPublishInfo( NULL ); + __CPROVER_assume( isValidMqttPublishInfo( pPublishInfo ) ); + + pFixedBuffer = allocateMqttFixedBuffer( NULL ); + __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) ); + + /* Before calling MQTT_SerializePublish() it is up to the application to + * make sure that the information in MQTTPublishInfo_t can fit into the + * MQTTFixedBuffer_t. It is a violation of the API to call + * MQTT_SerializePublish() without first calling MQTT_GetPublishPacketSize(). */ + if( pPublishInfo != NULL ) + { + /* The output parameter pPacketSize of the function MQTT_GetConnectPacketSize() + * must not be NULL. packetSize returned is not used in this proof, but + * is used normally by the application to verify the size of their + * MQTTFixedBuffer_t. MQTT_SerializeConnect() will use the remainingLength + * to recalculate the packetSize. */ + status = MQTT_GetPublishPacketSize( pPublishInfo, &remainingLength, &packetSize ); + } + + if( status == MQTTSuccess ) + { + /* For coverage it is expected that a NULL pPublishInfo could + * reach this function. */ + MQTT_SerializePublish( pPublishInfo, + packetId, + remainingLength, + pFixedBuffer ); + } +} diff --git a/cbmc/proofs/MQTT_SerializePublish/Makefile b/cbmc/proofs/MQTT_SerializePublish/Makefile new file mode 100644 index 00000000..f628a733 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePublish/Makefile @@ -0,0 +1,17 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY=harness +HARNESS_FILE=MQTT_SerializePublish_harness + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += encodeRemainingLength.0:4 + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c + +include ../Makefile.common diff --git a/cbmc/proofs/MQTT_SerializePublish/README.md b/cbmc/proofs/MQTT_SerializePublish/README.md new file mode 100644 index 00000000..019e9331 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePublish/README.md @@ -0,0 +1,10 @@ +MQTT_SerializePublish proof +============== + +This directory contains a memory safety proof for MQTT_SerializePublish. + +To run the proof. +* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer + to your path. +* Run "make". +* Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_SerializePublish/cbmc-batch.yaml b/cbmc/proofs/MQTT_SerializePublish/cbmc-batch.yaml new file mode 100644 index 00000000..7eeb12ad --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePublish/cbmc-batch.yaml @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# The contents of this file will be generated by continuous integration. diff --git a/cbmc/proofs/MQTT_SerializePublish/cbmc-viewer.json b/cbmc/proofs/MQTT_SerializePublish/cbmc-viewer.json new file mode 100644 index 00000000..f6464b32 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePublish/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "MQTT_SerializePublish", + "proof-root": "libraries/standard/mqtt/cbmc/proofs" +} diff --git a/cbmc/proofs/MQTT_SerializePublishHeader/MQTT_SerializePublishHeader_harness.c b/cbmc/proofs/MQTT_SerializePublishHeader/MQTT_SerializePublishHeader_harness.c new file mode 100644 index 00000000..32f10912 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePublishHeader/MQTT_SerializePublishHeader_harness.c @@ -0,0 +1,75 @@ +/* + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +/** + * @file MQTT_SerializePublishHeader_harness.c + * @brief Implements the proof harness for MQTT_SerializePublishHeader function. + */ +#include "mqtt.h" +#include "mqtt_cbmc_state.h" + +void harness() +{ + MQTTPublishInfo_t * pPublishInfo; + uint16_t packetId; + size_t remainingLength; + size_t packetSize; + MQTTFixedBuffer_t * pFixedBuffer; + size_t * pHeaderSize; + MQTTStatus_t status = MQTTSuccess; + + pPublishInfo = allocateMqttPublishInfo( NULL ); + __CPROVER_assume( isValidMqttPublishInfo( pPublishInfo ) ); + + pFixedBuffer = allocateMqttFixedBuffer( NULL ); + __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) ); + + /* Allocate space for a returned header size to get coverage of a possibly + * NULL input. */ + pHeaderSize = mallocCanFail( sizeof( size_t ) ); + + /* Before calling MQTT_SerializePublishHeader() it is up to the application + * to verify that the information in MQTTPublishInfo_t can fit into the + * MQTTFixedBuffer_t. It is a violation of the API to call + * MQTT_SerializePublishHeader() without first calling MQTT_GetPublishPacketSize(). */ + if( pPublishInfo != NULL ) + { + /* The output parameter pPacketSize of the function MQTT_GetConnectPacketSize() + * must not be NULL. packetSize returned is not used in this proof, but + * is used normally by the application to verify the size of their + * MQTTFixedBuffer_t. MQTT_SerializeConnect() will use the remainingLength + * to recalculate the packetSize. */ + status = MQTT_GetPublishPacketSize( pPublishInfo, + &remainingLength, + &packetSize ); + } + + if( status == MQTTSuccess ) + { + /* For coverage it is expected that a NULL pPublishInfo could + * reach this function. */ + MQTT_SerializePublishHeader( pPublishInfo, + packetId, + remainingLength, + pFixedBuffer, + pHeaderSize ); + } +} diff --git a/cbmc/proofs/MQTT_SerializePublishHeader/Makefile b/cbmc/proofs/MQTT_SerializePublishHeader/Makefile new file mode 100644 index 00000000..1c666d2d --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePublishHeader/Makefile @@ -0,0 +1,17 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY=harness +HARNESS_FILE=MQTT_SerializePublishHeader_harness + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += encodeRemainingLength.0:4 + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c + +include ../Makefile.common diff --git a/cbmc/proofs/MQTT_SerializePublishHeader/README.md b/cbmc/proofs/MQTT_SerializePublishHeader/README.md new file mode 100644 index 00000000..543ecb93 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePublishHeader/README.md @@ -0,0 +1,10 @@ +MQTT_SerializePublishHeader proof +============== + +This directory contains a memory safety proof for MQTT_SerializePublishHeader. + +To run the proof. +* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer + to your path. +* Run "make". +* Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_SerializePublishHeader/cbmc-batch.yaml b/cbmc/proofs/MQTT_SerializePublishHeader/cbmc-batch.yaml new file mode 100644 index 00000000..7eeb12ad --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePublishHeader/cbmc-batch.yaml @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# The contents of this file will be generated by continuous integration. diff --git a/cbmc/proofs/MQTT_SerializePublishHeader/cbmc-viewer.json b/cbmc/proofs/MQTT_SerializePublishHeader/cbmc-viewer.json new file mode 100644 index 00000000..1ddfd34e --- /dev/null +++ b/cbmc/proofs/MQTT_SerializePublishHeader/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "MQTT_SerializePublishHeader", + "proof-root": "libraries/standard/mqtt/cbmc/proofs" +} diff --git a/cbmc/proofs/MQTT_SerializeSubscribe/MQTT_SerializeSubscribe_harness.c b/cbmc/proofs/MQTT_SerializeSubscribe/MQTT_SerializeSubscribe_harness.c new file mode 100644 index 00000000..c9871bbe --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeSubscribe/MQTT_SerializeSubscribe_harness.c @@ -0,0 +1,74 @@ +/* + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +/** + * @file MQTT_SerializeSubscribe_harness.c + * @brief Implements the proof harness for MQTT_SerializeSubscribe function. + */ +#include "mqtt.h" +#include "mqtt_cbmc_state.h" + +void harness() +{ + MQTTSubscribeInfo_t * pSubscriptionList; + size_t subscriptionCount; + size_t remainingLength; + uint16_t packetId; + size_t packetSize; + MQTTFixedBuffer_t * pFixedBuffer; + MQTTStatus_t status = MQTTSuccess; + + __CPROVER_assume( subscriptionCount < SUBSCRIPTION_COUNT_MAX ); + + pSubscriptionList = allocateMqttSubscriptionList( NULL, subscriptionCount ); + __CPROVER_assume( isValidMqttSubscriptionList( pSubscriptionList, subscriptionCount ) ); + + pFixedBuffer = allocateMqttFixedBuffer( NULL ); + __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) ); + + /* Before calling MQTT_SerializeSubscribe() it is up to the application to + * make sure that the information in the list of MQTTSubscribeInfo_t can fit + * into the MQTTFixedBuffer_t. It is a violation of the API to call + * MQTT_SerializeSubscribe() without first calling MQTT_GetSubscribePacketSize(). */ + if( pSubscriptionList != NULL ) + { + /* The output parameter pPacketSize of the function MQTT_GetConnectPacketSize() + * must not be NULL. packetSize returned is not used in this proof, but + * is used normally by the application to verify the size of their + * MQTTFixedBuffer_t. MQTT_SerializeConnect() will use the remainingLength + * to recalculate the packetSize. */ + status = MQTT_GetSubscribePacketSize( pSubscriptionList, + subscriptionCount, + &remainingLength, + &packetSize ); + } + + if( status == MQTTSuccess ) + { + /* For coverage it is expected that a NULL pSubscriptionList could + * reach this function. */ + MQTT_SerializeSubscribe( pSubscriptionList, + subscriptionCount, + packetId, + remainingLength, + pFixedBuffer ); + } +} diff --git a/cbmc/proofs/MQTT_SerializeSubscribe/Makefile b/cbmc/proofs/MQTT_SerializeSubscribe/Makefile new file mode 100644 index 00000000..2ace4294 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeSubscribe/Makefile @@ -0,0 +1,25 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY=harness +HARNESS_FILE=MQTT_SerializeSubscribe_harness + +# Bind the subscription count. Please see the default value in mqtt_cbmc_state.c +# for more information on this bound. This is set to 2 currently to have the proof +# run quickly. +SUBSCRIPTION_COUNT_MAX=2 +DEFINES += -DSUBSCRIPTION_COUNT_MAX=$(SUBSCRIPTION_COUNT_MAX) +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += allocateMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX) +UNWINDSET += isValidMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX) +UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX) +UNWINDSET += MQTT_SerializeSubscribe.0:$(SUBSCRIPTION_COUNT_MAX) +UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:4 + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c + +include ../Makefile.common diff --git a/cbmc/proofs/MQTT_SerializeSubscribe/README.md b/cbmc/proofs/MQTT_SerializeSubscribe/README.md new file mode 100644 index 00000000..5ea33603 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeSubscribe/README.md @@ -0,0 +1,10 @@ +MQTT_SerializeSubscribe proof +============== + +This directory contains a memory safety proof for MQTT_SerializeSubscribe. + +To run the proof. +* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer + to your path. +* Run "make". +* Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_SerializeSubscribe/cbmc-batch.yaml b/cbmc/proofs/MQTT_SerializeSubscribe/cbmc-batch.yaml new file mode 100644 index 00000000..7eeb12ad --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeSubscribe/cbmc-batch.yaml @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# The contents of this file will be generated by continuous integration. diff --git a/cbmc/proofs/MQTT_SerializeSubscribe/cbmc-viewer.json b/cbmc/proofs/MQTT_SerializeSubscribe/cbmc-viewer.json new file mode 100644 index 00000000..5b0c51c4 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeSubscribe/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "MQTT_SerializeSubscribe", + "proof-root": "libraries/standard/mqtt/cbmc/proofs" +} diff --git a/cbmc/proofs/MQTT_SerializeUnsubscribe/MQTT_SerializeUnsubscribe_harness.c b/cbmc/proofs/MQTT_SerializeUnsubscribe/MQTT_SerializeUnsubscribe_harness.c new file mode 100644 index 00000000..63f7fecd --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeUnsubscribe/MQTT_SerializeUnsubscribe_harness.c @@ -0,0 +1,77 @@ +/* + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +/** + * @file MQTT_SerializeUnsubscribe_harness.c + * @brief Implements the proof harness for MQTT_SerializeUnsubscribe function. + */ +#include "mqtt.h" +#include "mqtt_cbmc_state.h" + +void harness() +{ + MQTTSubscribeInfo_t * pSubscriptionList; + size_t subscriptionCount; + size_t remainingLength; + uint16_t packetId; + + /* This variable is not used but is needed for MQTT_GetUnsubscribePacketSize() + * to verify the pSubscriptionList. */ + size_t packetSize; + MQTTFixedBuffer_t * pFixedBuffer; + MQTTStatus_t status = MQTTSuccess; + + __CPROVER_assume( subscriptionCount < SUBSCRIPTION_COUNT_MAX ); + + pSubscriptionList = allocateMqttSubscriptionList( NULL, subscriptionCount ); + __CPROVER_assume( isValidMqttSubscriptionList( pSubscriptionList, subscriptionCount ) ); + + pFixedBuffer = allocateMqttFixedBuffer( NULL ); + __CPROVER_assume( isValidMqttFixedBuffer( pFixedBuffer ) ); + + /* Before calling MQTT_SerializeUnsubscribe() it is up to the application to + * make sure that the information in the list of MQTTSubscribeInfo_t can fit + * into the MQTTFixedBuffer_t. It is a violation of the API to call + * MQTT_SerializeUnsubscribe() without first calling MQTT_GetUnsubscribePacketSize(). */ + if( pSubscriptionList != NULL ) + { + /* The output parameter pPacketSize of the function MQTT_GetConnectPacketSize() + * must not be NULL. packetSize returned is not used in this proof, but + * is used normally by the application to verify the size of their + * MQTTFixedBuffer_t. MQTT_SerializeConnect() will use the remainingLength + * to recalculate the packetSize. */ + status = MQTT_GetUnsubscribePacketSize( pSubscriptionList, + subscriptionCount, + &remainingLength, + &packetSize ); + } + + if( status == MQTTSuccess ) + { + /* For coverage it is expected that a NULL pSubscriptionList could + * reach this function. */ + MQTT_SerializeUnsubscribe( pSubscriptionList, + subscriptionCount, + packetId, + remainingLength, + pFixedBuffer ); + } +} diff --git a/cbmc/proofs/MQTT_SerializeUnsubscribe/Makefile b/cbmc/proofs/MQTT_SerializeUnsubscribe/Makefile new file mode 100644 index 00000000..2017873c --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeUnsubscribe/Makefile @@ -0,0 +1,25 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY=harness +HARNESS_FILE=MQTT_SerializeUnsubscribe_harness + +# Bind the subscription count. Please see the default value in mqtt_cbmc_state.c +# for more information on this bound. This is set to 2 currently to have the proof +# run quickly. +SUBSCRIPTION_COUNT_MAX=2 +DEFINES += -DSUBSCRIPTION_COUNT_MAX=$(SUBSCRIPTION_COUNT_MAX) +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += allocateMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX) +UNWINDSET += isValidMqttSubscriptionList.0:$(SUBSCRIPTION_COUNT_MAX) +UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_calculateSubscriptionPacketSize.0:$(SUBSCRIPTION_COUNT_MAX) +UNWINDSET += MQTT_SerializeUnsubscribe.0:$(SUBSCRIPTION_COUNT_MAX) +UNWINDSET += __CPROVER_file_local_mqtt_lightweight_c_encodeRemainingLength.0:4 + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROOF_SOURCES += $(SRCDIR)/libraries/standard/mqtt/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/libraries/standard/mqtt/src/mqtt_lightweight.c + +include ../Makefile.common diff --git a/cbmc/proofs/MQTT_SerializeUnsubscribe/README.md b/cbmc/proofs/MQTT_SerializeUnsubscribe/README.md new file mode 100644 index 00000000..30b6af43 --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeUnsubscribe/README.md @@ -0,0 +1,10 @@ +MQTT_SerializeUnsubscribe proof +============== + +This directory contains a memory safety proof for MQTT_SerializeUnsubscribe. + +To run the proof. +* Add cbmc, goto-cc, goto-instrument, goto-analyzer, and cbmc-viewer + to your path. +* Run "make". +* Open html/index.html in a web browser. diff --git a/cbmc/proofs/MQTT_SerializeUnsubscribe/cbmc-batch.yaml b/cbmc/proofs/MQTT_SerializeUnsubscribe/cbmc-batch.yaml new file mode 100644 index 00000000..7eeb12ad --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeUnsubscribe/cbmc-batch.yaml @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# The contents of this file will be generated by continuous integration. diff --git a/cbmc/proofs/MQTT_SerializeUnsubscribe/cbmc-viewer.json b/cbmc/proofs/MQTT_SerializeUnsubscribe/cbmc-viewer.json new file mode 100644 index 00000000..166638dc --- /dev/null +++ b/cbmc/proofs/MQTT_SerializeUnsubscribe/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "MQTT_SerializeUnsubscribe", + "proof-root": "libraries/standard/mqtt/cbmc/proofs" +} diff --git a/cbmc/sources/mqtt_cbmc_state.c b/cbmc/sources/mqtt_cbmc_state.c index 37e0f6c7..d794b9fa 100644 --- a/cbmc/sources/mqtt_cbmc_state.c +++ b/cbmc/sources/mqtt_cbmc_state.c @@ -22,6 +22,15 @@ #include #include "mqtt_cbmc_state.h" +/* A default bound on the subscription count. Iterating over possibly SIZE_MAX + * number of subscriptions does not add any value to the proofs. An application + * can allocate memory for as many subscriptions as their system can handle. + * The proofs verify that the code can handle the maximum topicFilterLength in + * each subscription. */ +#ifndef SUBSCRIPTION_COUNT_MAX + #define SUBSCRIPTION_COUNT_MAX 1U +#endif + void * mallocCanFail( size_t size ) { __CPROVER_assert( size < CBMC_MAX_OBJECT_SIZE, "mallocCanFail size is too big" ); @@ -126,29 +135,66 @@ bool isValidMqttConnectInfo( const MQTTConnectInfo_t * pConnectInfo ) return isValid; } -MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pBuffer ) +MQTTFixedBuffer_t * allocateMqttFixedBuffer( MQTTFixedBuffer_t * pFixedBuffer ) { - if( pBuffer == NULL ) + if( pFixedBuffer == NULL ) { - pBuffer = mallocCanFail( sizeof( MQTTFixedBuffer_t ) ); + pFixedBuffer = mallocCanFail( sizeof( MQTTFixedBuffer_t ) ); } - if( pBuffer != NULL ) + if( pFixedBuffer != NULL ) { - __CPROVER_assume( pBuffer->size < CBMC_MAX_OBJECT_SIZE ); - pBuffer->pBuffer = mallocCanFail( pBuffer->size ); + __CPROVER_assume( pFixedBuffer->size < CBMC_MAX_OBJECT_SIZE ); + pFixedBuffer->pBuffer = mallocCanFail( pFixedBuffer->size ); } - return pBuffer; + return pFixedBuffer; } -bool isValidMqttFixedBuffer( const MQTTFixedBuffer_t * pBuffer ) +bool isValidMqttFixedBuffer( const MQTTFixedBuffer_t * pFixedBuffer ) { bool isValid = true; - if( pBuffer != NULL ) + if( pFixedBuffer != NULL ) { - isValid = pBuffer->size < CBMC_MAX_OBJECT_SIZE; + isValid = pFixedBuffer->size < CBMC_MAX_OBJECT_SIZE; + } + + return isValid; +} + +MQTTSubscribeInfo_t * allocateMqttSubscriptionList( MQTTSubscribeInfo_t * pSubscriptionList, + size_t subscriptionCount ) +{ + if( pSubscriptionList == NULL ) + { + __CPROVER_assume( sizeof( MQTTSubscribeInfo_t ) * subscriptionCount < CBMC_MAX_OBJECT_SIZE ); + pSubscriptionList = mallocCanFail( sizeof( MQTTSubscribeInfo_t ) * subscriptionCount ); + } + + if( pSubscriptionList != NULL ) + { + for( int i = 0; i < subscriptionCount; i++ ) + { + __CPROVER_assume( pSubscriptionList[ i ].topicFilterLength < CBMC_MAX_OBJECT_SIZE ); + pSubscriptionList[ i ].pTopicFilter = mallocCanFail( pSubscriptionList[ i ].topicFilterLength ); + } + } + + return pSubscriptionList; +} + +bool isValidMqttSubscriptionList( MQTTSubscribeInfo_t * pSubscriptionList, + size_t subscriptionCount ) +{ + bool isValid = true; + + if( pSubscriptionList != NULL ) + { + for( int i = 0; i < subscriptionCount; i++ ) + { + isValid = isValid && ( pSubscriptionList[ i ].topicFilterLength < CBMC_MAX_OBJECT_SIZE ); + } } return isValid;