Fix Buffer Over-Read (CWE-126) in DNS Response Parser

CMakeLists.txt

@@ -198,6 +198,10 @@ add_compile_options(
  $<$<COMPILE_LANG_AND_ID:C,GNU>:-fdiagnostics-color=always>
  $<$<COMPILE_LANG_AND_ID:C,Clang>:-fcolor-diagnostics>
 
+ ## Suppress warnings from kernel port files.
+ $<$<COMPILE_LANG_AND_ID:C,Clang,GNU>:-Wno-sign-compare>
+ $<$<COMPILE_LANG_AND_ID:C,Clang,GNU>:-Wno-sign-conversion>
+
  $<$<COMPILE_LANG_AND_ID:C,Clang,GNU>:-Wall>
  $<$<COMPILE_LANG_AND_ID:C,Clang,GNU>:-Wextra>
  $<$<COMPILE_LANG_AND_ID:C,Clang,GNU>:-Werror>

source/FreeRTOS_DNS_Parser.c

@@ -613,7 +613,7 @@
  }
 
  uxResult = DNS_SkipNameField( pxSet->pucByte,
- sizeof( pxSet->pcName ) );
+ pxSet->uxSourceBytesRemaining );
 
  /* Check for a malformed response. */
  if( uxResult == 0U )

test/cbmc/proofs/DNS_ParseDNSReply/Configurations.json

@@ -0,0 +1,50 @@
+{
+ "ENTRY": "DNS_ParseDNSReply",
+ "TEST_PAYLOAD_SIZE": 5,
+ "TEST_IPV4_PACKET_SIZE": 59,
+ "TEST_IPV6_PACKET_SIZE": 79,
+ "CBMCFLAGS":
+ [
+ "--unwind 1",
+ "--unwindset DNS_ParseDNSReply.0:{TEST_PAYLOAD_SIZE}",
+ "--unwindset DNS_ReadNameField.0:{TEST_PAYLOAD_SIZE}",
+ "--unwindset DNS_ReadNameField.1:{TEST_PAYLOAD_SIZE}",
+ "--unwindset parseDNSAnswer.0:{TEST_PAYLOAD_SIZE}",
+ "--unwindset strncpy.0:{TEST_PAYLOAD_SIZE}"
+ ],
+ "OPT":
+ [
+ "--export-file-local-symbols"
+ ],
+ "OBJS":
+ [
+ "$(ENTRY)_harness.goto",
+ "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto",
+ "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto"
+ ],
+ "DEF":
+ [
+ {
+ "IPv4":
+ [
+ "TEST_PACKET_SIZE={TEST_IPV4_PACKET_SIZE}",
+ "ipconfigUSE_LLMNR=1",
+ "ipconfigUSE_MDNS=1",
+ "IS_TESTING_IPV6=0"
+ ]
+ },
+ {
+ "IPv6":
+ [
+ "TEST_PACKET_SIZE={TEST_IPV6_PACKET_SIZE}",
+ "ipconfigUSE_LLMNR=1",
+ "ipconfigUSE_MDNS=1",
+ "IS_TESTING_IPV6=1"
+ ]
+ }
+ ],
+ "INC":
+ [
+ "$(FREERTOS_PLUS_TCP)/test/cbmc/include"
+ ]
+}

test/cbmc/proofs/DNS_ParseDNSReply/DNS_ParseDNSReply_harness.c

