Skip to content

Commit 28dd66c

Browse files
tony-josi-awstony-josi-aws
authored
Fix potential out of bounds write (CWE-787) when processing LLMNR or mDNS queries (#1258)
* Fix potential out of bounds write (CWE-787) when processing LLMNR or mDNS queries * Fix formatting
1 parent 7fe3bc7 commit 28dd66c

File tree

9 files changed

+429
-70
lines changed

9 files changed

+429
-70
lines changed

‎source/FreeRTOS_DNS_Parser.c

Lines changed: 36 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -486,31 +486,30 @@
486486
LLMNRAnswer_t * pxAnswer;
487487
uint8_t * pucNewBuffer = NULL;
488488
size_t uxExtraLength;
489+
size_t uxDataLength = uxBufferLength +
490+
sizeof( UDPHeader_t ) +
491+
sizeof( EthernetHeader_t ) +
492+
uxIPHeaderSizePacket( pxNetworkBuffer );
489493

490-
if( xBufferAllocFixedSize == pdFALSE )
491-
{
492-
size_t uxDataLength = uxBufferLength +
493-
sizeof( UDPHeader_t ) +
494-
sizeof( EthernetHeader_t ) +
495-
uxIPHeaderSizePacket( pxNetworkBuffer );
496-
497-
#if ( ipconfigUSE_IPv6 != 0 )
498-
if( xSet.usType == dnsTYPE_AAAA_HOST )
499-
{
500-
uxExtraLength = sizeof( LLMNRAnswer_t ) + ipSIZE_OF_IPv6_ADDRESS - sizeof( pxAnswer->ulIPAddress );
501-
}
502-
else
503-
#endif /* ( ipconfigUSE_IPv6 != 0 ) */
504-
#if ( ipconfigUSE_IPv4 != 0 )
505-
{
506-
uxExtraLength = sizeof( LLMNRAnswer_t );
507-
}
508-
#else /* ( ipconfigUSE_IPv4 != 0 ) */
494+
#if ( ipconfigUSE_IPv6 != 0 )
495+
if( xSet.usType == dnsTYPE_AAAA_HOST )
509496
{
510-
/* do nothing, coverity happy */
497+
uxExtraLength = sizeof( LLMNRAnswer_t ) + ipSIZE_OF_IPv6_ADDRESS - sizeof( pxAnswer->ulIPAddress );
511498
}
512-
#endif /* ( ipconfigUSE_IPv4 != 0 ) */
499+
else
500+
#endif /* ( ipconfigUSE_IPv6 != 0 ) */
501+
#if ( ipconfigUSE_IPv4 != 0 )
502+
{
503+
uxExtraLength = sizeof( LLMNRAnswer_t );
504+
}
505+
#else /* ( ipconfigUSE_IPv4 != 0 ) */
506+
{
507+
/* do nothing, coverity happy */
508+
}
509+
#endif /* ( ipconfigUSE_IPv4 != 0 ) */
513510

511+
if( xBufferAllocFixedSize == pdFALSE )
512+
{
514513
/* Set the size of the outgoing packet. */
515514
pxNetworkBuffer->xDataLength = uxDataLength;
516515
pxNewBuffer = pxDuplicateNetworkBufferWithDescriptor( pxNetworkBuffer,
@@ -539,7 +538,17 @@
539538
}
540539
else
541540
{
542-
pucNewBuffer = &( pxNetworkBuffer->pucEthernetBuffer[ uxUDPOffset ] );
541+
/* When xBufferAllocFixedSize is TRUE, check if the buffer size is big enough to
542+
* store the answer. */
543+
if( ( uxDataLength + uxExtraLength ) <= ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER )
544+
{
545+
pucNewBuffer = &( pxNetworkBuffer->pucEthernetBuffer[ uxUDPOffset ] );
546+
}
547+
else
548+
{
549+
/* Just to indicate that the message may not be answered. */
550+
pxNetworkBuffer = NULL;
551+
}
543552
}
544553

545554
if( ( pxNetworkBuffer != NULL ) )
@@ -1214,7 +1223,11 @@
12141223
{
12151224
/* BufferAllocation_1.c is used, the Network Buffers can contain at least
12161225
* ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER. */
1217-
configASSERT( uxSizeNeeded < ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER );
1226+
if( uxSizeNeeded > ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) )
1227+
{
1228+
/* The buffer is too small to reply. Drop silently. */
1229+
break;
1230+
}
12181231
}
12191232

12201233
pxNetworkBuffer->xDataLength = uxSizeNeeded;

‎source/portable/BufferManagement/BufferAllocation_1.c

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -237,11 +237,8 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
237237
BaseType_t xInvalid = pdFALSE;
238238
UBaseType_t uxCount;
239239

240-
/* The current implementation only has a single size memory block, so
241-
* the requested size parameter is not used (yet). */
242-
( void ) xRequestedSizeBytes;
243-
244-
if( xNetworkBufferSemaphore != NULL )
240+
if( ( xNetworkBufferSemaphore != NULL ) &&
241+
( xRequestedSizeBytes <= ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) ) )
245242
{
246243
/* If there is a semaphore available, there is a network buffer
247244
* available. */
@@ -432,10 +429,18 @@ UBaseType_t uxGetNumberOfFreeNetworkBuffers( void )
432429
NetworkBufferDescriptor_t * pxResizeNetworkBufferWithDescriptor( NetworkBufferDescriptor_t * pxNetworkBuffer,
433430
size_t xNewSizeBytes )
434431
{
435-
/* In BufferAllocation_1.c all network buffer are allocated with a
436-
* maximum size of 'ipTOTAL_ETHERNET_FRAME_SIZE'.No need to resize the
437-
* network buffer. */
438-
pxNetworkBuffer->xDataLength = xNewSizeBytes;
432+
if( xNewSizeBytes <= ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) )
433+
{
434+
/* In BufferAllocation_1.c all network buffer are allocated with a
435+
* maximum size of 'ipTOTAL_ETHERNET_FRAME_SIZE'.No need to resize the
436+
* network buffer. */
437+
pxNetworkBuffer->xDataLength = xNewSizeBytes;
438+
}
439+
else
440+
{
441+
pxNetworkBuffer = NULL;
442+
}
443+
439444
return pxNetworkBuffer;
440445
}
441446

‎test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -122,10 +122,7 @@ void harness()
122122

123123
BaseType_t xDataSize;
124124

125-
/* When re-adjusting the buffer, (sizeof( NBNSAnswer_t ) - 2 * sizeof( uint16_t )) more bytes are
126-
* required to be added to the existing buffer. Make sure total bytes doesn't exceed ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER
127-
* when re-resizing. This will prevent hitting an assert if Buffer Allocation 1 is used. */
128-
__CPROVER_assume( ( xDataSize != 0 ) && ( xDataSize < ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER - ( sizeof( NBNSAnswer_t ) - 2 * sizeof( uint16_t ) ) ) ) );
125+
__CPROVER_assume( ( xDataSize > 0 ) && ( xDataSize < ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) ) );
129126

