1 /*
2  * FreeRTOS memory safety proofs with CBMC.
3  * Copyright (C) 2022 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
4  *
5  * Permission is hereby granted, free of charge, to any person
6  * obtaining a copy of this software and associated documentation
7  * files (the "Software"), to deal in the Software without
8  * restriction, including without limitation the rights to use, copy,
9  * modify, merge, publish, distribute, sublicense, and/or sell copies
10  * of the Software, and to permit persons to whom the Software is
11  * furnished to do so, subject to the following conditions:
12  *
13  * The above copyright notice and this permission notice shall be
14  * included in all copies or substantial portions of the Software.
15  *
16  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
17  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
18  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
19  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
20  * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
21  * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
22  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
23  * SOFTWARE.
24  *
25  * http://aws.amazon.com/freertos
26  * http://www.FreeRTOS.org
27  */
28 
29 /* FreeRTOS includes. */
30 #include "FreeRTOS.h"
31 #include "queue.h"
32 
33 /* FreeRTOS+TCP includes. */
34 #include "FreeRTOS_IP.h"
35 #include "FreeRTOS_IP_Private.h"
36 
37 /* CBMC includes. */
38 #include "cbmc.h"
39 
40 /* Function usGenerateChecksum is proven to be correct separately.
41  * Check if input buffer is readable. */
usGenerateChecksum(uint16_t usSum,const uint8_t * pucNextData,size_t uxByteCount)42 uint16_t usGenerateChecksum( uint16_t usSum,
43                              const uint8_t * pucNextData,
44                              size_t uxByteCount )
45 {
46     __CPROVER_assert( __CPROVER_r_ok( pucNextData, uxByteCount ), "pucNextData should be readable." );
47 }
48 
harness()49 void harness()
50 {
51     size_t uxBufferLength;
52     uint8_t * pucEthernetBuffer;
53     BaseType_t xOutgoingPacket;
54     EthernetHeader_t * pxEthernetHeader;
55     IPPacket_t * pxIPPacket;
56     uint16_t usHeaderLength;
57 
58     /* The buffer must contain enough buffer size for ethernet header + IPv4 header and less than MTU size. */
59     __CPROVER_assume( uxBufferLength >= ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv4_HEADER + sizeof( ProtocolHeaders_t ) && uxBufferLength < ipconfigNETWORK_MTU );
60     pucEthernetBuffer = safeMalloc( uxBufferLength );
61     __CPROVER_assume( pucEthernetBuffer != NULL );
62 
63     /* This test case verifies IPv4 only. */
64     pxIPPacket = ( IPPacket_t * ) pucEthernetBuffer;
65     __CPROVER_assume( pxIPPacket->xEthernetHeader.usFrameType == ipIPv4_FRAME_TYPE );
66 
67     /* Make sure the length of buffer is enough for protocol header.
68      * CBMC checks union structure before accessing it, so we need to make sure the buffer size is enough for whole union structure. */
69     usHeaderLength = pxIPPacket->xIPHeader.ucVersionHeaderLength & ( uint8_t ) 0x0FU;
70     usHeaderLength = usHeaderLength << 2;
71     __CPROVER_assume( uxBufferLength >= ipSIZE_OF_ETH_HEADER + usHeaderLength + sizeof( ProtocolHeaders_t ) );
72     /* IPv4 header length is checked in prvProcessIPPacket. */
73     __CPROVER_assume( ( usHeaderLength <= ( uxBufferLength - ipSIZE_OF_ETH_HEADER ) ) && ( usHeaderLength >= ipSIZE_OF_IPv4_HEADER ) );
74 
75     /* Set to valid input. */
76     __CPROVER_assume( ( xOutgoingPacket == pdTRUE ) || ( xOutgoingPacket == pdFALSE ) );
77 
78     ( void ) usGenerateProtocolChecksum( pucEthernetBuffer, uxBufferLength, xOutgoingPacket );
79 }
80