diff --git a/source/include/core_mqtt.h b/source/include/core_mqtt.h index 8eef1cdc6..c4f2357dd 100644 --- a/source/include/core_mqtt.h +++ b/source/include/core_mqtt.h @@ -1228,7 +1228,7 @@ const char * MQTT_Status_strerror( MQTTStatus_t status ); /** * @brief Get the bytes in a #MQTTVec pointer which can store the whole array as a an MQTT packet when calling MQTT_SerializeMQTTVec( void * pAllocatedMem, MQTTVec_t *pVec ) function. * - * @param[in] pVec The #MQTTVec pointer. + * @param[in] pVec The #MQTTVec pointer given as input to the user defined #MQTTStorePacketForRetransmit callback function. Must not be NULL. * * @return The bytes in the provided #MQTTVec array which can then be used to set aside memory to be used with MQTT_SerializeMQTTVec( void * pAllocatedMem, MQTTVec_t *pVec ) function. */ @@ -1239,8 +1239,8 @@ size_t MQTT_GetBytesInMQTTVec( const MQTTVec_t * pVec ); /** * @brief Serialize the bytes in an array of #MQTTVec in the provided \p pAllocatedMem * - * @param[in] pAllocatedMem Memory in which to serialize the data in the #MQTTVec array. It must be of size provided by MQTT_GetBytesInMQTTVec( MQTTVec_t *pVec ). - * @param[in] pVec The #MQTTVec pointer. + * @param[in] pAllocatedMem Memory in which to serialize the data in the #MQTTVec array. It must be of size provided by MQTT_GetBytesInMQTTVec( MQTTVec_t *pVec ). Should not be NULL. + * @param[in] pVec The #MQTTVec pointer given as input to the user defined #MQTTStorePacketForRetransmit callback function. Must not be NULL. */ /* @[declare_mqtt_serializemqttvec] */ void MQTT_SerializeMQTTVec( uint8_t * pAllocatedMem, diff --git a/test/cbmc/include/mqtt_cbmc_state.h b/test/cbmc/include/mqtt_cbmc_state.h index 741fa4ee3..2929ca7e5 100644 --- a/test/cbmc/include/mqtt_cbmc_state.h +++ b/test/cbmc/include/mqtt_cbmc_state.h @@ -165,4 +165,13 @@ MQTTContext_t * allocateMqttContext( MQTTContext_t * pContext ); */ bool isValidMqttContext( const MQTTContext_t * pContext ); +/** + * @brief Allocate a #MQTTVec_t object. + * + * @param[in] mqttVec #MQTTVec_t object information. + * + * @return NULL or allocated #MQTTContext_t memory. + */ +MQTTVec_t * allocateMqttVec( MQTTVec_t * mqttVec ); + #endif /* ifndef MQTT_CBMC_STATE_H_ */ diff --git a/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/MQTT_GetBytesInMQTTVec_harness.c b/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/MQTT_GetBytesInMQTTVec_harness.c new file mode 100644 index 000000000..08d3203aa --- /dev/null +++ b/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/MQTT_GetBytesInMQTTVec_harness.c @@ -0,0 +1,40 @@ +/* + * coreMQTT + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * SPDX-License-Identifier: MIT + * + * 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_Disconnect_harness.c + * @brief Implements the proof harness for MQTT_Disconnect function. + */ +#include "core_mqtt.h" +#include "mqtt_cbmc_state.h" + +void harness() +{ + MQTTVec_t * mqttVec; + size_t memoryRequired; + + mqttVec = allocateMqttVec( NULL ); + + memoryRequired = MQTT_GetBytesInMQTTVec( mqttVec ); +} diff --git a/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/Makefile b/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/Makefile new file mode 100644 index 000000000..8b9a67dcc --- /dev/null +++ b/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/Makefile @@ -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. +# + +HARNESS_ENTRY=harness +HARNESS_FILE=MQTT_GetBytesInMQTTVec_harness +PROOF_UID=MQTT_GetBytesInMQTTVec + +PUBLISH_PACKET_VECTORS = 5 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += MQTT_GetBytesInMQTTVec.0:${PUBLISH_PACKET_VECTORS} +UNWINDSET += allocateMqttVec.0:${PUBLISH_PACKET_VECTORS} + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c + +include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/README.md b/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/README.md new file mode 100644 index 000000000..57dbc109b --- /dev/null +++ b/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/README.md @@ -0,0 +1,10 @@ +MQTT_GetBytesInMQTTVec proof +============== + +This directory contains a memory safety proof for MQTT_GetBytesInMQTTVec. + +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/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/cbmc-proof.txt b/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/cbmc-proof.txt new file mode 100644 index 000000000..6ed46f125 --- /dev/null +++ b/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/cbmc-viewer.json b/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/cbmc-viewer.json new file mode 100644 index 000000000..aa8ea504b --- /dev/null +++ b/test/cbmc/proofs/MQTT_GetBytesInMQTTVec/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "MQTT_GetBytesInMQTTVec", + "proof-root": "test/cbmc/proofs" +} diff --git a/test/cbmc/proofs/MQTT_SerializeMQTTVec/MQTT_SerializeMQTTVec_harness.c b/test/cbmc/proofs/MQTT_SerializeMQTTVec/MQTT_SerializeMQTTVec_harness.c new file mode 100644 index 000000000..2d283cbbd --- /dev/null +++ b/test/cbmc/proofs/MQTT_SerializeMQTTVec/MQTT_SerializeMQTTVec_harness.c @@ -0,0 +1,52 @@ +/* + * coreMQTT + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * SPDX-License-Identifier: MIT + * + * 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_Disconnect_harness.c + * @brief Implements the proof harness for MQTT_Disconnect function. + */ +#include "core_mqtt.h" +#include "mqtt_cbmc_state.h" + +void harness() +{ + MQTTVec_t * mqttVec; + size_t memoryRequired; + uint8_t * memoryBuffer; + + mqttVec = allocateMqttVec( NULL ); + + memoryRequired = MQTT_GetBytesInMQTTVec( mqttVec ); + + /* It is a part of the API contract that #MQTT_SerializeMQTTVec will be called with + * a memory buffer of size output by #MQTT_GetBytesInMQTTVec function and the + * #MQTTVec_t pointer given by the library as an input to the user defined + * #MQTTStorePacketForRetransmit callback function. Hence the memory buffer must + * not be NULL. + */ + memoryBuffer = malloc( memoryRequired ); + __CPROVER_assume( memoryBuffer != NULL ); + + MQTT_SerializeMQTTVec( memoryBuffer, mqttVec ); +} diff --git a/test/cbmc/proofs/MQTT_SerializeMQTTVec/Makefile b/test/cbmc/proofs/MQTT_SerializeMQTTVec/Makefile new file mode 100644 index 000000000..c90240bc9 --- /dev/null +++ b/test/cbmc/proofs/MQTT_SerializeMQTTVec/Makefile @@ -0,0 +1,40 @@ +# +# 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. +# + +HARNESS_ENTRY=harness +HARNESS_FILE=MQTT_SerializeMQTTVec_harness +PROOF_UID=MQTT_SerializeMQTTVec + +PUBLISH_PACKET_VECTORS = 5 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += MQTT_GetBytesInMQTTVec.0:${PUBLISH_PACKET_VECTORS} +UNWINDSET += allocateMqttVec.0:${PUBLISH_PACKET_VECTORS} +UNWINDSET += MQTT_SerializeMQTTVec.0:${PUBLISH_PACKET_VECTORS} + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_cbmc_state.c +PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt.c + +include ../Makefile.common diff --git a/test/cbmc/proofs/MQTT_SerializeMQTTVec/README.md b/test/cbmc/proofs/MQTT_SerializeMQTTVec/README.md new file mode 100644 index 000000000..f6b06b8e3 --- /dev/null +++ b/test/cbmc/proofs/MQTT_SerializeMQTTVec/README.md @@ -0,0 +1,10 @@ +MQTT_SerializeMQTTVec proof +============== + +This directory contains a memory safety proof for MQTT_SerializeMQTTVec. + +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/test/cbmc/proofs/MQTT_SerializeMQTTVec/cbmc-proof.txt b/test/cbmc/proofs/MQTT_SerializeMQTTVec/cbmc-proof.txt new file mode 100644 index 000000000..6ed46f125 --- /dev/null +++ b/test/cbmc/proofs/MQTT_SerializeMQTTVec/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/MQTT_SerializeMQTTVec/cbmc-viewer.json b/test/cbmc/proofs/MQTT_SerializeMQTTVec/cbmc-viewer.json new file mode 100644 index 000000000..252b61bef --- /dev/null +++ b/test/cbmc/proofs/MQTT_SerializeMQTTVec/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "MQTT_SerializeMQTTVec", + "proof-root": "test/cbmc/proofs" +} diff --git a/test/cbmc/sources/mqtt_cbmc_state.c b/test/cbmc/sources/mqtt_cbmc_state.c index 5022642f8..76a0019c2 100644 --- a/test/cbmc/sources/mqtt_cbmc_state.c +++ b/test/cbmc/sources/mqtt_cbmc_state.c @@ -67,7 +67,27 @@ * @note This definition must exist in order to compile. 10U is a typical value * used in the MQTT demos. */ -#define MAX_UNACKED_PACKETS ( 20U ) +#define MAX_UNACKED_PACKETS ( 20U ) + +/** + * @brief Gives the maximum number of transport vectors required to encode + * a publish packet to send over the network interface. + */ +#define PUBLISH_PACKET_VECTORS ( 4U ) + +/** + * @brief Definition of the MQTTVec_t struct that is used to pass the outgoing + * publish packet content to the user callback function to store the packet for + * retransmission purposes + * + * @note The definition of this struct is hidden from the application code. The intent + * behind defining the struct here is to simulate the actual process flow. + */ +struct MQTTVec +{ + TransportOutVector_t * pVector; /**< Pointer to transport vector. USER SHOULD NOT ACCESS THIS DIRECTLY - IT IS AN INTERNAL DETAIL AND CAN CHANGE. */ + size_t vectorLen; /**< Length of the transport vector. USER SHOULD NOT ACCESS THIS DIRECTLY - IT IS AN INTERNAL DETAIL AND CAN CHANGE. */ +}; MQTTPacketInfo_t * allocateMqttPacketInfo( MQTTPacketInfo_t * pPacketInfo ) { @@ -284,3 +304,50 @@ bool isValidMqttContext( const MQTTContext_t * pContext ) return isValid; } + +MQTTVec_t * allocateMqttVec( MQTTVec_t * mqttVec ) +{ + size_t vecLen; + TransportOutVector_t * pVector; + + if( mqttVec == NULL ) + { + mqttVec = malloc( sizeof( MQTTVec_t ) ); + } + + /* It is a part of the API contract that the #MQTT_GetBytesInMQTTVec API will be called + * with the #MQTTVec_t pointer given by the library as an input to the user defined + * #MQTTStorePacketForRetransmit callback function. The library would never provide with + * a NULL pointer. As this is a simulation of the real flow, it can be assumed that the + * mqttVec pointer is non-NULL. + */ + __CPROVER_assume( mqttVec != NULL ); + __CPROVER_assume( vecLen <= PUBLISH_PACKET_VECTORS ); + __CPROVER_assume( vecLen > 0U ); + + pVector = malloc( vecLen * sizeof( TransportOutVector_t ) ); + + /* The library is responsible with providing the memory for pVector within the mqttVec. Hence + * it can be assumed that pVector is also non-NULL + */ + __CPROVER_assume( pVector != NULL ); + + for( int i = 0; i < vecLen; i++ ) + { + /* One of there vectors will also hold the buffer pointing to the publish payload. The + * maximum size of thepublish payload is limited by the remaining length field. Hence the maximum + * size of the buffer in the vector can be 268435455 B. + */ + __CPROVER_assume( pVector[ i ].iov_len <= 268435455 ); + __CPROVER_assume( pVector[ i ].iov_len >= 0U ); + + pVector[ i ].iov_base = malloc( pVector[ i ].iov_len * sizeof( uint8_t ) ); + + __CPROVER_assume( pVector[ i ].iov_base != NULL ); + } + + mqttVec->pVector = pVector; + mqttVec->vectorLen = vecLen; + + return mqttVec; +} diff --git a/tools/coverity/README.md b/tools/coverity/README.md index 58d5d27a7..30bd46661 100644 --- a/tools/coverity/README.md +++ b/tools/coverity/README.md @@ -25,32 +25,36 @@ To compile and run the Coverity target successfully, you must have the following ### To build and run coverity: Go to the root directory of the library and run the following commands in terminal: -1. Update the compiler configuration in Coverity +1. Create a local directory for the configuration files ~~~ - cov-configure --force --compiler cc --comptype gcc + mkdir covConfig ~~~ -2. Create the build files using CMake in a `build` directory +2. Update the compiler configuration in Coverity + ~~~ + cov-configure --config covConfig/coverity.xml --compiler cc --comptype gcc --template + ~~~ +3. Create the build files using CMake in a `build` directory ~~~ cmake -B build -S test ~~~ -3. Go to the build directory and copy the coverity configuration file +4. Go to the build directory and copy the coverity configuration file ~~~ cd build/ ~~~ -4. Build the static analysis target +5. Build the static analysis target ~~~ - cov-build --emit-complementary-info --dir cov-out make coverity_analysis + cov-build --config ../covConfig/coverity.xml --emit-complementary-info --dir cov-out make coverity_analysis ~~~ -5. Go to the Coverity output directory (`cov-out`) and begin Coverity static analysis +6. Go to the Coverity output directory (`cov-out`) and begin Coverity static analysis ~~~ cd cov-out/ cov-analyze --dir . --coding-standard-config ../../tools/coverity/misra.config --tu-pattern "file('.*/source/.*')" ~~~ -6. Format the errors in HTML format so that it is more readable while removing the test and build directory from the report +7. Format the errors in HTML format so that it is more readable while removing the test and build directory from the report ~~~ cov-format-errors --dir . --file "source" --exclude-files '(/build/|/test/)' --html-output html-out; ~~~ -7. Format the errors in JSON format to perform a jq query to get a simplified list of any exceptions. +8. Format the errors in JSON format to perform a jq query to get a simplified list of any exceptions. NOTE: A blank output means there are no defects that aren't being suppressed by the config or inline comments. ~~~ cov-format-errors --dir . --file "source" --exclude-files '(/build/|/test/)' --json-output-v2 defects.json; @@ -61,10 +65,11 @@ Go to the root directory of the library and run the following commands in termin For your convenience the commands above are below to be copy/pasted into a UNIX command friendly terminal. ~~~ - cov-configure --force --compiler cc --comptype gcc; + mkdir covConfig + cov-configure --config covConfig/coverity.xml --compiler cc --comptype gcc --template cmake -B build -S test; cd build/; - cov-build --emit-complementary-info --dir cov-out make coverity_analysis; + cov-build --config ../covConfig/coverity.xml --emit-complementary-info --dir cov-out make coverity_analysis cd cov-out/ cov-analyze --dir . --coding-standard-config ../../tools/coverity/misra.config --tu-pattern "file('.*/source/.*')"; cov-format-errors --dir . --file "source" --exclude-files '(/build/|/test/)' --html-output html-out;