130127
xNetworkBuffer.pucEthernetBuffer = safeMalloc( xDataSize );
131128
xNetworkBuffer.xDataLength = xDataSize;

‎test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@
2424
"DEF":
2525
[
2626
"ipconfigUSE_DNS_CACHE={USE_CACHE}",
27-
"ipconfigUSE_NBNS=1"
27+
"ipconfigUSE_NBNS=1",
28+
"ipconfigNETWORK_MTU=586"
2829
]
2930
}

‎test/cbmc/proofs/DNS_ParseDNSReply/Configurations.json

Lines changed: 58 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,18 @@
11
{
22
"ENTRY": "DNS_ParseDNSReply",
3-
"TEST_PAYLOAD_SIZE": 2,
4-
"TEST_IPV4_PACKET_SIZE": 29,
5-
"TEST_IPV6_PACKET_SIZE": 49,
3+
"TEST_MAX_TEST_UNWIND_LOOP": 6,
4+
"TEST_MIN_TEST_DNS_HEADER": 12,
5+
"TEST_MIN_IPV4_UDP_PACKET_SIZE": 42,
6+
"TEST_MIN_IPV6_UDP_PACKET_SIZE": 62,
7+
"TEST_IPV4_NETWORK_MTU": "__eval {TEST_MIN_IPV4_UDP_PACKET_SIZE} + {TEST_MIN_TEST_DNS_HEADER} + {TEST_MAX_TEST_UNWIND_LOOP}",
8+
"TEST_IPV6_NETWORK_MTU": "__eval {TEST_MIN_IPV6_UDP_PACKET_SIZE} + {TEST_MIN_TEST_DNS_HEADER} + {TEST_MAX_TEST_UNWIND_LOOP}",
69
"CBMCFLAGS":
710
[
811
"--unwind 1",
9-
"--unwindset DNS_ParseDNSReply.0:{TEST_PAYLOAD_SIZE}",
10-
"--unwindset DNS_ReadNameField.0:{TEST_PAYLOAD_SIZE}",
11-
"--unwindset DNS_ReadNameField.1:{TEST_PAYLOAD_SIZE}",
12-
"--unwindset parseDNSAnswer.0:{TEST_PAYLOAD_SIZE}",
13-
"--unwindset strncpy.0:{TEST_PAYLOAD_SIZE}"
12+
"--unwindset strlen.0:{TEST_MAX_TEST_UNWIND_LOOP}",
13+
"--unwindset DNS_ParseDNSReply.0:{TEST_MAX_TEST_UNWIND_LOOP}",
14+
"--unwindset DNS_ReadNameField.0:{TEST_MAX_TEST_UNWIND_LOOP}",
15+
"--unwindset DNS_ReadNameField.1:{TEST_MAX_TEST_UNWIND_LOOP}"
1416
],
1517
"OPT":
1618
[
@@ -25,21 +27,63 @@
2527
"DEF":
2628
[
2729
{
28-
"IPv4":
30+
"IPv4_FixedNetworkBufferSize":
2931
[
30-
"TEST_PACKET_SIZE={TEST_IPV4_PACKET_SIZE}",
32+
"TEST_MAX_PAYLOAD_SIZE={TEST_MAX_TEST_UNWIND_LOOP}",
3133
"ipconfigUSE_LLMNR=1",
3234
"ipconfigUSE_MDNS=1",
33-
"IS_TESTING_IPV6=0"
35+
"IS_TESTING_IPV6=0",
36+
"IS_BUFFER_ALLOCATE_FIXED=1",
37+
"ipconfigNETWORK_MTU={TEST_IPV4_NETWORK_MTU}",
38+
"ipconfigUSE_TCP=0",
39+
"ipconfigUSE_DHCP=0",
40+
"ipconfigTCP_MSS=536",
41+
"ipconfigDNS_CACHE_NAME_LENGTH={TEST_MAX_TEST_UNWIND_LOOP}"
3442
]
3543
},
3644
{
37-
"IPv6":
45+
"IPv6_FixedNetworkBufferSize":
3846
[
39-
"TEST_PACKET_SIZE={TEST_IPV6_PACKET_SIZE}",
47+
"TEST_MAX_PAYLOAD_SIZE={TEST_MAX_TEST_UNWIND_LOOP}",
4048
"ipconfigUSE_LLMNR=1",
4149
"ipconfigUSE_MDNS=1",
42-
"IS_TESTING_IPV6=1"
50+
"IS_TESTING_IPV6=1",
51+
"IS_BUFFER_ALLOCATE_FIXED=1",
52+
"ipconfigNETWORK_MTU={TEST_IPV6_NETWORK_MTU}",
53+
"ipconfigUSE_TCP=0",
54+
"ipconfigUSE_DHCP=0",
55+
"ipconfigTCP_MSS=536",
56+
"ipconfigDNS_CACHE_NAME_LENGTH={TEST_MAX_TEST_UNWIND_LOOP}"
57+
]
58+
},
59+
{
60+
"IPv4_DynamicNetworkBufferSize":
61+
[
62+
"TEST_MAX_PAYLOAD_SIZE={TEST_MAX_TEST_UNWIND_LOOP}",
63+
"ipconfigUSE_LLMNR=1",
64+
"ipconfigUSE_MDNS=1",
65+
"IS_TESTING_IPV6=0",
66+
"IS_BUFFER_ALLOCATE_FIXED=0",
67+
"ipconfigNETWORK_MTU={TEST_IPV4_NETWORK_MTU}",
68+
"ipconfigUSE_TCP=0",
69+
"ipconfigUSE_DHCP=0",
70+
"ipconfigTCP_MSS=536",
71+
"ipconfigDNS_CACHE_NAME_LENGTH={TEST_MAX_TEST_UNWIND_LOOP}"
72+
]
73+
},
74+
{
75+
"IPv6_DynamicNetworkBufferSize":
76+
[
77+
"TEST_MAX_PAYLOAD_SIZE={TEST_MAX_TEST_UNWIND_LOOP}",
78+
"ipconfigUSE_LLMNR=1",
79+
"ipconfigUSE_MDNS=1",
80+
"IS_TESTING_IPV6=1",
81+
"IS_BUFFER_ALLOCATE_FIXED=0",
82+
"ipconfigNETWORK_MTU={TEST_IPV6_NETWORK_MTU}",
83+
"ipconfigUSE_TCP=0",
84+
"ipconfigUSE_DHCP=0",
85+
"ipconfigTCP_MSS=536",
86+
"ipconfigDNS_CACHE_NAME_LENGTH={TEST_MAX_TEST_UNWIND_LOOP}"
4387
]
4488
}
4589
],

‎test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c

Lines changed: 31 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -10,14 +10,16 @@
1010

1111
/* FreeRTOS+TCP includes. */
1212
#include "FreeRTOS_IP.h"
13+
#include "FreeRTOS_IP_Private.h"
1314
#include "FreeRTOS_DNS.h"
1415
#include "FreeRTOS_DNS_Parser.h"
1516
#include "NetworkBufferManagement.h"
1617
#include "NetworkInterface.h"
1718
#include "IPTraceMacroDefaults.h"
1819

1920
#include "cbmc.h"
20-
#include "../../utility/memory_assignments.c"
21+
22+
const BaseType_t xBufferAllocFixedSize = IS_BUFFER_ALLOCATE_FIXED;
2123

2224
/****************************************************************
2325
* Signature of function under test
@@ -60,12 +62,18 @@ NetworkBufferDescriptor_t * pxUDPPayloadBuffer_to_NetworkBuffer( const void * pv
6062

6163
uint32_t ulChar2u32( const uint8_t * pucPtr )
6264
{
65+
uint32_t ret;
66+
6367
__CPROVER_assert( __CPROVER_r_ok( pucPtr, 4 ), "must be 4 bytes legal address to read" );
68+
return ret;
6469
}
6570

6671
uint16_t usChar2u16( const uint8_t * pucPtr )
6772
{
73+
uint16_t ret;
74+
6875
__CPROVER_assert( __CPROVER_r_ok( pucPtr, 2 ), "must be 2 bytes legal address to read" );
76+
return ret;
6977
}
7078

7179
const char * FreeRTOS_inet_ntop( BaseType_t xAddressFamily,
@@ -131,11 +139,14 @@ NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const Networ
131139
{
132140
NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
133141

134-
if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) )
142+
if( pxNetworkBuffer != NULL )
135143
{
136144
pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xNewLength );
137-
__CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer );
145+
__CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
138146
pxNetworkBuffer->xDataLength = xNewLength;
147+
148+
pxNetworkBuffer->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
149+
__CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL );
139150
}
140151

141152
return pxNetworkBuffer;
@@ -176,23 +187,31 @@ void harness()
176187
uint8_t * pPayloadBuffer;
177188
size_t uxPayloadBufferLength;
178189

179-
__CPROVER_assert( TEST_PACKET_SIZE < CBMC_MAX_OBJECT_SIZE,
180-
"TEST_PACKET_SIZE < CBMC_MAX_OBJECT_SIZE" );
181-
182-
__CPROVER_assume( uxBufferLength < CBMC_MAX_OBJECT_SIZE );
183-
__CPROVER_assume( uxBufferLength <= TEST_PACKET_SIZE );
190+
__CPROVER_assume( uxBufferLength <= ipconfigNETWORK_MTU );
191+
__CPROVER_assume( pxNetworkEndPoint_Temp != NULL );
184192

185193
lIsIPv6Packet = IS_TESTING_IPV6;
186194

187-
xNetworkBuffer.pucEthernetBuffer = safeMalloc( uxBufferLength );
188-
xNetworkBuffer.xDataLength = uxBufferLength;
189-
xNetworkBuffer.pxEndPoint = pxNetworkEndPoint_Temp;
195+
if( xBufferAllocFixedSize != pdFALSE )
196+
{
197+
/* When xBufferAllocFixedSize is true, buffers in all network descriptors
198+
* is big enough to allow all Ethernet packet. */
199+
xNetworkBuffer.pucEthernetBuffer = safeMalloc( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER );
200+
xNetworkBuffer.xDataLength = uxBufferLength;
201+
xNetworkBuffer.pxEndPoint = pxNetworkEndPoint_Temp;
202+
}
203+
else
204+
{
205+
xNetworkBuffer.pucEthernetBuffer = safeMalloc( uxBufferLength );
206+
xNetworkBuffer.xDataLength = uxBufferLength;
207+
xNetworkBuffer.pxEndPoint = pxNetworkEndPoint_Temp;
208+
}
190209

191210
__CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL );
192211

