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 #include <stdint.h>
30
31 /* FreeRTOS includes. */
32 #include "FreeRTOS.h"
33 #include "task.h"
34
35 /* FreeRTOS+TCP includes. */
36 #include "FreeRTOS_IP.h"
37 #include "FreeRTOS_IP_Private.h"
38
39 /* CBMC includes. */
40 #include "cbmc.h"
41
42 /* We do not need to calculate the actual checksum for the proof to be complete.
43 * Neither does the checksum matter for completeness. */
usGenerateChecksum(uint16_t usSum,const uint8_t * pucNextData,size_t uxByteCount)44 uint16_t usGenerateChecksum( uint16_t usSum,
45 const uint8_t * pucNextData,
46 size_t uxByteCount )
47 {
48 __CPROVER_assert( pucNextData != NULL, "Next data in GenerateChecksum cannot be NULL" );
49
50 uint16_t usChecksum;
51
52 /* Return any random value of checksum since it does not matter for CBMC checks. */
53 return usChecksum;
54 }
55
56 /* We do not need to calculate the actual checksum for the proof to be complete.
57 * Neither does the checksum matter for completeness. */
usGenerateProtocolChecksum(const uint8_t * const pucEthernetBuffer,size_t uxBufferLength,BaseType_t xOutgoingPacket)58 uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer,
59 size_t uxBufferLength,
60 BaseType_t xOutgoingPacket )
61 {
62 __CPROVER_assert( pucEthernetBuffer != NULL, "The Ethernet buffer cannot be NULL while generating Protocol Checksum" );
63 uint16_t usProtocolChecksum;
64
65 /* Return random value of checksum since it does not matter for CBMC checks. */
66 return usProtocolChecksum;
67 }
68
69 eFrameProcessingResult_t __CPROVER_file_local_FreeRTOS_ICMP_c_prvProcessICMPEchoRequest( ICMPPacket_t * const pxICMPPacket,
70 const NetworkBufferDescriptor_t * const pxNetworkBuffer );
71
harness()72 void harness()
73 {
74 NetworkBufferDescriptor_t xNetworkBuffer;
75
76 ICMPPacket_t * pxICMPPacket = safeMalloc( sizeof( ICMPPacket_t ) );
77
78 __CPROVER_assume( pxICMPPacket != NULL );
79
80 xNetworkBuffer.xDataLength = sizeof( ICMPPacket_t );
81 xNetworkBuffer.pucEthernetBuffer = pxICMPPacket;
82
83 __CPROVER_file_local_FreeRTOS_ICMP_c_prvProcessICMPEchoRequest( pxICMPPacket, &xNetworkBuffer );
84 }
85
