From 5ea58024e0b316359c5d1e34fac44ab16f14bd45 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 8 Feb 2023 16:37:56 +0000 Subject: [PATCH 1/7] fix cbmc vProcessGeneratedUDPPacket proof --- test/cbmc/patches/FreeRTOSConfig.h | 2 +- test/cbmc/stubs/freertos_api.c | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/test/cbmc/patches/FreeRTOSConfig.h b/test/cbmc/patches/FreeRTOSConfig.h index e3ed1f8ad5..7e61af32f1 100644 --- a/test/cbmc/patches/FreeRTOSConfig.h +++ b/test/cbmc/patches/FreeRTOSConfig.h @@ -127,7 +127,7 @@ * is set to 2 so the formatting functions are included without the stdio.h being * included in tasks.c. That is because this project defines its own sprintf() * functions. */ -#define configUSE_STATS_FORMATTING_FUNCTIONS 1 +#define configUSE_STATS_FORMATTING_FUNCTIONS 0 /* Assert call defined for debug builds. */ extern void vAssertCalled( const char * pcFile, diff --git a/test/cbmc/stubs/freertos_api.c b/test/cbmc/stubs/freertos_api.c index c4e3281e61..15407a6398 100644 --- a/test/cbmc/stubs/freertos_api.c +++ b/test/cbmc/stubs/freertos_api.c @@ -212,7 +212,8 @@ int32_t FreeRTOS_sendto( Socket_t xSocket, ****************************************************************/ void * FreeRTOS_GetUDPPayloadBuffer( size_t xRequestedSizeBytes, - TickType_t xBlockTimeTicks ) + TickType_t xBlockTimeTicks, + uint8_t ucIPType ) { size_t size; @@ -225,7 +226,7 @@ void * FreeRTOS_GetUDPPayloadBuffer( size_t xRequestedSizeBytes, } /**************************************************************** -* Abstract FreeRTOS_GetUDPPayloadBuffer +* Abstract FreeRTOS_ReleaseUDPPayloadBuffer * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/FreeRTOS_ReleaseUDPPayloadBuffer.html ****************************************************************/ From 3b693273583cccade4cabff99af5811e5b2836e7 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Fri, 13 Jan 2023 17:42:24 +0000 Subject: [PATCH 2/7] Use CBMC XML output to enable VSCode debugger (#673) Prior to this commit, CBMC would emit logging information in plain text format, which does not contain information required for the CBMC VSCode debugger. This commit makes CBMC use XML instead of plain text. Co-authored-by: Mark Tuttle --- test/cbmc/proofs/Makefile.template | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/test/cbmc/proofs/Makefile.template b/test/cbmc/proofs/Makefile.template index 375c15c120..094fd560c1 100644 --- a/test/cbmc/proofs/Makefile.template +++ b/test/cbmc/proofs/Makefile.template @@ -119,8 +119,8 @@ goto: # Ignore the return code for CBMC, so that we can still generate the # report if the proof failed. If the proof failed, we separately fail # the entire job using the check-cbmc-result rule. -cbmc.txt: $(ENTRY).goto - -cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1 +cbmc.xml: $(ENTRY).goto + -cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace --xml-ui @RULE_INPUT@ > $@ 2>&1 property.xml: $(ENTRY).goto cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1 @@ -128,29 +128,27 @@ property.xml: $(ENTRY).goto coverage.xml: $(ENTRY).goto cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1 -cbmc: cbmc.txt +cbmc: cbmc.xml property: property.xml coverage: coverage.xml -report: cbmc.txt property.xml coverage.xml +report: cbmc.xml property.xml coverage.xml $(VIEWER) \ --goto $(ENTRY).goto \ --srcdir $(FREERTOS_PLUS_TCP) \ - --blddir $(FREERTOS_PLUS_TCP) \ - --htmldir html \ - --srcexclude "(.@FORWARD_SLASH@doc|.@FORWARD_SLASH@tests|.@FORWARD_SLASH@vendors)" \ - --result cbmc.txt \ + --reportdir report \ + --result cbmc.xml \ --property property.xml \ - --block coverage.xml + --coverage coverage.xml -# This rule depends only on cbmc.txt and has no dependents, so it will +# This rule depends only on cbmc.xml and has no dependents, so it will # not block the report from being generated if it fails. This rule is # intended to fail if and only if the CBMC safety check that emits -# cbmc.txt yielded a proof failure. -check-cbmc-result: cbmc.txt - grep -e "^VERIFICATION SUCCESSFUL" $^ +# cbmc.xml yielded a proof failure. +check-cbmc-result: cbmc.xml + grep 'SUCCESS' $^ # ____________________________________________________________________ # Rules @@ -160,7 +158,7 @@ check-cbmc-result: cbmc.txt clean: @RM@ $(OBJS) $(ENTRY).goto @RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt - @RM@ cbmc.txt property.xml coverage.xml TAGS TAGS-* + @RM@ cbmc.xml property.xml coverage.xml TAGS TAGS-* @RM@ *~ \#* @RM@ queue_datastructure.h From 4f83b21c7bffa6702ee51d384fb6e8270c2deacd Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Mon, 13 Feb 2023 09:58:22 +0000 Subject: [PATCH 3/7] fix cbmc proofs for vProcessGeneratedUDPPacket and ProcessReceivedUDPPacket --- .../vProcessGeneratedUDPPacket/Makefile.json | 4 ++- .../vProcessGeneratedUDPPacket_harness.c | 28 +++++++++++++++++++ .../ProcessReceivedUDPPacket/Makefile.json | 1 + 3 files changed, 32 insertions(+), 1 deletion(-) diff --git a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json index 596e49d7ab..f7ef2a84df 100644 --- a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json +++ b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json @@ -7,7 +7,9 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto", - "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IP.goto" + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IPv4.goto" ], "INSTFLAGS": [ diff --git a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c index 1f21e2a32c..5c9b6e5a1e 100644 --- a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c +++ b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c @@ -75,11 +75,23 @@ eARPLookupResult_t eARPGetCacheEntry( uint32_t * pulIPAddress, return eResult; } +BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor, + NetworkBufferDescriptor_t * const pxNetworkBuffer, + BaseType_t xReleaseAfterSend ) +{ + BaseType_t ret; + return ret; +} + void harness() { size_t xRequestedSizeBytes; + pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoints != NULL ); + __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL ); + /* Assume that the size of packet must be greater than that of UDP-Packet and less than * that of the Ethernet Frame Size. */ __CPROVER_assume( xRequestedSizeBytes >= sizeof( UDPPacket_t ) && xRequestedSizeBytes <= ipTOTAL_ETHERNET_FRAME_SIZE ); @@ -91,5 +103,21 @@ void harness() __CPROVER_assume( pxNetworkBuffer != NULL ); __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); + /* + This proof assumes one end point is present. + */ + pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL ); + __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNext == NULL ); + + /* Interface init. */ + pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) ); + __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL ); + + pxNetworkEndPoints->pxNetworkInterface = pxNetworkBuffer->pxEndPoint->pxNetworkInterface; + __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL ); + + pxNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub; + vProcessGeneratedUDPPacket( pxNetworkBuffer ); } diff --git a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json index 558025ef64..4579f9d711 100644 --- a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json +++ b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json @@ -12,6 +12,7 @@ [ "$(ENTRY)_harness.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IP.goto", + "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IPv4.goto", "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto" ], "DEF": From 018dd4a674bba54356d4284d650b006f1a1971c0 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Wed, 15 Feb 2023 18:10:07 +0530 Subject: [PATCH 4/7] adding more asserts --- source/FreeRTOS_UDP_IPv4.c | 5 ++++- .../vProcessGeneratedUDPPacket_harness.c | 8 +++++++- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/source/FreeRTOS_UDP_IPv4.c b/source/FreeRTOS_UDP_IPv4.c index 32f42a5e37..633780c0d6 100644 --- a/source/FreeRTOS_UDP_IPv4.c +++ b/source/FreeRTOS_UDP_IPv4.c @@ -297,7 +297,10 @@ void vProcessGeneratedUDPPacket_IPv4( NetworkBufferDescriptor_t * const pxNetwor } #endif /* if( ipconfigETHERNET_MINIMUM_PACKET_BYTES > 0 ) */ iptraceNETWORK_INTERFACE_OUTPUT( pxNetworkBuffer->xDataLength, pxNetworkBuffer->pucEthernetBuffer ); - ( void ) pxInterface->pfOutput( pxInterface, pxNetworkBuffer, pdTRUE ); + if( pxInterface != NULL && pxInterface->pfOutput != NULL ) + { + ( void ) pxInterface->pfOutput( pxInterface, pxNetworkBuffer, pdTRUE ); + } } else { diff --git a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c index 5c9b6e5a1e..ebdf452f45 100644 --- a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c +++ b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c @@ -79,6 +79,8 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes NetworkBufferDescriptor_t * const pxNetworkBuffer, BaseType_t xReleaseAfterSend ) { + __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." ); + __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." ); BaseType_t ret; return ret; } @@ -90,7 +92,9 @@ void harness() pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); - __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL ); + pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL ); + __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL ); /* Assume that the size of packet must be greater than that of UDP-Packet and less than * that of the Ethernet Frame Size. */ @@ -115,7 +119,9 @@ void harness() __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL ); pxNetworkEndPoints->pxNetworkInterface = pxNetworkBuffer->pxEndPoint->pxNetworkInterface; + pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkBuffer->pxEndPoint->pxNetworkInterface; __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL ); + __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL ); pxNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub; From 62a79bc9ea33e7abc4adb6dd2f2b6f22961c91fe Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 16 Feb 2023 00:33:31 +0530 Subject: [PATCH 5/7] NULL assume to assignment --- .../vProcessGeneratedUDPPacket_harness.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c index ebdf452f45..cb3d2faf09 100644 --- a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c +++ b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c @@ -94,7 +94,7 @@ void harness() __CPROVER_assume( pxNetworkEndPoints != NULL ); pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL ); - __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL ); + pxNetworkEndPoints->pxNext->pxNext = NULL; /* Assume that the size of packet must be greater than that of UDP-Packet and less than * that of the Ethernet Frame Size. */ @@ -112,7 +112,7 @@ void harness() */ pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL ); - __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNext == NULL ); + pxNetworkBuffer->pxEndPoint->pxNext = NULL; /* Interface init. */ pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) ); From ef2ebea7b11eeaae31239f29f7bffb7139eca914 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Thu, 16 Feb 2023 15:23:20 +0530 Subject: [PATCH 6/7] fixing formatting and adding more non determinism to the proof --- source/FreeRTOS_UDP_IPv4.c | 2 +- .../vProcessGeneratedUDPPacket_harness.c | 27 +++++++++++-------- 2 files changed, 17 insertions(+), 12 deletions(-) diff --git a/source/FreeRTOS_UDP_IPv4.c b/source/FreeRTOS_UDP_IPv4.c index 633780c0d6..d0a557074c 100644 --- a/source/FreeRTOS_UDP_IPv4.c +++ b/source/FreeRTOS_UDP_IPv4.c @@ -297,7 +297,7 @@ void vProcessGeneratedUDPPacket_IPv4( NetworkBufferDescriptor_t * const pxNetwor } #endif /* if( ipconfigETHERNET_MINIMUM_PACKET_BYTES > 0 ) */ iptraceNETWORK_INTERFACE_OUTPUT( pxNetworkBuffer->xDataLength, pxNetworkBuffer->pucEthernetBuffer ); - if( pxInterface != NULL && pxInterface->pfOutput != NULL ) + if( ( pxInterface != NULL ) && ( pxInterface->pfOutput != NULL ) ) { ( void ) pxInterface->pfOutput( pxInterface, pxNetworkBuffer, pdTRUE ); } diff --git a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c index cb3d2faf09..7a620e2aba 100644 --- a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c +++ b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c @@ -89,13 +89,7 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes void harness() { size_t xRequestedSizeBytes; - - pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); - __CPROVER_assume( pxNetworkEndPoints != NULL ); - pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); - __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL ); - pxNetworkEndPoints->pxNext->pxNext = NULL; - + /* Assume that the size of packet must be greater than that of UDP-Packet and less than * that of the Ethernet Frame Size. */ __CPROVER_assume( xRequestedSizeBytes >= sizeof( UDPPacket_t ) && xRequestedSizeBytes <= ipTOTAL_ETHERNET_FRAME_SIZE ); @@ -117,11 +111,22 @@ void harness() /* Interface init. */ pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) ); __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL ); - + + /* Add few endpoints */ + pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoints != NULL ); pxNetworkEndPoints->pxNetworkInterface = pxNetworkBuffer->pxEndPoint->pxNetworkInterface; - pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkBuffer->pxEndPoint->pxNetworkInterface; - __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL ); - __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL ); + if( nondet_bool() ) + { + pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); + __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL ); + pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkBuffer->pxEndPoint->pxNetworkInterface; + pxNetworkEndPoints->pxNext->pxNext = NULL; + } + else + { + pxNetworkEndPoints->pxNext = NULL; + } pxNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub; From 0a903ce89b20c8a16b508df836a6731f4d635552 Mon Sep 17 00:00:00 2001 From: tony-josi-aws Date: Fri, 17 Feb 2023 11:02:34 +0530 Subject: [PATCH 7/7] adding asserts and comments --- .../vProcessGeneratedUDPPacket_harness.c | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c index 7a620e2aba..8b03ee8a05 100644 --- a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c +++ b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c @@ -81,6 +81,7 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes { __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." ); __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." ); + __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The Ethernet buffer cannot be NULL." ); BaseType_t ret; return ret; } @@ -102,17 +103,18 @@ void harness() __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL ); /* - This proof assumes one end point is present. + Add an end point to the network buffer present. Its assumed that the + network interface layer correctly assigns the end point to the generated buffer. */ pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL ); pxNetworkBuffer->pxEndPoint->pxNext = NULL; - /* Interface init. */ + /* Add an interface */ pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) ); __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL ); - /* Add few endpoints */ + /* Add few endpoints to global pxNetworkEndPoints */ pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) ); __CPROVER_assume( pxNetworkEndPoints != NULL ); pxNetworkEndPoints->pxNetworkInterface = pxNetworkBuffer->pxEndPoint->pxNetworkInterface;