193212
if( lIsIPv6Packet )
194213
{
195-
__CPROVER_assume( uxBufferLength >= ulIpv6UdpOffset ); /* 62 is total size of IPv4 UDP header, including ethernet, IPv6, UDP headers. */
214+
__CPROVER_assume( uxBufferLength >= ulIpv6UdpOffset ); /* 62 is total size of IPv6 UDP header, including ethernet, IPv6, UDP headers. */
196215
pPayloadBuffer = xNetworkBuffer.pucEthernetBuffer + ulIpv6UdpOffset;
197216
uxPayloadBufferLength = uxBufferLength - ulIpv6UdpOffset;
198217
}

‎test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -47,8 +47,7 @@ void prvTCPReturnPacket( FreeRTOS_Socket_t * pxSocket,
4747
uint32_t ulLen,
4848
BaseType_t xReleaseAfterSend )
4949
{
50-
__CPROVER_assert( pxSocket != NULL, "pxSocket should not be NULL" );
51-
__CPROVER_assert( pxDescriptor != NULL, "pxDescriptor should not be NULL" );
50+
__CPROVER_assert( pxSocket != NULL || pxDescriptor != NULL, "Either pxSocket or pxDescriptor must be non-NULL" );
5251
__CPROVER_assert( pxDescriptor->pucEthernetBuffer != NULL, "pucEthernetBuffer should not be NULL" );
5352
}
5453

