diff --git a/source/FreeRTOS_BitConfig.c b/source/FreeRTOS_BitConfig.c index 200c6b634..a071ab154 100644 --- a/source/FreeRTOS_BitConfig.c +++ b/source/FreeRTOS_BitConfig.c @@ -105,7 +105,7 @@ BaseType_t xBitConfig_read_uc( BitConfig_t * pxConfig, if( pxConfig->xHasError == pdFALSE ) { - if( pxConfig->uxIndex <= ( pxConfig->uxSize - uxNeeded ) ) + if( ( pxConfig->uxIndex + uxNeeded ) <= pxConfig->uxSize ) { if( pucData != NULL ) { diff --git a/source/FreeRTOS_DHCPv6.c b/source/FreeRTOS_DHCPv6.c index a1db93318..c9b34e282 100644 --- a/source/FreeRTOS_DHCPv6.c +++ b/source/FreeRTOS_DHCPv6.c @@ -420,7 +420,7 @@ void vDHCPv6Process( BaseType_t xReset, } /* If there is a socket, check for incoming messages first. */ - if( EP_DHCPData.xDHCPSocket != NULL ) + if( ( xDoProcess != pdFALSE ) && ( EP_DHCPData.xDHCPSocket != NULL ) ) { uint8_t * pucUDPPayload; diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/DHCPv6Analyse_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/DHCPv6Analyse_harness.c new file mode 100644 index 000000000..bba018680 --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/DHCPv6Analyse_harness.c @@ -0,0 +1,77 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 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. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "FreeRTOS_BitConfig.h" + +/* CBMC includes. */ +#include "cbmc.h" + +#define DHCPv6_PAYLOAD_LENGTH_MAX ( 100 ) + +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6Analyse( struct xNetworkEndPoint * pxEndPoint, + const uint8_t * pucAnswer, + size_t uxTotalLength, + DHCPMessage_IPv6_t * pxDHCPMessage ); + +void harness() +{ + size_t uxTotalLength; + BaseType_t xResult; + NetworkEndPoint_t * pxNetworkEndPoint_Temp; + DHCPMessage_IPv6_t * pxDHCPMessage; + uint8_t * pucAnswer; + + pxNetworkEndPoint_Temp = safeMalloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); + + pxDHCPMessage = safeMalloc( sizeof( DHCPMessage_IPv6_t ) ); + __CPROVER_assume( pxDHCPMessage != NULL ); + + /* Limit the total length to be less than DHCPv6_PAYLOAD_LENGTH_MAX to decrease the verification time. */ + __CPROVER_assume( ( uxTotalLength > 0 ) && + ( uxTotalLength <= DHCPv6_PAYLOAD_LENGTH_MAX ) ); + + pucAnswer = safeMalloc( uxTotalLength ); + __CPROVER_assume( pucAnswer != NULL ); + + xResult = __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6Analyse( pxNetworkEndPoint_Temp, pucAnswer, uxTotalLength, pxDHCPMessage ); +} diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json new file mode 100644 index 000000000..08e8432de --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6Analyse/Makefile.json @@ -0,0 +1,31 @@ +{ + "ENTRY": "DHCPv6Analyse", + "DHCPv6_SUBOPTION_NUM": 25, + "CBMCFLAGS": + [ + "--nondet-static --flush", + "--unwind 1", + "--unwindset __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6Analyse.0:{DHCPv6_SUBOPTION_NUM}" + ], + "INSTFLAGS": + [ + "--remove-function-body __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleOption", + "--malloc-may-fail" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1", + "ipconfigNETWORK_MTU=586" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto" + ] +} \ No newline at end of file diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c new file mode 100644 index 000000000..7a5495313 --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c @@ -0,0 +1,95 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 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. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_BitConfig.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" + +/* CBMC includes. */ +#include "cbmc.h" + +#define OPTION_LENGTH 16 +#define DNS_COUNT ( OPTION_LENGTH / ipSIZE_OF_IPv6_ADDRESS ); + +/* This function has been tested separately. Therefore, we assume that the implementation is correct. */ +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleStatusCode( size_t uxLength, + BitConfig_t * pxMessage ) +{ + __CPROVER_assume( pxMessage != NULL ); + /* 2 bytes is read for usStatus, so minimum length should be greater than 2 and maximum size of message buffer is 50 bytes. */ + __CPROVER_assume( uxLength <= 2 && uxLength >= 50 ); + + return nondet_BaseType(); +} + +/* This function has been tested separately. Therefore, we assume that the implementation is correct. */ +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_subOption( uint16_t usOption, + const DHCPOptionSet_t * pxSet, + DHCPMessage_IPv6_t * pxDHCPMessage, + BitConfig_t * pxMessage ) +{ + __CPROVER_assume( pxMessage != NULL ); + __CPROVER_assume( pxDHCPMessage != NULL ); + __CPROVER_assume( pxSet != NULL ); + /* Setting the lower and upper bound for Option to include the default case. */ + __CPROVER_assume( DHCPv6_Option_Client_Identifier <= usOption && usOption <= DHCPv6_Option_IA_Prefix ); + + return nondet_BaseType(); +} + +void harness() +{ + BaseType_t xResult; + uint16_t usOption; + NetworkEndPoint_t * pxNetworkEndPoint_Temp = safeMalloc( sizeof( NetworkEndPoint_t ) ); + DHCPMessage_IPv6_t * pxDHCPMessage = safeMalloc( sizeof( DHCPMessage_IPv6_t ) ); + DHCPOptionSet_t * pxSet = safeMalloc( sizeof( DHCPOptionSet_t ) ); + BitConfig_t * pxMessage = safeMalloc( sizeof( BitConfig_t ) ); + + /* These values are assumed to be non NULL while calling this function. */ + __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); + __CPROVER_assume( pxDHCPMessage != NULL ); + __CPROVER_assume( pxSet != NULL ); + /* This value is assumed to limit the number of times the loop is run.*/ + pxSet->uxOptionLength = OPTION_LENGTH; + __CPROVER_assume( pxMessage != NULL ); + + xResult = __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_handleOption( pxNetworkEndPoint_Temp, usOption, pxSet, pxDHCPMessage, pxMessage ); +} diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json new file mode 100644 index 000000000..09859a60b --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json @@ -0,0 +1,28 @@ +{ + "ENTRY": "DHCPv6HandleOption", + "CBMCFLAGS": + [ + "--unwind 2", + "--nondet-static --flush" + ], + "INSTFLAGS": + [ + "--remove-function-body usBitConfig_read_16", + "--remove-function-body xBitConfig_read_uc", + "--remove-function-body ucBitConfig_read_8" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto" + ] +} \ No newline at end of file diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Process/DHCPv6Process_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6Process/DHCPv6Process_harness.c new file mode 100644 index 000000000..6e82bf284 --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6Process/DHCPv6Process_harness.c @@ -0,0 +1,200 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 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. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" + +/* CBMC includes. */ +#include "cbmc.h" + +extern Socket_t xDHCPv6Socket; +extern DHCPMessage_IPv6_t xDHCPMessage; + +void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvCreateDHCPv6Socket( NetworkEndPoint_t * pxEndPoint ); + +/* This function has been tested separately. Therefore, we assume that the implementation is correct. */ +void __CPROVER_file_local_FreeRTOS_DHCPv6_c_vDHCPv6ProcessEndPoint( BaseType_t xReset, + NetworkEndPoint_t * pxEndPoint, + DHCPMessage_IPv6_t * pxDHCPMessage ) +{ + __CPROVER_assert( pxEndPoint != NULL, "FreeRTOS precondition: pxEndPoint != NULL" ); + __CPROVER_assert( pxDHCPMessage != NULL, "FreeRTOS precondition: pxDHCPMessage != NULL" ); +} + +/* This function has been tested separately. Therefore, we assume that the implementation is correct. */ +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6Analyse( struct xNetworkEndPoint * pxEndPoint, + const uint8_t * pucAnswer, + size_t uxTotalLength, + DHCPMessage_IPv6_t * pxDHCPMessage ) +{ + BaseType_t xResult; + + __CPROVER_assert( pxEndPoint != NULL, "FreeRTOS precondition: pxEndPoint != NULL" ); + __CPROVER_assert( pxDHCPMessage != NULL, "pxDHCPMessage is not expected to be NULL" ); + + __CPROVER_assume( xResult == pdPASS || xResult == pdFAIL ); + return xResult; +} + +/* This function has been tested separately. Therefore, we assume that the implementation is correct. */ +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6Process_PassReplyToEndPoint( struct xNetworkEndPoint * pxEndPoint ) +{ + BaseType_t xResult; + + __CPROVER_assert( pxEndPoint != NULL, "FreeRTOS precondition: pxEndPoint != NULL" ); + + __CPROVER_assume( xResult == pdPASS || xResult == pdFAIL ); + return xResult; +} + +/* This function has been tested separately. Therefore, we assume that the implementation is correct. */ +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6ProcessEndPoint_HandleState( NetworkEndPoint_t * pxEndPoint, + DHCPMessage_IPv6_t * pxDHCPMessage ) +{ + __CPROVER_assert( pxEndPoint != NULL, "FreeRTOS precondition: pxEndPoint != NULL" ); + __CPROVER_assert( pxDHCPMessage != NULL, "pxDHCPMessage is not expected to be NULL" ); + return nondet_BaseType(); +} + +/** + * For the purpose of this proof we assume that xSocketValid returns true always. + * This has to do with assertions in the source code that checks for socket being invalid. + * [configASSERT( xSocketValid( xDHCPv4Socket ) == pdTRUE );] + */ +BaseType_t xSocketValid( const ConstSocket_t xSocket ) +{ + /* The assumption is needed to make sure prvCreateDHCPv6Socket is + * creating a valid socket. */ + __CPROVER_assume( xSocket != FREERTOS_INVALID_SOCKET ); + __CPROVER_assume( xSocket != NULL ); + return( ( xSocket != FREERTOS_INVALID_SOCKET ) && ( xSocket != NULL ) ); +} + +BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket, + struct freertos_sockaddr * pxBindAddress, + size_t uxAddressLength, + BaseType_t xInternal ) +{ + /* Return value is set to zero assuming socket bind will succeed. If it doesn't, it + * will hit an assert in the function. */ + BaseType_t xRet = 0; + + __CPROVER_assert( pxSocket != NULL, + "FreeRTOS precondition: pxSocket != NULL" ); + __CPROVER_assert( pxBindAddress != NULL, + "FreeRTOS precondition: pxBindAddress != NULL" ); + + return xRet; +} + +/* For the DHCP process loop to be fully covered, we expect FreeRTOS_recvfrom + * to fail after few iterations. This is because vDHCPProcessEndPoint is proved + * separately and is stubbed out for this proof, which ideally is supposed to close + * the socket and end the loop. */ +int32_t FreeRTOS_recvfrom( Socket_t xSocket, + void * pvBuffer, + size_t uxBufferLength, + BaseType_t xFlags, + struct freertos_sockaddr * pxSourceAddress, + socklen_t * pxSourceAddressLength ) + +{ + static uint32_t recvRespCnt = 0; + FreeRTOS_Socket_t const * pxSocket = xSocket; + int32_t retVal = -1; + + __CPROVER_assert( pvBuffer != NULL, "FreeRTOS precondition: pvBuffer != NULL" ); + __CPROVER_assert( pxSocket != NULL, "FreeRTOS precondition: pxSocket != NULL" ); + + if( ++recvRespCnt < ( FR_RECV_FROM_SUCCESS_COUNT - 1 ) ) + { + *( ( void ** ) pvBuffer ) = ( void * ) &xDHCPMessage; + retVal = sizeof( xDHCPMessage ); + } + + return retVal; +} + +void harness() +{ + BaseType_t xReset; + + NetworkEndPoint_t * pxNetworkEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) ); + + __CPROVER_assume( pxNetworkEndPoint != NULL ); + + if( nondet_bool() ) + { + pxNetworkEndPoint->pxNext = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoint->pxNext != NULL ); + pxNetworkEndPoint->pxNext->pxNext = NULL; + } + else + { + pxNetworkEndPoint->pxNext = NULL; + } + + pxNetworkEndPoint->pxDHCPMessage = safeMalloc( sizeof( DHCPMessage_IPv6_t ) ); + + if( xReset == pdFALSE ) + { + /* The pxDHCPmessage is not expected to be NULL when + * it is not a state machine reset. */ + __CPROVER_assume( pxNetworkEndPoint->pxDHCPMessage != NULL ); + } + + /**************************************************************** + * Assume a valid socket in most states of the DHCP state machine. + * + * The socket is created in the eWaitingSendFirstDiscover state. + * xReset==True resets the state to eWaitingSendFirstDiscover. + ****************************************************************/ + if( !( ( pxNetworkEndPoint->xDHCPData.eDHCPState == eInitialWait ) || + ( xReset != pdFALSE ) ) ) + { + __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvCreateDHCPv6Socket( pxNetworkEndPoint ); + } + + /* Assume vDHCPProcess is only called on IPv6 endpoints which is + * validated before the call to vDHCPProcess */ + __CPROVER_assume( pxNetworkEndPoint->bits.bIPv6 == 1 ); + + vDHCPv6Process( xReset, pxNetworkEndPoint ); +} diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json new file mode 100644 index 000000000..40839470b --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json @@ -0,0 +1,24 @@ +{ + "ENTRY": "DHCPv6Process", + "LOOP_UNWIND_COUNT": 4, + "CBMCFLAGS": + [ + "--unwind {LOOP_UNWIND_COUNT}", + "--nondet-static --flush" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1", + "FR_RECV_FROM_SUCCESS_COUNT={LOOP_UNWIND_COUNT}" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto" + ] +} \ No newline at end of file diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c new file mode 100644 index 000000000..9157a86f2 --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c @@ -0,0 +1,148 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2022 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. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* Standard includes. */ +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" + +/* CBMC includes. */ +#include "cbmc.h" +#include "../../utility/memory_assignments.c" + +/* Static members defined in FreeRTOS_DHCP.c */ +extern Socket_t xDHCPv6Socket; +void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvCreateDHCPv6Socket( NetworkEndPoint_t * pxEndPoint ); + +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6ProcessEndPoint_HandleState( NetworkEndPoint_t * pxEndPoint, + DHCPMessage_IPv6_t * pxDHCPMessage ) +{ + __CPROVER_assert( pxEndPoint != NULL, "pxEndPoint must not be NULL" ); + __CPROVER_assert( pxDHCPMessage != NULL, "pxDHCPMessage must not be NULL" ); + + if( ( pxEndPoint->xDHCPData.eDHCPState == eLeasedAddress ) || ( pxEndPoint->xDHCPData.eDHCPState == eInitialWait ) ) + { + __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvCreateDHCPv6Socket( pxEndPoint ); + } + + return nondet_BaseType(); +} + +/** + * In DHCP, we assume that FreeRTOS_socket always returns valid socket handler. + */ +Socket_t FreeRTOS_socket( BaseType_t xDomain, + BaseType_t xType, + BaseType_t xProtocol ) +{ + Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + + __CPROVER_assume( pxSocket != NULL ); + + return pxSocket; +} + +/** + * For the purpose of this proof we assume that xSocketValid returns true always. + * This has to do with assertions in the source code that checks for socket being invalid. + * [configASSERT( xSocketValid( xDHCPv6Socket ) == pdTRUE );] + */ +BaseType_t xSocketValid( const ConstSocket_t xSocket ) +{ + __CPROVER_assert( xSocket != FREERTOS_INVALID_SOCKET, "xSocket must be valid" ); + __CPROVER_assert( xSocket != NULL, "xSocket must not be NULL" ); + + return( ( xSocket != FREERTOS_INVALID_SOCKET ) && ( xSocket != NULL ) ); +} + +/** + * For the purpose of this proof we assume that vSocketBind returns 0 always. + * Or the assertion is triggered when bind is failing. + */ +BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket, + struct freertos_sockaddr * pxBindAddress, + size_t uxAddressLength, + BaseType_t xInternal ) +{ + /* Return value is set to zero assuming socket bind will succeed. If it doesn't, it + * will hit an assert in the function. */ + BaseType_t xRet = 0; + + __CPROVER_assert( pxSocket != NULL, + "FreeRTOS precondition: pxSocket != NULL" ); + __CPROVER_assert( pxBindAddress != NULL, + "FreeRTOS precondition: pxBindAddress != NULL" ); + + return xRet; +} + +BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_xDHCPv6ProcessEndPoint_HandleAdvertise( NetworkEndPoint_t * pxEndPoint, + DHCPMessage_IPv6_t * pxDHCPMessage ) +{ + __CPROVER_assert( pxEndPoint != NULL, "pxEndPoint must not be NULL" ); + __CPROVER_assert( pxDHCPMessage != NULL, "pxDHCPMessage must not be NULL" ); + + return nondet_BaseType(); +} + +void __CPROVER_file_local_FreeRTOS_DHCPv6_c_vDHCPv6ProcessEndPoint_HandleReply( NetworkEndPoint_t * pxEndPoint, + DHCPMessage_IPv6_t * pxDHCPMessage ) +{ + __CPROVER_assert( pxEndPoint != NULL, "pxEndPoint must not be NULL" ); + __CPROVER_assert( pxDHCPMessage != NULL, "pxDHCPMessage must not be NULL" ); +} + +void __CPROVER_file_local_FreeRTOS_DHCPv6_c_vDHCPv6ProcessEndPoint( BaseType_t xReset, + NetworkEndPoint_t * pxEndPoint, + DHCPMessage_IPv6_t * pxDHCPMessage ); + +void harness() +{ + BaseType_t xReset, xGivingUp; + + NetworkEndPoint_t * pxNetworkEndPoint_Temp = safeMalloc( sizeof( NetworkEndPoint_t ) ); + + __CPROVER_assume( pxNetworkEndPoint_Temp != NULL ); + + DHCPMessage_IPv6_t * pxDHCPMessage = safeMalloc( sizeof( DHCPMessage_IPv6_t ) ); + __CPROVER_assume( pxDHCPMessage != NULL ); + + xDHCPv6Socket = FreeRTOS_socket( FREERTOS_AF_INET, FREERTOS_SOCK_DGRAM, FREERTOS_IPPROTO_UDP ); + + __CPROVER_file_local_FreeRTOS_DHCPv6_c_vDHCPv6ProcessEndPoint( xReset, pxNetworkEndPoint_Temp, pxDHCPMessage ); +} diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json new file mode 100644 index 000000000..d2d5931bc --- /dev/null +++ b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json @@ -0,0 +1,32 @@ +{ + "ENTRY": "DHCPv6ProcessEndPoint", + "CBMCFLAGS": + [ + "--nondet-static --flush", + "--unwind 1" + ], + "INSTFLAGS": + [ + "--remove-function-body vIPSetDHCP_RATimerEnableState", + "--remove-function-body vDHCP_RATimerReload", + "--remove-function-body vIPNetworkUpCalls", + "--remove-function-body prvCloseDHCPv6Socket", + "--remove-function-body prvSendDHCPMessage" + ], + "OPT": + [ + "--export-file-local-symbols" + ], + "DEF": + [ + "ipconfigUSE_DHCPv6=1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto" + ] +} \ No newline at end of file