Skip to content

Changes to recreate and expose CVEs #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
AmPaschal wants to merge 1 commit into
base: nier-base
Choose a base branch
from
Open

Changes to recreate and expose CVEs #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions source/FreeRTOS_ICMP.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,9 +86,11 @@

iptraceICMP_PACKET_RECEIVED();

configASSERT( pxNetworkBuffer->xDataLength >= sizeof( ICMPPacket_t ) );
// ICSE-NIER: Commented out the following two checks to expose CVE-2018-16527
// configASSERT( pxNetworkBuffer->xDataLength >= sizeof( ICMPPacket_t ) );

if( pxNetworkBuffer->xDataLength >= sizeof( ICMPPacket_t ) )
// if( pxNetworkBuffer->xDataLength >= sizeof( ICMPPacket_t ) )
// if (pdTRUE)
{
/* Map the buffer onto a ICMP-Packet struct to easily access the
* fields of ICMP packet. */
Expand Down
2 changes: 2 additions & 0 deletions source/FreeRTOS_TCP_IP.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -703,7 +703,9 @@
uxIPHeaderOffset = ipSIZE_OF_ETH_HEADER + uxIPHeaderSizePacket( pxNetworkBuffer );

/* Check for a minimum packet size. */
// ICSE-NIER: Commented out the validation to expose CVE-2018-16603
if( pxNetworkBuffer->xDataLength < ( uxIPHeaderOffset + ipSIZE_OF_TCP_HEADER ) )
// if (pdFALSE)
{
xResult = pdFAIL;
}
Expand Down
37 changes: 22 additions & 15 deletions source/FreeRTOS_TCP_Reception.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,10 @@
if( pxNetworkBuffer->xDataLength > uxOptionOffset )
{
/* Validate options size calculation. */
if( uxOptionsLength <= ( pxNetworkBuffer->xDataLength - uxOptionOffset ) )

// ICSE-NIER - Commented out to reproduce CVE-2018-16524
// if( uxOptionsLength <= ( pxNetworkBuffer->xDataLength - uxOptionOffset ) )
if (pdTRUE)
{
if( ( pxTCPHeader->ucTCPFlags & tcpTCP_FLAG_SYN ) != ( uint8_t ) 0U )
{
Expand Down Expand Up @@ -262,28 +265,32 @@
if( pxSocket->u.xTCP.usMSS != uxNewMSS )
{
/* Perform a basic check on the the new MSS. */
if( uxNewMSS == 0U )
{
lIndex = -1;

/* Return Condition found. */
xReturn = pdTRUE;
}
else
{
FreeRTOS_debug_printf( ( "MSS change %u -> %u\n", pxSocket->u.xTCP.usMSS, ( unsigned ) uxNewMSS ) );
}
// ICSE-NIER - Commented out to reproduce CVE-2018-16523
// if( uxNewMSS == 0U )
// {
// lIndex = -1;

// /* Return Condition found. */
// xReturn = pdTRUE;
// }
// else
// {
// FreeRTOS_debug_printf( ( "MSS change %u -> %u\n", pxSocket->u.xTCP.usMSS, ( unsigned ) uxNewMSS ) );
// }
}

/* If a 'return' condition has not been found. */
if( xReturn == pdFALSE )
{
/* Restrict the minimum value of segment length to the ( Minimum IP MTU (576) - IP header(20) - TCP Header(20) ).
* See "RFC 791 section 3.1 Total Length" for more details. */
if( uxNewMSS < tcpMINIMUM_SEGMENT_LENGTH )
{
uxNewMSS = tcpMINIMUM_SEGMENT_LENGTH;
}

// ICSE-NIER - Commented out to reproduce CVE-2018-16523
// if( uxNewMSS < tcpMINIMUM_SEGMENT_LENGTH )
// {
// uxNewMSS = tcpMINIMUM_SEGMENT_LENGTH;
// }

if( pxSocket->u.xTCP.usMSS > uxNewMSS )
{
Expand Down
10 changes: 6 additions & 4 deletions test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,16 +70,18 @@ void harness()
* is at least allocated to sizeof(ARPPacket_t) size but eventually an even larger buffer.
* This is not checked inside eARPProcessPacket.
*/
uint8_t ucBUFFER_SIZE;

void * xBuffer = malloc( ucBUFFER_SIZE + sizeof( ARPPacket_t ) );
uint8_t ucBUFFER_SIZE;

// ICSE-NIER: Updated the buffer size so it can contain truncated ARP header, reproducing CVE-2018-16600
// void * xBuffer = malloc( ucBUFFER_SIZE + sizeof( ARPPacket_t ) );
void * xBuffer = malloc( ucBUFFER_SIZE + sizeof( EthernetHeader_t ) );

__CPROVER_assume( xBuffer != NULL );

NetworkBufferDescriptor_t xNetworkBuffer2;

xNetworkBuffer2.pucEthernetBuffer = xBuffer;
xNetworkBuffer2.xDataLength = ucBUFFER_SIZE + sizeof( ARPPacket_t );
xNetworkBuffer2.xDataLength = ucBUFFER_SIZE + sizeof( EthernetHeader_t );

/*
* This proof assumes one end point is present.
Expand Down
13 changes: 3 additions & 10 deletions test/cbmc/proofs/CheckOptions/CheckOptions_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,9 @@ int32_t __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOpti
FreeRTOS_Socket_t * const pxSocket,
BaseType_t xHasSYNFlag )
{
// ICSE-NIER: Added this constraint to expose CVE-2018-16524
__CPROVER_assert(__CPROVER_rw_ok(pucPtr, uxTotalLength), "p is readable and writable");

/* CBMC model of pointers limits the size of the buffer */

/* Preconditions */
Expand All @@ -73,16 +76,6 @@ int32_t __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOpti
return index;
}

size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer )
{
__CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer should not be NULL" );
return uxIPHeaderSizePacket_uxResult;
}

/****************************************************************
* Proof of CheckOptions
****************************************************************/

void harness()
{
/* Give buffer_size an unconstrained value */
Expand Down
3 changes: 2 additions & 1 deletion test/cbmc/proofs/CheckOptionsOuter/Makefile.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,8 @@
"ENTRY": "CheckOptionsOuter",
"CBMCFLAGS":
[
"--unwind 1",
"--div-by-zero-check",
"--unwind 1",
"--unwindset __CPROVER_file_local_FreeRTOS_TCP_Reception_c_prvSingleStepTCPHeaderOptions.0:32"
],
"OPT":
Expand Down
12 changes: 10 additions & 2 deletions test/cbmc/proofs/ICMP/ProcessICMPPacket/ProcessICMPPacket_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,13 +58,21 @@ void harness()
{
NetworkBufferDescriptor_t xNetworkBuffer;

// ICSE-NIER: Updated this harness to expose CVE-2018-16527
uint8_t data_size;

__CPROVER_assume( data_size < 1000 );

/* Allocate a ICMP packet */
ICMPPacket_t * const pxICMPPacket = safeMalloc( sizeof( ICMPPacket_t ) );
// ICMPPacket_t * const pxICMPPacket = safeMalloc( sizeof( ICMPPacket_t ) );
ICMPPacket_t * const pxICMPPacket = safeMalloc( data_size );

__CPROVER_assume( pxICMPPacket != NULL );

xNetworkBuffer.xDataLength = sizeof( ICMPPacket_t );
// xNetworkBuffer.xDataLength = sizeof( ICMPPacket_t );
xNetworkBuffer.xDataLength = data_size;
xNetworkBuffer.pucEthernetBuffer = pxICMPPacket;

ProcessICMPPacket( &xNetworkBuffer );
}

2 changes: 1 addition & 1 deletion test/cbmc/proofs/ParseDNSReply/Makefile.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@
"OBJS":
[
"$(ENTRY)_harness.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
"$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto",
"$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto"
],

Expand Down
43 changes: 29 additions & 14 deletions test/cbmc/proofs/ParseDNSReply/ParseDNSReply_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,18 +25,28 @@
* Signature of function under test
****************************************************************/

uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
size_t uxBufferLength,
BaseType_t xExpected );
// ICSE-NIER: Updated the function signature to expose CVE-2018-16525
// uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
// size_t uxBufferLength,
// BaseType_t xExpected );

uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
size_t uxBufferLength,
struct freertos_addrinfo ** ppxAddressInfo,
BaseType_t xExpected,
uint16_t usPort );

/****************************************************************
* Abstraction of DNS_ReadNameField proved in ReadNameField
****************************************************************/

size_t DNS_ReadNameField( const uint8_t * pucByte,
size_t uxRemainingBytes,
char * pcName,
size_t uxDestLen )
// ICSE-NIER: Updated the function signature to expose CVE-2018-16525
size_t DNS_ReadNameField( ParseSet_t * pxSet,
size_t uxDestLen )
// size_t DNS_ReadNameField( const uint8_t * pucByte,
// size_t uxRemainingBytes,
// char * pcName,
// size_t uxDestLen )
{
__CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE,
"NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE" );
Expand All @@ -47,12 +57,12 @@ size_t DNS_ReadNameField( const uint8_t * pucByte,


/* Preconditions */
__CPROVER_assert( uxRemainingBytes < CBMC_MAX_OBJECT_SIZE,
__CPROVER_assert( pxSet->uxSourceBytesRemaining < CBMC_MAX_OBJECT_SIZE,
"ReadNameField: uxRemainingBytes < CBMC_MAX_OBJECT_SIZE)" );
__CPROVER_assert( uxDestLen < CBMC_MAX_OBJECT_SIZE,
"ReadNameField: uxDestLen < CBMC_MAX_OBJECT_SIZE)" );

__CPROVER_assert( uxRemainingBytes <= NETWORK_BUFFER_SIZE,
__CPROVER_assert( pxSet->uxSourceBytesRemaining <= NETWORK_BUFFER_SIZE,
"ReadNameField: uxRemainingBytes <= NETWORK_BUFFER_SIZE)" );

/* This precondition in the function contract for prvReadNameField
Expand All @@ -62,9 +72,9 @@ size_t DNS_ReadNameField( const uint8_t * pucByte,
* "ReadNameField: uxDestLen <= NAME_SIZE)");
*/

__CPROVER_assert( pucByte != NULL,
__CPROVER_assert( pxSet->pucByte != NULL,
"ReadNameField: pucByte != NULL )" );
__CPROVER_assert( pcName != NULL,
__CPROVER_assert( pxSet->pcName != NULL,
"ReadNameField: pcName != NULL )" );

__CPROVER_assert( uxDestLen > 0,
Expand All @@ -74,7 +84,7 @@ size_t DNS_ReadNameField( const uint8_t * pucByte,
size_t index;

/* Postconditions */
__CPROVER_assume( index <= uxDestLen + 1 && index <= uxRemainingBytes );
__CPROVER_assume( index <= uxDestLen + 1 && index <= pxSet->uxSourceBytesRemaining );

return index;
}
Expand Down Expand Up @@ -115,6 +125,8 @@ void harness()
{
size_t uxBufferLength;
BaseType_t xExpected;
uint16_t usPort;
struct freertos_addrinfo * pxAddressInfo;
uint8_t * pucUDPPayloadBuffer = malloc( uxBufferLength );

__CPROVER_assert( NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE,
Expand All @@ -124,7 +136,10 @@ void harness()
__CPROVER_assume( uxBufferLength <= NETWORK_BUFFER_SIZE );
__CPROVER_assume( pucUDPPayloadBuffer != NULL );

uint32_t index = prvParseDNSReply( pucUDPPayloadBuffer,
// ICSE-NIER: Updated the function invocation to expose CVE-2018-16525
uint32_t index = DNS_ParseDNSReply( pucUDPPayloadBuffer,
uxBufferLength,
xExpected );
&pxAddressInfo,
xExpected,
usPort );
}
8 changes: 7 additions & 1 deletion test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,13 @@ void harness()
/* To avoid asserting on the network buffer being NULL. */
__CPROVER_assume( pxNetworkBuffer != NULL );

pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) );
// ICSE-NIER: Made the buffer size non-deterministic to recreate CVE-2018-16603
// pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) );

uint8_t data_size;
__CPROVER_assume(data_size > 54);
pxNetworkBuffer->pucEthernetBuffer = safeMalloc( data_size );
pxNetworkBuffer->xDataLength = data_size;

/* To avoid asserting on the ethernet buffer being NULL. */
__CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
Expand Down