@@ -57,11 +56,14 @@ int32_t prvTCPPrepareSend( FreeRTOS_Socket_t * pxSocket,
5756
NetworkBufferDescriptor_t ** ppxNetworkBuffer,
5857
UBaseType_t uxOptionsLength )
5958
{
59+
int32_t ret = nondet_int32();
60+
6061
__CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
6162
__CPROVER_assert( *ppxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" );
6263
__CPROVER_assert( __CPROVER_r_ok( ( *ppxNetworkBuffer )->pucEthernetBuffer, ( *ppxNetworkBuffer )->xDataLength ), "Data in *ppxNetworkBuffer must be readable" );
6364

64-
return nondet_int32();
65+
__CPROVER_assume( ret >= 0 && ret <= ipconfigNETWORK_MTU );
66+
return ret;
6567
}
6668

6769
/* prvTCPHandleState is proven separately. */
@@ -137,6 +139,7 @@ FreeRTOS_Socket_t * pxTCPSocketLookup( uint32_t ulLocalIP,
137139
{
138140
/* This test case is for IPv4. */
139141
__CPROVER_assume( xRetSocket->bits.bIsIPv6 == pdFALSE );
142+
__CPROVER_assume( xRetSocket->u.xTCP.ucPeerWinScaleFactor <= tcpTCP_OPT_WSOPT_MAXIMUM_VALUE );
140143
}
141144

142145
return xRetSocket;
@@ -151,7 +154,7 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
151154
if( pxNetworkBuffer )
152155
{
153156
pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes );
154-
__CPROVER_assume( pxNetworkBuffer->xDataLength == ipSIZE_OF_ETH_HEADER + sizeof( int32_t ) );
157+
pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
155158
}
156159

157160
return pxNetworkBuffer;
@@ -174,8 +177,12 @@ size_t uxIPHeaderSizeSocket( const FreeRTOS_Socket_t * pxSocket )
174177
void harness()
175178
{
176179
NetworkBufferDescriptor_t * pxNetworkBuffer;
180+
size_t tcpPacketSize;
181+
182+
__CPROVER_assume( tcpPacketSize >= ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv4_HEADER + sizeof( TCPHeader_t ) ) );
183+
184+
pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( tcpPacketSize, 0 );
177185

178-
pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( sizeof( TCPPacket_t ), 0 );
179186

180187
/* To avoid asserting on the network buffer being NULL. */
181188
__CPROVER_assume( pxNetworkBuffer != NULL );

0 commit comments

Comments
 (0)