Skip to content

Commit 1ab47c9

Browse files
tony-josi-awstony-josi-aws
committed
Fix potential out of bounds write (CWE-787) when processing LLMNR or mDNS queries
1 parent b1a964e commit 1ab47c9

File tree

9 files changed

+424
-70
lines changed

9 files changed

+424
-70
lines changed

‎source/FreeRTOS_DNS_Parser.c‎

Lines changed: 36 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -484,31 +484,30 @@
484484
LLMNRAnswer_t * pxAnswer;
485485
uint8_t * pucNewBuffer = NULL;
486486
size_t uxExtraLength;
487+
size_t uxDataLength = uxBufferLength +
488+
sizeof( UDPHeader_t ) +
489+
sizeof( EthernetHeader_t ) +
490+
uxIPHeaderSizePacket( pxNetworkBuffer );
487491

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

509+
if( xBufferAllocFixedSize == pdFALSE )
510+
{
512511
/* Set the size of the outgoing packet. */
513512
pxNetworkBuffer->xDataLength = uxDataLength;
514513
pxNewBuffer = pxDuplicateNetworkBufferWithDescriptor( pxNetworkBuffer,
@@ -537,7 +536,17 @@
537536
}
538537
else
539538
{
540-
pucNewBuffer = &( pxNetworkBuffer->pucEthernetBuffer[ uxUDPOffset ] );
539+
/* When xBufferAllocFixedSize is TRUE, check if the buffer size is big enough to
540+
* store the answer. */
541+
if( ( uxDataLength + uxExtraLength ) <= ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER )
542+
{
543+
pucNewBuffer = &( pxNetworkBuffer->pucEthernetBuffer[ uxUDPOffset ] );
544+
}
545+
else
546+
{
547+
/* Just to indicate that the message may not be answered. */
548+
pxNetworkBuffer = NULL;
549+
}
541550
}
542551

543552
if( ( pxNetworkBuffer != NULL ) )
@@ -1208,7 +1217,11 @@
12081217
{
12091218
/* BufferAllocation_1.c is used, the Network Buffers can contain at least
12101219
* ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER. */
1211-
configASSERT( uxSizeNeeded < ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER );
1220+
if( uxSizeNeeded > ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) )
1221+
{
1222+
/* The buffer is too small to reply. Drop silently. */
1223+
break;
1224+
}
12121225
}
12131226

12141227
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
@@ -23,6 +23,7 @@
2323
"DEF":
2424
[
2525
"ipconfigUSE_DNS_CACHE={USE_CACHE}",
26-
"ipconfigUSE_NBNS=1"
26+
"ipconfigUSE_NBNS=1",
27+
"ipconfigNETWORK_MTU=586"
2728
]
2829
}

‎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: 29 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,16 @@ NetworkBufferDescriptor_t * pxUDPPayloadBuffer_to_NetworkBuffer( const void * pv
6062

6163
uint32_t ulChar2u32( const uint8_t * pucPtr )
6264
{
65+
uint32_t ret;
6366
__CPROVER_assert( __CPROVER_r_ok( pucPtr, 4 ), "must be 4 bytes legal address to read" );
67+
return ret;
6468
}
6569

6670
uint16_t usChar2u16( const uint8_t * pucPtr )
6771
{
72+
uint16_t ret;
6873
__CPROVER_assert( __CPROVER_r_ok( pucPtr, 2 ), "must be 2 bytes legal address to read" );
74+
return ret;
6975
}
7076

7177
const char * FreeRTOS_inet_ntop( BaseType_t xAddressFamily,
@@ -131,11 +137,14 @@ NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const Networ
131137
{
132138
NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
133139

134-
if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) )
140+
if( pxNetworkBuffer != NULL )
135141
{
136142
pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xNewLength );
137-
__CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer );
143+
__CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
138144
pxNetworkBuffer->xDataLength = xNewLength;
145+
146+
pxNetworkBuffer->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
147+
__CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL );
139148
}
140149

141150
return pxNetworkBuffer;
@@ -176,23 +185,31 @@ void harness()
176185
uint8_t * pPayloadBuffer;
177186
size_t uxPayloadBufferLength;
178187

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 );
188+
__CPROVER_assume( uxBufferLength <= ipconfigNETWORK_MTU );
189+
__CPROVER_assume( pxNetworkEndPoint_Temp != NULL );
184190

185191
lIsIPv6Packet = IS_TESTING_IPV6;
186192

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

191208
__CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL );
192209

193210
if( lIsIPv6Packet )
194211
{
195-
__CPROVER_assume( uxBufferLength >= ulIpv6UdpOffset ); /* 62 is total size of IPv4 UDP header, including ethernet, IPv6, UDP headers. */
212+
__CPROVER_assume( uxBufferLength >= ulIpv6UdpOffset ); /* 62 is total size of IPv6 UDP header, including ethernet, IPv6, UDP headers. */
196213
pPayloadBuffer = xNetworkBuffer.pucEthernetBuffer + ulIpv6UdpOffset;
197214
uxPayloadBufferLength = uxBufferLength - ulIpv6UdpOffset;
198215
}

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

Lines changed: 11 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,11 @@ size_t uxIPHeaderSizeSocket( const FreeRTOS_Socket_t * pxSocket )
174177
void harness()
175178
{
176179
NetworkBufferDescriptor_t * pxNetworkBuffer;
180+
size_t tcpPacketSize;
181+
__CPROVER_assume( tcpPacketSize >= ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv4_HEADER + sizeof( TCPHeader_t ) ) );
182+
183+
pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( tcpPacketSize, 0 );
177184

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

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

0 commit comments

Comments
 (0)