@@ -0,0 +1,211 @@
+/* Standard includes. */
+#include <stdint.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "task.h"
+#include "queue.h"
+#include "list.h"
+#include "semphr.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_DNS.h"
+#include "FreeRTOS_DNS_Parser.h"
+#include "NetworkBufferManagement.h"
+#include "NetworkInterface.h"
+#include "IPTraceMacroDefaults.h"
+
+#include "cbmc.h"
+#include "../../utility/memory_assignments.c"
+
+/****************************************************************
+* Signature of function under test
+****************************************************************/
+
+uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
+ size_t uxBufferLength,
+ struct freertos_addrinfo ** ppxAddressInfo,
+ BaseType_t xExpected,
+ uint16_t usPort );
+
+NetworkBufferDescriptor_t xNetworkBuffer;
+int lIsIPv6Packet;
+
+size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer )
+{
+ #if IS_TESTING_IPV6
+ return ipSIZE_OF_IPv6_HEADER;
+ #else
+ return ipSIZE_OF_IPv4_HEADER;
+ #endif
+}
+
+NetworkBufferDescriptor_t * pxUDPPayloadBuffer_to_NetworkBuffer( const void * pvBuffer )
+{
+ __CPROVER_assert( pvBuffer != NULL, "Precondition: pvBuffer != NULL" );
+ NetworkBufferDescriptor_t * pxRBuf;
+
+ if( nondet_bool() )
+ {
+ pxRBuf = NULL;
+ }
+ else
+ {
+ pxRBuf = &xNetworkBuffer;
+ }
+
+ return pxRBuf;
+}
+
+uint32_t ulChar2u32( const uint8_t * pucPtr )
+{
+ __CPROVER_assert( __CPROVER_r_ok( pucPtr, 4 ), "must be 4 bytes legal address to read" );
+}
+
+uint16_t usChar2u16( const uint8_t * pucPtr )
+{
+ __CPROVER_assert( __CPROVER_r_ok( pucPtr, 2 ), "must be 2 bytes legal address to read" );
+}
+
+const char * FreeRTOS_inet_ntop( BaseType_t xAddressFamily,
+ const void * pvSource,
+ char * pcDestination,
+ socklen_t uxSize )
+{
+ __CPROVER_assert( __CPROVER_r_ok( pcDestination, uxSize ), "input buffer must be available" );
+
+ #if IS_TESTING_IPV6
+ __CPROVER_assert( ( xAddressFamily == FREERTOS_AF_INET6 && __CPROVER_r_ok( pvSource, 16 ) ), "input address must be available" );
+ #else
+ __CPROVER_assert( ( xAddressFamily == FREERTOS_AF_INET && __CPROVER_r_ok( pvSource, 4 ) ), "input address must be available" );
+ #endif
+}
+
+BaseType_t xApplicationDNSQueryHook_Multi( struct xNetworkEndPoint * pxEndPoint,
+ const char * pcName )
+{
+ __CPROVER_assert( strlen( pcName ) < ipconfigDNS_CACHE_NAME_LENGTH, "The length of domain name must be less than cache size" );
+}
+
+void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+ __CPROVER_assert( pxNetworkBuffer, "network descriptor must be valid." );
+ __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer, "network buffer must be valid." );
+
+ free( pxNetworkBuffer->pucEthernetBuffer );
+ free( pxNetworkBuffer );
+}
+
+/* The checksum generation is stubbed out since the actual checksum
+ * does not matter. The stub will return an indeterminate value each time. */
+uint16_t usGenerateChecksum( uint16_t usSum,
+ const uint8_t * pucNextData,
+ size_t uxByteCount )
+{
+ uint16_t usReturn;
+
+ __CPROVER_assert( __CPROVER_r_ok( pucNextData, uxByteCount ), "Data must be valid" );
+
+ /* Return an indeterminate value. */
+ return usReturn;
+}
+
+/* The checksum generation is stubbed out since the actual checksum
+ * does not matter. The stub will return an indeterminate value each time. */
+uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer,
+ size_t uxBufferLength,
+ BaseType_t xOutgoingPacket )
+{
+ uint16_t usReturn;
+
+ __CPROVER_assert( __CPROVER_r_ok( pucEthernetBuffer, uxBufferLength ), "Data must be valid" );
+
+ /* Return an indeterminate value. */
+ return usReturn;
+}
+
+/* pxDuplicateNetworkBufferWithDescriptor() is proved separately */
+NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const NetworkBufferDescriptor_t * const pxNetworkBuffer,
+ size_t xNewLength )
+{
+ NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+
+ if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) )
+ {
+ pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xNewLength );
+ __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer );
+ pxNetworkBuffer->xDataLength = xNewLength;
+ }
+
+ return pxNetworkBuffer;
+}
+
+/* vReturnEthernetFrame() is proved separately */
+void vReturnEthernetFrame( NetworkBufferDescriptor_t * pxNetworkBuffer,
+ BaseType_t xReleaseAfterSend )
+{
+ __CPROVER_assert( pxNetworkBuffer != NULL, "xNetworkBuffer != NULL" );
+ __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "pxNetworkBuffer->pucEthernetBuffer != NULL" );
+ __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data must be valid" );
+}
+
+uint32_t parseDNSAnswer( ParseSet_t * pxSet,
+ struct freertos_addrinfo ** ppxAddressInfo,
+ size_t * uxBytesRead )
+{
+ uint32_t result;
+
+ __CPROVER_assert( __CPROVER_r_ok( pxSet->pucByte, pxSet->uxSourceBytesRemaining ), "Data must be valid" );
+
+ return result;
+}
+
+/****************************************************************
+* Proof of prvParseDNSReply
+****************************************************************/
+
+void harness()
+{
+ size_t uxBufferLength;
+ uint16_t usPort;
+ struct freertos_addrinfo * pxAddressInfo;
+ BaseType_t xExpected;
+ NetworkEndPoint_t * pxNetworkEndPoint_Temp = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
+ const uint32_t ulIpv4UdpOffset = 42, ulIpv6UdpOffset = 62;
+ uint8_t * pPayloadBuffer;
+ size_t uxPayloadBufferLength;
+
+ __CPROVER_assert( TEST_PACKET_SIZE < CBMC_MAX_OBJECT_SIZE,
+ "TEST_PACKET_SIZE < CBMC_MAX_OBJECT_SIZE" );
+
+ __CPROVER_assume( uxBufferLength < CBMC_MAX_OBJECT_SIZE );
+ __CPROVER_assume( uxBufferLength <= TEST_PACKET_SIZE );
+
+ lIsIPv6Packet = IS_TESTING_IPV6;
+
+ xNetworkBuffer.pucEthernetBuffer = safeMalloc( uxBufferLength );
+ xNetworkBuffer.xDataLength = uxBufferLength;
+ xNetworkBuffer.pxEndPoint = pxNetworkEndPoint_Temp;
+
+ __CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL );
+
+ if( lIsIPv6Packet )
+ {
+ __CPROVER_assume( uxBufferLength >= ulIpv6UdpOffset ); /* 62 is total size of IPv4 UDP header, including ethernet, IPv6, UDP headers. */
+ pPayloadBuffer = xNetworkBuffer.pucEthernetBuffer + ulIpv6UdpOffset;
+ uxPayloadBufferLength = uxBufferLength - ulIpv6UdpOffset;
+ }
+ else
+ {
+ __CPROVER_assume( uxBufferLength >= ulIpv4UdpOffset ); /* 42 is total size of IPv4 UDP header, including ethernet, IPv4, UDP headers. */
+ pPayloadBuffer = xNetworkBuffer.pucEthernetBuffer + ulIpv4UdpOffset;
+ uxPayloadBufferLength = uxBufferLength - ulIpv4UdpOffset;
+ }
+
+ uint32_t index = DNS_ParseDNSReply( pPayloadBuffer,
+ uxPayloadBufferLength,
+ &pxAddressInfo,
+ xExpected,
+ usPort );
+}