diff --git a/FreeRTOS/Test/CBMC/README.md b/FreeRTOS/Test/CBMC/README.md index b7e8d37f91..4473fe33d4 100644 --- a/FreeRTOS/Test/CBMC/README.md +++ b/FreeRTOS/Test/CBMC/README.md @@ -2,7 +2,7 @@ CBMC Proof Infrastructure ========================= This directory contains automated proofs of the memory safety of various parts -of the amazon:FreeRTOS codebase. A continuous integration system validates every +of the FreeRTOS codebase. A continuous integration system validates every pull request posted to the repository against these proofs, and developers can also run the proofs on their local machines. @@ -27,16 +27,16 @@ CMake-based build Follow the CBMC installation instructions below. -Suppose that the amazon-freertos source tree is located at -`~/src/amazon-freertos` and you wish to build the proofs into -`~/build/amazon-freertos`. The following three commands build and run +Suppose that the freertos source tree is located at +`~/src/freertos` and you wish to build the proofs into +`~/build/freertos`. The following three commands build and run the proofs: ```sh -cmake -S~/src/amazon-freertos -B~/build/amazon-freertos -DCOMPILER=cbmc +cmake -S~/src/freertos -B~/build/freertos -DCOMPILER=cbmc -DBOARD=windows -DVENDOR=pc -cmake --build ~/build/amazon-freertos --target all-proofs -cd ~/build/amazon-freertos && ctest -L cbmc +cmake --build ~/build/freertos --target all-proofs +cd ~/build/freertos && ctest -L cbmc ``` Alternatively, this single command does the same thing, assuming you @@ -44,8 +44,8 @@ have the Ninja build tool installed: ```sh ctest --build-and-test \ - ~/src/amazon-freertos \ - ~/build/amazon-freertos \ + ~/src/freertos \ + ~/build/freertos \ --build-target cbmc \ --build-generator Ninja \ --build-options \ diff --git a/FreeRTOS/Test/CBMC/patches/0001-Remove-static-storage-class-from-entry-points.patch b/FreeRTOS/Test/CBMC/patches/0001-Remove-static-storage-class-from-entry-points.patch index 323e272029..fa7d7451f4 100644 --- a/FreeRTOS/Test/CBMC/patches/0001-Remove-static-storage-class-from-entry-points.patch +++ b/FreeRTOS/Test/CBMC/patches/0001-Remove-static-storage-class-from-entry-points.patch @@ -14,10 +14,10 @@ Patch revised on October 21, 2019. .../freertos_plus_tcp/source/FreeRTOS_TCP_WIN.c | 2 +- 3 files changed, 10 insertions(+), 10 deletions(-) -diff --git a/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_DHCP.c b/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_DHCP.c +diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c index c4f79e8e7..d8089a5e7 100644 ---- a/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_DHCP.c -+++ b/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_DHCP.c +--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c ++++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.c @@ -198,7 +198,7 @@ static void prvSendDHCPDiscover( void ); /* * Interpret message received on the DHCP socket. @@ -45,10 +45,10 @@ index c4f79e8e7..d8089a5e7 100644 { uint8_t *pucUDPPayload, *pucLastByte; struct freertos_sockaddr xClient; -diff --git a/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_DNS.c b/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_DNS.c +diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c index e511ca324..d6f335304 100644 ---- a/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_DNS.c -+++ b/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_DNS.c +--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c ++++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.c @@ -116,7 +116,7 @@ static size_t prvCreateDNSMessage( uint8_t *pucUDPPayloadBuffer, /* * Simple routine that jumps over the NAME field of a resource record. @@ -103,10 +103,10 @@ index e511ca324..d6f335304 100644 size_t uxBufferLength, BaseType_t xExpected ) { -diff --git a/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_TCP_WIN.c b/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_TCP_WIN.c +diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c index 1f5a845fa..1a69807c0 100644 ---- a/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_TCP_WIN.c -+++ b/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_TCP_WIN.c +--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c ++++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.c @@ -206,7 +206,7 @@ extern void vListInsertGeneric( List_t * const pxList, ListItem_t * const pxNewL /* List of free TCP segments. */ diff --git a/FreeRTOS/Test/CBMC/patches/0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch b/FreeRTOS/Test/CBMC/patches/0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch index 922091653b..8e096a5a92 100644 --- a/FreeRTOS/Test/CBMC/patches/0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch +++ b/FreeRTOS/Test/CBMC/patches/0002-Change-FreeRTOS_IP_Private.h-union-to-struct.patch @@ -8,10 +8,10 @@ This patch should be removed soon: It is for a CBMC issue being fixed now. libraries/freertos_plus/standard/freertos_plus_tcp/include/FreeRTOS_IP_Private.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) -diff --git a/libraries/freertos_plus/standard/freertos_plus_tcp/include/FreeRTOS_IP_Private.h b/libraries/freertos_plus/standard/freertos_plus_tcp/include/FreeRTOS_IP_Private.h +diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h index 6006f89f0..d1a0cf898 100644 ---- a/libraries/freertos_plus/standard/freertos_plus_tcp/include/FreeRTOS_IP_Private.h -+++ b/libraries/freertos_plus/standard/freertos_plus_tcp/include/FreeRTOS_IP_Private.h +--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h ++++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include/FreeRTOS_IP_Private.h @@ -643,7 +643,7 @@ typedef struct XSOCKET /* Before accessing any member of this structure, it should be confirmed */ /* that the protocol corresponds with the type of structure */ diff --git a/FreeRTOS/Test/CBMC/patches/0008-Remove-static-attributes-from-functions-implementing.patch b/FreeRTOS/Test/CBMC/patches/0008-Remove-static-attributes-from-functions-implementing.patch index c62dd051a4..c8f9c36e6a 100644 --- a/FreeRTOS/Test/CBMC/patches/0008-Remove-static-attributes-from-functions-implementing.patch +++ b/FreeRTOS/Test/CBMC/patches/0008-Remove-static-attributes-from-functions-implementing.patch @@ -8,10 +8,10 @@ Subject: [PATCH] Remove static attributes from functions implementing .../freertos_plus_tcp/source/FreeRTOS_TCP_IP.c | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) -diff --git a/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_TCP_IP.c b/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_TCP_IP.c +diff --git a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c index 4378e28de..2cd072d24 100644 ---- a/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_TCP_IP.c -+++ b/libraries/freertos_plus/standard/freertos_plus_tcp/source/FreeRTOS_TCP_IP.c +--- a/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c ++++ b/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.c @@ -225,20 +225,20 @@ static BaseType_t prvTCPPrepareConnect( FreeRTOS_Socket_t *pxSocket ); /* * Parse the TCP option(s) received, if present. diff --git a/FreeRTOS/Test/CBMC/patches/FreeRTOSConfig.h b/FreeRTOS/Test/CBMC/patches/FreeRTOSConfig.h index 281ddafd7b..28de2bd157 100644 --- a/FreeRTOS/Test/CBMC/patches/FreeRTOSConfig.h +++ b/FreeRTOS/Test/CBMC/patches/FreeRTOSConfig.h @@ -134,6 +134,103 @@ extern void vAssertCalled( const char * pcFile, #define configASSERT( x ) if( ( x ) == 0 ) vAssertCalled( __FILE__, __LINE__ ) #endif +/* Remove logging in formal verification */ +#define configPRINTF( X ) + +/* Non-format version thread-safe print. */ +#define configPRINT_STRING( X ) + +/* Application specific definitions follow. **********************************/ + +/* If configINCLUDE_DEMO_DEBUG_STATS is set to one, then a few basic IP trace + * macros are defined to gather some UDP stack statistics that can then be viewed + * through the CLI interface. */ +#define configINCLUDE_DEMO_DEBUG_STATS 1 + +/* The size of the global output buffer that is available for use when there + * are multiple command interpreters running at once (for example, one on a UART + * and one on TCP/IP). This is done to prevent an output buffer being defined by + * each implementation - which would waste RAM. In this case, there is only one + * command interpreter running, and it has its own local output buffer, so the + * global buffer is just set to be one byte long as it is not used and should not + * take up unnecessary RAM. */ +#define configCOMMAND_INT_MAX_OUTPUT_SIZE 1 + +/* Only used when running in the FreeRTOS Windows simulator. Defines the + * priority of the task used to simulate Ethernet interrupts. */ +#define configMAC_ISR_SIMULATOR_PRIORITY ( configMAX_PRIORITIES - 1 ) + +/* This demo creates a virtual network connection by accessing the raw Ethernet + * or WiFi data to and from a real network connection. Many computers have more + * than one real network port, and configNETWORK_INTERFACE_TO_USE is used to tell + * the demo which real port should be used to create the virtual port. The ports + * available are displayed on the console when the application is executed. For + * example, on my development laptop setting configNETWORK_INTERFACE_TO_USE to 4 + * results in the wired network being used, while setting + * configNETWORK_INTERFACE_TO_USE to 2 results in the wireless network being + * used. */ +#define configNETWORK_INTERFACE_TO_USE ( 0L ) + +/* The address of an echo server that will be used by the two demo echo client + * tasks: + * http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_Echo_Clients.html, + * http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/UDP_Echo_Clients.html. */ +#define configECHO_SERVER_ADDR0 192 +#define configECHO_SERVER_ADDR1 168 +#define configECHO_SERVER_ADDR2 2 +#define configECHO_SERVER_ADDR3 6 +#define configTCP_ECHO_CLIENT_PORT 7 + +/* Default MAC address configuration. The demo creates a virtual network + * connection that uses this MAC address by accessing the raw Ethernet/WiFi data + * to and from a real network connection on the host PC. See the + * configNETWORK_INTERFACE_TO_USE definition above for information on how to + * configure the real network connection to use. */ +#define configMAC_ADDR0 0x00 +#define configMAC_ADDR1 0x11 +#define configMAC_ADDR2 0x22 +#define configMAC_ADDR3 0x33 +#define configMAC_ADDR4 0x44 +#define configMAC_ADDR5 0x21 + +/* Default IP address configuration. Used in ipconfigUSE_DHCP is set to 0, or + * ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configIP_ADDR0 192 +#define configIP_ADDR1 168 +#define configIP_ADDR2 0 +#define configIP_ADDR3 105 + +/* Default gateway IP address configuration. Used in ipconfigUSE_DHCP is set to + * 0, or ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configGATEWAY_ADDR0 192 +#define configGATEWAY_ADDR1 168 +#define configGATEWAY_ADDR2 0 +#define configGATEWAY_ADDR3 1 + +/* Default DNS server configuration. OpenDNS addresses are 208.67.222.222 and + * 208.67.220.220. Used in ipconfigUSE_DHCP is set to 0, or ipconfigUSE_DHCP is + * set to 1 but a DNS server cannot be contacted.*/ +#define configDNS_SERVER_ADDR0 208 +#define configDNS_SERVER_ADDR1 67 +#define configDNS_SERVER_ADDR2 222 +#define configDNS_SERVER_ADDR3 222 + +/* Default netmask configuration. Used in ipconfigUSE_DHCP is set to 0, or + * ipconfigUSE_DHCP is set to 1 but a DNS server cannot be contacted. */ +#define configNET_MASK0 255 +#define configNET_MASK1 255 +#define configNET_MASK2 255 +#define configNET_MASK3 0 + +/* The UDP port to which print messages are sent. */ +#define configPRINT_PORT ( 15000 ) + +#define configPROFILING ( 0 ) + +/* Pseudo random number generater used by some demo tasks. */ +extern uint32_t ulRand(); +#define configRAND32() ulRand() + /* The platform that FreeRTOS is running on. */ #define configPLATFORM_NAME "WinSim" diff --git a/FreeRTOS/Test/CBMC/patches/FreeRTOSIPConfig.h b/FreeRTOS/Test/CBMC/patches/FreeRTOSIPConfig.h new file mode 100644 index 0000000000..5e4c51eee1 --- /dev/null +++ b/FreeRTOS/Test/CBMC/patches/FreeRTOSIPConfig.h @@ -0,0 +1,307 @@ +/* +FreeRTOS Kernel V10.2.0 +Copyright (C) 2017 Amazon.com, Inc. or its affiliates. All Rights Reserved. + +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the "Software"), to deal in +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of +the Software, and to permit persons to whom the Software is furnished to do so, +subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR +COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER +IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + + http://aws.amazon.com/freertos + http://www.FreeRTOS.org +*/ + + +/***************************************************************************** +* +* See the following URL for configuration information. +* http://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_IP_Configuration.html +* +*****************************************************************************/ + +#ifndef FREERTOS_IP_CONFIG_H +#define FREERTOS_IP_CONFIG_H + +/* Set to 1 to print out debug messages. If ipconfigHAS_DEBUG_PRINTF is set to + * 1 then FreeRTOS_debug_printf should be defined to the function used to print + * out the debugging messages. */ +#define ipconfigHAS_DEBUG_PRINTF 0 +#if ( ipconfigHAS_DEBUG_PRINTF == 1 ) + #define FreeRTOS_debug_printf( X ) configPRINTF( X ) +#endif + +/* Set to 1 to print out non debugging messages, for example the output of the + * FreeRTOS_netstat() command, and ping replies. If ipconfigHAS_PRINTF is set to 1 + * then FreeRTOS_printf should be set to the function used to print out the + * messages. */ +#define ipconfigHAS_PRINTF 0 +#if ( ipconfigHAS_PRINTF == 1 ) + #define FreeRTOS_printf( X ) configPRINTF( X ) +#endif + +/* Define the byte order of the target MCU (the MCU FreeRTOS+TCP is executing + * on). Valid options are pdFREERTOS_BIG_ENDIAN and pdFREERTOS_LITTLE_ENDIAN. */ +#define ipconfigBYTE_ORDER pdFREERTOS_LITTLE_ENDIAN + +/* If the network card/driver includes checksum offloading (IP/TCP/UDP checksums) + * then set ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM to 1 to prevent the software + * stack repeating the checksum calculations. */ +#define ipconfigDRIVER_INCLUDED_RX_IP_CHECKSUM 1 + +/* Several API's will block until the result is known, or the action has been + * performed, for example FreeRTOS_send() and FreeRTOS_recv(). The timeouts can be + * set per socket, using setsockopt(). If not set, the times below will be + * used as defaults. */ +#define ipconfigSOCK_DEFAULT_RECEIVE_BLOCK_TIME ( 5000 ) +#define ipconfigSOCK_DEFAULT_SEND_BLOCK_TIME ( 5000 ) + +/* Include support for DNS caching. For TCP, having a small DNS cache is very + * useful. When a cache is present, ipconfigDNS_REQUEST_ATTEMPTS can be kept low + * and also DNS may use small timeouts. If a DNS reply comes in after the DNS + * socket has been destroyed, the result will be stored into the cache. The next + * call to FreeRTOS_gethostbyname() will return immediately, without even creating + * a socket. */ +#define ipconfigUSE_DNS_CACHE ( 1 ) +#define ipconfigDNS_REQUEST_ATTEMPTS ( 2 ) + +/* The IP stack executes it its own task (although any application task can make + * use of its services through the published sockets API). ipconfigUDP_TASK_PRIORITY + * sets the priority of the task that executes the IP stack. The priority is a + * standard FreeRTOS task priority so can take any value from 0 (the lowest + * priority) to (configMAX_PRIORITIES - 1) (the highest priority). + * configMAX_PRIORITIES is a standard FreeRTOS configuration parameter defined in + * FreeRTOSConfig.h, not FreeRTOSIPConfig.h. Consideration needs to be given as to + * the priority assigned to the task executing the IP stack relative to the + * priority assigned to tasks that use the IP stack. */ +#define ipconfigIP_TASK_PRIORITY ( configMAX_PRIORITIES - 2 ) + +/* The size, in words (not bytes), of the stack allocated to the FreeRTOS+TCP + * task. This setting is less important when the FreeRTOS Win32 simulator is used + * as the Win32 simulator only stores a fixed amount of information on the task + * stack. FreeRTOS includes optional stack overflow detection, see: + * http://www.freertos.org/Stacks-and-stack-overflow-checking.html. */ +#define ipconfigIP_TASK_STACK_SIZE_WORDS ( configMINIMAL_STACK_SIZE * 5 ) + +/* ipconfigRAND32() is called by the IP stack to generate random numbers for + * things such as a DHCP transaction number or initial sequence number. Random + * number generation is performed via this macro to allow applications to use their + * own random number generation method. For example, it might be possible to + * generate a random number by sampling noise on an analogue input. */ +extern uint32_t ulRand(); +#define ipconfigRAND32() ulRand() + +/* If ipconfigUSE_NETWORK_EVENT_HOOK is set to 1 then FreeRTOS+TCP will call the + * network event hook at the appropriate times. If ipconfigUSE_NETWORK_EVENT_HOOK + * is not set to 1 then the network event hook will never be called. See: + * http://www.FreeRTOS.org/FreeRTOS-Plus/FreeRTOS_Plus_UDP/API/vApplicationIPNetworkEventHook.shtml. + */ +#define ipconfigUSE_NETWORK_EVENT_HOOK 1 + +/* Sockets have a send block time attribute. If FreeRTOS_sendto() is called but + * a network buffer cannot be obtained then the calling task is held in the Blocked + * state (so other tasks can continue to executed) until either a network buffer + * becomes available or the send block time expires. If the send block time expires + * then the send operation is aborted. The maximum allowable send block time is + * capped to the value set by ipconfigMAX_SEND_BLOCK_TIME_TICKS. Capping the + * maximum allowable send block time prevents prevents a deadlock occurring when + * all the network buffers are in use and the tasks that process (and subsequently + * free) the network buffers are themselves blocked waiting for a network buffer. + * ipconfigMAX_SEND_BLOCK_TIME_TICKS is specified in RTOS ticks. A time in + * milliseconds can be converted to a time in ticks by dividing the time in + * milliseconds by portTICK_PERIOD_MS. */ +#define ipconfigUDP_MAX_SEND_BLOCK_TIME_TICKS ( 5000 / portTICK_PERIOD_MS ) + +/* If ipconfigUSE_DHCP is 1 then FreeRTOS+TCP will attempt to retrieve an IP + * address, netmask, DNS server address and gateway address from a DHCP server. If + * ipconfigUSE_DHCP is 0 then FreeRTOS+TCP will use a static IP address. The + * stack will revert to using the static IP address even when ipconfigUSE_DHCP is + * set to 1 if a valid configuration cannot be obtained from a DHCP server for any + * reason. The static configuration used is that passed into the stack by the + * FreeRTOS_IPInit() function call. */ +#define ipconfigUSE_DHCP 1 +#define ipconfigDHCP_REGISTER_HOSTNAME 1 +#define ipconfigDHCP_USES_UNICAST 1 + +/* If ipconfigDHCP_USES_USER_HOOK is set to 1 then the application writer must + * provide an implementation of the DHCP callback function, + * xApplicationDHCPUserHook(). */ +#define ipconfigUSE_DHCP_HOOK 0 + +/* When ipconfigUSE_DHCP is set to 1, DHCP requests will be sent out at + * increasing time intervals until either a reply is received from a DHCP server + * and accepted, or the interval between transmissions reaches + * ipconfigMAXIMUM_DISCOVER_TX_PERIOD. The IP stack will revert to using the + * static IP address passed as a parameter to FreeRTOS_IPInit() if the + * re-transmission time interval reaches ipconfigMAXIMUM_DISCOVER_TX_PERIOD without + * a DHCP reply being received. */ +#define ipconfigMAXIMUM_DISCOVER_TX_PERIOD \ + ( 120000 / portTICK_PERIOD_MS ) + +/* The ARP cache is a table that maps IP addresses to MAC addresses. The IP + * stack can only send a UDP message to a remove IP address if it knowns the MAC + * address associated with the IP address, or the MAC address of the router used to + * contact the remote IP address. When a UDP message is received from a remote IP + * address the MAC address and IP address are added to the ARP cache. When a UDP + * message is sent to a remote IP address that does not already appear in the ARP + * cache then the UDP message is replaced by a ARP message that solicits the + * required MAC address information. ipconfigARP_CACHE_ENTRIES defines the maximum + * number of entries that can exist in the ARP table at any one time. */ +#define ipconfigARP_CACHE_ENTRIES 6 + +/* ARP requests that do not result in an ARP response will be re-transmitted a + * maximum of ipconfigMAX_ARP_RETRANSMISSIONS times before the ARP request is + * aborted. */ +#define ipconfigMAX_ARP_RETRANSMISSIONS ( 5 ) + +/* ipconfigMAX_ARP_AGE defines the maximum time between an entry in the ARP + * table being created or refreshed and the entry being removed because it is stale. + * New ARP requests are sent for ARP cache entries that are nearing their maximum + * age. ipconfigMAX_ARP_AGE is specified in tens of seconds, so a value of 150 is + * equal to 1500 seconds (or 25 minutes). */ +#define ipconfigMAX_ARP_AGE 150 + +/* Implementing FreeRTOS_inet_addr() necessitates the use of string handling + * routines, which are relatively large. To save code space the full + * FreeRTOS_inet_addr() implementation is made optional, and a smaller and faster + * alternative called FreeRTOS_inet_addr_quick() is provided. FreeRTOS_inet_addr() + * takes an IP in decimal dot format (for example, "192.168.0.1") as its parameter. + * FreeRTOS_inet_addr_quick() takes an IP address as four separate numerical octets + * (for example, 192, 168, 0, 1) as its parameters. If + * ipconfigINCLUDE_FULL_INET_ADDR is set to 1 then both FreeRTOS_inet_addr() and + * FreeRTOS_indet_addr_quick() are available. If ipconfigINCLUDE_FULL_INET_ADDR is + * not set to 1 then only FreeRTOS_indet_addr_quick() is available. */ +#define ipconfigINCLUDE_FULL_INET_ADDR 1 + +/* ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS defines the total number of network buffer that + * are available to the IP stack. The total number of network buffers is limited + * to ensure the total amount of RAM that can be consumed by the IP stack is capped + * to a pre-determinable value. */ +#define ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS 60 + +/* A FreeRTOS queue is used to send events from application tasks to the IP + * stack. ipconfigEVENT_QUEUE_LENGTH sets the maximum number of events that can + * be queued for processing at any one time. The event queue must be a minimum of + * 5 greater than the total number of network buffers. */ +#define ipconfigEVENT_QUEUE_LENGTH \ + ( ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS + 5 ) + +/* The address of a socket is the combination of its IP address and its port + * number. FreeRTOS_bind() is used to manually allocate a port number to a socket + * (to 'bind' the socket to a port), but manual binding is not normally necessary + * for client sockets (those sockets that initiate outgoing connections rather than + * wait for incoming connections on a known port number). If + * ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND is set to 1 then calling + * FreeRTOS_sendto() on a socket that has not yet been bound will result in the IP + * stack automatically binding the socket to a port number from the range + * socketAUTO_PORT_ALLOCATION_START_NUMBER to 0xffff. If + * ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND is set to 0 then calling FreeRTOS_sendto() + * on a socket that has not yet been bound will result in the send operation being + * aborted. */ +#define ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND 1 + +/* Defines the Time To Live (TTL) values used in outgoing UDP packets. */ +#define ipconfigUDP_TIME_TO_LIVE 128 +/* Also defined in FreeRTOSIPConfigDefaults.h. */ +#define ipconfigTCP_TIME_TO_LIVE 128 + +/* USE_TCP: Use TCP and all its features. */ +#define ipconfigUSE_TCP ( 1 ) + +/* USE_WIN: Let TCP use windowing mechanism. */ +#define ipconfigUSE_TCP_WIN ( 1 ) + +/* The MTU is the maximum number of bytes the payload of a network frame can + * contain. For normal Ethernet V2 frames the maximum MTU is 1500. Setting a + * lower value can save RAM, depending on the buffer management scheme used. If + * ipconfigCAN_FRAGMENT_OUTGOING_PACKETS is 1 then (ipconfigNETWORK_MTU - 28) must + * be divisible by 8. */ +#define ipconfigNETWORK_MTU 1200 + +/* Set ipconfigUSE_DNS to 1 to include a basic DNS client/resolver. DNS is used + * through the FreeRTOS_gethostbyname() API function. */ +#define ipconfigUSE_DNS 1 + +/* If ipconfigREPLY_TO_INCOMING_PINGS is set to 1 then the IP stack will + * generate replies to incoming ICMP echo (ping) requests. */ +#define ipconfigREPLY_TO_INCOMING_PINGS 1 + +/* If ipconfigSUPPORT_OUTGOING_PINGS is set to 1 then the + * FreeRTOS_SendPingRequest() API function is available. */ +#define ipconfigSUPPORT_OUTGOING_PINGS 0 + +/* If ipconfigSUPPORT_SELECT_FUNCTION is set to 1 then the FreeRTOS_select() + * (and associated) API function is available. */ +#define ipconfigSUPPORT_SELECT_FUNCTION 0 + +/* If ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES is set to 1 then Ethernet frames + * that are not in Ethernet II format will be dropped. This option is included for + * potential future IP stack developments. */ +#define ipconfigFILTER_OUT_NON_ETHERNET_II_FRAMES 1 + +/* If ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES is set to 1 then it is the + * responsibility of the Ethernet interface to filter out packets that are of no + * interest. If the Ethernet interface does not implement this functionality, then + * set ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES to 0 to have the IP stack + * perform the filtering instead (it is much less efficient for the stack to do it + * because the packet will already have been passed into the stack). If the + * Ethernet driver does all the necessary filtering in hardware then software + * filtering can be removed by using a value other than 1 or 0. */ +#define ipconfigETHERNET_DRIVER_FILTERS_FRAME_TYPES 1 + +/* The windows simulator cannot really simulate MAC interrupts, and needs to + * block occasionally to allow other tasks to run. */ +#define configWINDOWS_MAC_INTERRUPT_SIMULATOR_DELAY ( 20 / portTICK_PERIOD_MS ) + +/* Advanced only: in order to access 32-bit fields in the IP packets with + * 32-bit memory instructions, all packets will be stored 32-bit-aligned, + * plus 16-bits. This has to do with the contents of the IP-packets: all + * 32-bit fields are 32-bit-aligned, plus 16-bit. */ +#define ipconfigPACKET_FILLER_SIZE 2 + +/* Define the size of the pool of TCP window descriptors. On the average, each + * TCP socket will use up to 2 x 6 descriptors, meaning that it can have 2 x 6 + * outstanding packets (for Rx and Tx). When using up to 10 TP sockets + * simultaneously, one could define TCP_WIN_SEG_COUNT as 120. */ +#define ipconfigTCP_WIN_SEG_COUNT 240 + +/* Each TCP socket has a circular buffers for Rx and Tx, which have a fixed + * maximum size. Define the size of Rx buffer for TCP sockets. */ +#define ipconfigTCP_RX_BUFFER_LENGTH ( 10000 ) + +/* Define the size of Tx buffer for TCP sockets. */ +#define ipconfigTCP_TX_BUFFER_LENGTH ( 10000 ) + +/* When using call-back handlers, the driver may check if the handler points to + * real program memory (RAM or flash) or just has a random non-zero value. */ +#define ipconfigIS_VALID_PROG_ADDRESS( x ) ( ( x ) != NULL ) + +/* Include support for TCP keep-alive messages. */ +#define ipconfigTCP_KEEP_ALIVE ( 1 ) +#define ipconfigTCP_KEEP_ALIVE_INTERVAL ( 20 ) /* Seconds. */ + +/* The socket semaphore is used to unblock the MQTT task. */ +#define ipconfigSOCKET_HAS_USER_SEMAPHORE ( 0 ) + +#define ipconfigSOCKET_HAS_USER_WAKE_CALLBACK ( 1 ) +#define ipconfigUSE_CALLBACKS ( 0 ) + + +#define portINLINE __inline + +void vApplicationMQTTGetKeys( const char ** ppcRootCA, + const char ** ppcClientCert, + const char ** ppcClientPrivateKey ); + +#endif /* FREERTOS_IP_CONFIG_H */ diff --git a/FreeRTOS/Test/CBMC/patches/Makefile b/FreeRTOS/Test/CBMC/patches/Makefile index 7b98244bbf..27888e63b6 100644 --- a/FreeRTOS/Test/CBMC/patches/Makefile +++ b/FreeRTOS/Test/CBMC/patches/Makefile @@ -8,7 +8,7 @@ default: patch: if [ ! -f $(PATCHED) ]; then \ for p in *.patch; do \ - (cd ../../..; patch -p1 < cbmc/patches/$${p}) \ + (cd ../../..; patch -p1 < CBMC/patches/$${p}) \ done; \ cat > $(PATCHED) < /dev/null; \ fi diff --git a/FreeRTOS/Test/CBMC/patches/__init__.py b/FreeRTOS/Test/CBMC/patches/__init__.py old mode 100644 new mode 100755 diff --git a/FreeRTOS/Test/CBMC/patches/compute_patch.py b/FreeRTOS/Test/CBMC/patches/compute_patch.py old mode 100644 new mode 100755 diff --git a/FreeRTOS/Test/CBMC/patches/patch.py b/FreeRTOS/Test/CBMC/patches/patch.py index e75dafbcb1..c2c0883a3c 100755 --- a/FreeRTOS/Test/CBMC/patches/patch.py +++ b/FreeRTOS/Test/CBMC/patches/patch.py @@ -16,8 +16,8 @@ def patch(): failed_patches = [] for tmpfile in glob(os.path.join(PATCHES_DIR, "*.patch")): print("patch", tmpfile) - result = subprocess.run(["git", "apply", "--ignore-whitespace", tmpfile], - cwd=os.path.join("..", "..", "..")) + result = subprocess.run(["git", "apply", "--ignore-space-change", "--ignore-whitespace", tmpfile], + cwd=os.path.join("..", "..", "..", "..")) if result.returncode: failed_patches.append(tmpfile) logging.error("patching failed: %s", tmpfile) diff --git a/FreeRTOS/Test/CBMC/patches/patches_constants.py b/FreeRTOS/Test/CBMC/patches/patches_constants.py old mode 100644 new mode 100755 index 171e504ebc..71f0b05371 --- a/FreeRTOS/Test/CBMC/patches/patches_constants.py +++ b/FreeRTOS/Test/CBMC/patches/patches_constants.py @@ -38,4 +38,5 @@ absolute_prefix = os.path.abspath(os.path.join(PATCHES_DIR, *shared_prefix)) absolute_prefix_port = os.path.abspath(os.path.join(PATCHES_DIR, *shared_prefix_port)) HEADERS = [os.path.join(absolute_prefix, "FreeRTOSConfig.h"), + os.path.join(absolute_prefix, "FreeRTOSIPConfig.h"), os.path.join(absolute_prefix_port, "portmacro.h")] diff --git a/FreeRTOS/Test/CBMC/patches/unpatch.py b/FreeRTOS/Test/CBMC/patches/unpatch.py index 689b7b05c8..2162971fdc 100755 --- a/FreeRTOS/Test/CBMC/patches/unpatch.py +++ b/FreeRTOS/Test/CBMC/patches/unpatch.py @@ -36,7 +36,7 @@ except FileNotFoundError: sys.exit(0) for tmpfile in glob(os.path.join(PATCHES_DIR, "*.patch")): print("unpatch", tmpfile) - result = subprocess.run(["git", "apply", "-R", "--ignore-whitespace", tmpfile], - cwd=os.path.join("..", "..", "..")) + result = subprocess.run(["git", "apply", "-R", "--ignore-space-change", "--ignore-whitespace", tmpfile], + cwd=os.path.join("..", "..", "..", "..")) if result.returncode: print("Unpatching failed: {}".format(tmpfile)) diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c new file mode 100644 index 0000000000..5237835649 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c @@ -0,0 +1,22 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "list.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +//We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. +//This is the mock to mimic the correct expected bahvior. If this allocation fails, this might invalidate the proof. +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + NetworkBufferDescriptor_t *pxNetworkBuffer = (NetworkBufferDescriptor_t *) malloc(sizeof(NetworkBufferDescriptor_t)); + pxNetworkBuffer->pucEthernetBuffer = malloc(xRequestedSizeBytes); + pxNetworkBuffer->xDataLength = xRequestedSizeBytes; + return pxNetworkBuffer; +} + +void harness() +{ + vARPAgeCache(); +} \ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json b/FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json new file mode 100644 index 0000000000..83c351d70a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/Makefile.json @@ -0,0 +1,18 @@ +{ + "ENTRY": "ARPAgeCache", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPAgeCache.0:7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/README.md b/FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/README.md new file mode 100644 index 0000000000..3352f80964 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPAgeCache/README.md @@ -0,0 +1,2 @@ +Assuming that xNetworkInterfaceOutput is memory safe, +this harness proves the memory safety of the vARPAgeCache function. diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c new file mode 100644 index 0000000000..3ec9500cc3 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c @@ -0,0 +1,28 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + /* + * The assumption made here is that the buffer pointed by pucEthernerBuffer + * is at least allocated to sizeof(ARPPacket_t) size but eventually a even larger buffer. + * This is not checked inside vARPGenerateRequestPacket. + */ + uint8_t ucBUFFER_SIZE; + __CPROVER_assume( ucBUFFER_SIZE >= sizeof(ARPPacket_t) && ucBUFFER_SIZE < 2 * sizeof(ARPPacket_t) ); + void *xBuffer = malloc(ucBUFFER_SIZE); + + NetworkBufferDescriptor_t xNetworkBuffer2; + xNetworkBuffer2.pucEthernetBuffer = xBuffer; + xNetworkBuffer2.xDataLength = ucBUFFER_SIZE; + + /* vARPGenerateRequestPacket asserts buffer has room for a packet */ + __CPROVER_assume( xNetworkBuffer2.xDataLength >= sizeof(ARPPacket_t) ); + vARPGenerateRequestPacket( &xNetworkBuffer2 ); +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json new file mode 100644 index 0000000000..65c3524893 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/Makefile.json @@ -0,0 +1,15 @@ +{ + "ENTRY": "ARPGenerateRequestPacket", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md new file mode 100644 index 0000000000..f8fdcc97dd --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md @@ -0,0 +1,3 @@ +Given that the pointer target of xNetworkDescriptor.pucEthernetBuffer is allocated +to the size claimed in xNetworkDescriptor.xDataLength, +this harness proves the memory safety of ARPGenerateRequestPacket. \ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c new file mode 100644 index 0000000000..bf188efa1a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c @@ -0,0 +1,17 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + + +void harness() +{ + uint32_t ulIPAddress; + MACAddress_t xMACAddress; + + eARPGetCacheEntry( &ulIPAddress, &xMACAddress ); +} \ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json new file mode 100644 index 0000000000..ecc95a87fa --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/Configurations.json @@ -0,0 +1,41 @@ +{ + "ENTRY": "ARPGetCacheEntry", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvCacheLookup.0:7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + { + "ARPGetCacheEntry_default":[ + "ipconfigARP_STORES_REMOTE_ADDRESSES=0", + "ipconfigUSE_LLMNR=0" + ] + }, + { + "ARPGetCacheEntry_LLMNR": [ + "ipconfigARP_STORES_REMOTE_ADDRESSES=0", + "ipconfigUSE_LLMNR=1" + ] + }, + { + "ARPGetCacheEntry_STORE_REMOTE": [ + "ipconfigARP_STORES_REMOTE_ADDRESSES=1", + "ipconfigUSE_LLMNR=0" + ] + }, + { + "ARPGetCacheEntry_REMOTE_LLMNR": [ + "ipconfigARP_STORES_REMOTE_ADDRESSES=1", + "ipconfigUSE_LLMNR=1" + ] + } + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md new file mode 100644 index 0000000000..03e987ebd6 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntry/README.md @@ -0,0 +1,4 @@ +The combined proofs in the subdirectories prove that ARPGetCacheEntry +is memory safe for all possible combinations of ipconfigARP_STORES_REMOTE_ADDRESSES +and ipconfigUSE_LLMNR. These are the only configuration +parameters used inside the ARPGetCacheEntry. diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c new file mode 100644 index 0000000000..442b1df6bc --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c @@ -0,0 +1,14 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +void harness(){ + MACAddress_t xMACAddress; + uint32_t ulIPAddress; + eARPGetCacheEntryByMac( &xMACAddress, &ulIPAddress ); +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json new file mode 100644 index 0000000000..0f589a8e25 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json @@ -0,0 +1,17 @@ +{ + "ENTRY": "ARPGetCacheEntryByMac", + "CBMCFLAGS": + [ + "--unwind 7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + "ipconfigUSE_ARP_REVERSED_LOOKUP=1", "ipconfigARP_CACHE_ENTRIES=6" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md new file mode 100644 index 0000000000..77c17e2e9d --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPGetCacheEntryByMac/README.md @@ -0,0 +1,4 @@ +ARPGetCacheEntryByMac is memory safe, +if it is enabled. + +ARPGetCacheEntryByMac does not use multiple configurations internally. diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c new file mode 100644 index 0000000000..f2d8e61aef --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c @@ -0,0 +1,15 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + ARPPacket_t xARPFrame; + + eARPProcessPacket( &xARPFrame ); +} \ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json b/FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json new file mode 100644 index 0000000000..48d5d83c98 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/Configurations.json @@ -0,0 +1,19 @@ +{ + "ENTRY": "ARPProcessPacket", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + {"disableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=0"]}, + {"enableClashDetection": ["ipconfigARP_USE_CLASH_DETECTION=1"]} + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md b/FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md new file mode 100644 index 0000000000..0197851b15 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPProcessPacket/README.md @@ -0,0 +1,4 @@ +The proofs in the subdirectories show that +ARPProcessPacket is memory safe independent +of the configuration value of +ipconfigARP_USE_CLASH_DETECTION. \ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c b/FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c new file mode 100644 index 0000000000..6664d3cd04 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c @@ -0,0 +1,15 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + MACAddress_t xMACAddress; + uint32_t ulIPAddress; + vARPRefreshCacheEntry( &xMACAddress, ulIPAddress ); + vARPRefreshCacheEntry( NULL, ulIPAddress ); +} \ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json b/FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json new file mode 100644 index 0000000000..6cde60a51c --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/Configurations.json @@ -0,0 +1,19 @@ +{ + "ENTRY": "ARPRefreshCacheEntry", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + {"NOT_STORE_REMOTE":["ipconfigARP_STORES_REMOTE_ADDRESSES=0"]}, + {"STORE_REMOTE":["ipconfigARP_STORES_REMOTE_ADDRESSES=1"]} + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md b/FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md new file mode 100644 index 0000000000..0f84300cf7 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPRefreshCacheEntry/README.md @@ -0,0 +1,4 @@ +The proofs in this directory guarantee together that +ARPRefreshCacheEntry is memory safe independent +of the configuration value of +ipconfigARP_STORES_REMOTE_ADDRESSES. diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c b/FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c new file mode 100644 index 0000000000..fd02b10a22 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/ARPSendGratuitous_harness.c @@ -0,0 +1,13 @@ +// /* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_ARP.h" + + +void harness() +{ + vARPSendGratuitous(); +} \ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json b/FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json new file mode 100644 index 0000000000..1f9616ef89 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/Makefile.json @@ -0,0 +1,18 @@ +{ + "ENTRY": "ARPSendGratuitous", + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md b/FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md new file mode 100644 index 0000000000..5bb155221f --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARPSendGratuitous/README.md @@ -0,0 +1,6 @@ +Abstracting xQueueGenericSend away +and including tasks.c and FreeRTOS_IP.c: +The ARPSendGratutious function is memory safe, +if xQueueGenericSend is memory safe. + +queue.c is not compiled into the proof binary. \ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c new file mode 100644 index 0000000000..9577201338 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c @@ -0,0 +1,13 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + FreeRTOS_ClearARP(); +} + diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json new file mode 100644 index 0000000000..332106c4e6 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json @@ -0,0 +1,15 @@ +{ + "ENTRY": "ClearARP", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md new file mode 100644 index 0000000000..2447722c9a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_ClearARP/README.md @@ -0,0 +1,2 @@ +This proof demonstrates the memory safety of the ClearARP function in the FreeRTOS_ARP.c file. +No restrictions are made. \ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json new file mode 100644 index 0000000000..13792bb685 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json @@ -0,0 +1,57 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Permission is hereby granted, free of charge, to any person +# obtaining a copy of this software and associated documentation +# files (the "Software"), to deal in the Software without +# restriction, including without limitation the rights to use, copy, +# modify, merge, publish, distribute, sublicense, and/or sell copies +# of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be +# included in all copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +# MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +# NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS +# BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN +# ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +# CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. +# +# http://aws.amazon.com/freertos +# http://www.FreeRTOS.org +# + +{ + "ENTRY": "OutputARPRequest", + "CBMCFLAGS": + [ + "--unwind 20" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + #That is the minimal required size for an ARPPacket_t plus offset in the buffer. + "MINIMUM_PACKET_BYTES": 50, + "DEF": + [ + { + "CBMC_PROOF_ASSUMPTION_HOLDS_Packet_bytes": [ + "CBMC_PROOF_ASSUMPTION_HOLDS=1", + "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}" + ] + }, + { + "CBMC_PROOF_ASSUMPTION_HOLDS_no_packet_bytes": ["CBMC_PROOF_ASSUMPTION_HOLDS=1"] + }, + { + "CBMC_PROOF_ASSUMPTION_DOES_NOT_HOLD": ["CBMC_PROOF_ASSUMPTION_HOLDS=0"] + } + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c new file mode 100644 index 0000000000..472f6b1e10 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c @@ -0,0 +1,76 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" + + +ARPPacket_t xARPPacket; +NetworkBufferDescriptor_t xNetworkBuffer; + +/* STUB! + * We assume that the pxGetNetworkBufferWithDescriptor function is + * implemented correctly and returns a valid data structure. + * This is the mock to mimic the expected behavior. + * If this allocation fails, this might invalidate the proof. + * FreeRTOS_OutputARPRequest calls pxGetNetworkBufferWithDescriptor + * to get a NetworkBufferDescriptor. Then it calls vARPGenerateRequestPacket + * passing this buffer along in the function call. vARPGenerateRequestPacket + * casts the pointer xNetworkBuffer.pucEthernetBuffer into an ARPPacket_t pointer + * and writes a complete ARPPacket to it. Therefore the buffer has to be at least of the size + * of an ARPPacket to gurantee memory safety. + */ +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + #ifdef CBMC_PROOF_ASSUMPTION_HOLDS + #ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES + xNetworkBuffer.pucEthernetBuffer = malloc(ipconfigETHERNET_MINIMUM_PACKET_BYTES); + #else + xNetworkBuffer.pucEthernetBuffer = malloc(xRequestedSizeBytes); + #endif + #else + uint32_t malloc_size; + __CPROVER_assert(!__CPROVER_overflow_mult(2, xRequestedSizeBytes)); + __CPROVER_assume(malloc_size > 0 && malloc_size < 2 * xRequestedSizeBytes); + xNetworkBuffer.pucEthernetBuffer = malloc(malloc_size); + #endif + xNetworkBuffer.xDataLength = xRequestedSizeBytes; + return &xNetworkBuffer; +} + + +void harness() +{ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md new file mode 100644 index 0000000000..8a868dda10 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/README.md @@ -0,0 +1,29 @@ +This is the memory safety proof for FreeRTOS_OutputARPRequest. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* xNetworkInterfaceOutput + +This proof checks FreeRTOS_OutputARPRequest in multiple configuration: + +* The config_CBMC_PROOF_ASSUMPTION_HOLDS_no_packet_bytes proof + guarantees that for a buffer allocated to xDataLength, + the code executed by the FreeRTOS_OutputARPRequest function + call of FreeRTOS_ARP.c is memory safe. +* If the ipconfigETHERNET_MINIMUM_PACKET_BYTES is set and the + buffer allocated by pxGetNetworkBufferWithDescriptor allocates + a buffer of at least ipconfigETHERNET_MINIMUM_PACKET_BYTES, + the config_CBMC_PROOF_ASSUMPTION_HOLDS_Packet_bytes proof + guarantees that the code executed by the + FreeRTOS_OutputARPRequest function call + of FreeRTOS_ARP.c is memory safe. +* The third configuration in the subdirectory + config_CBMC_PROOF_ASSUMPTION_DOES_NOT_HOLD demonstrates + that the code is not memory safe, if the allocation + code violates our assumption. +* All proofs mock the pxGetNetworkBufferWithDescriptor + function for modelling the assumptions about the + buffer management layer. diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c new file mode 100644 index 0000000000..4975d66ee6 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c @@ -0,0 +1,14 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOSIPConfig.h" +#include "FreeRTOS_ARP.h" + +void harness() +{ + FreeRTOS_PrintARPCache(); +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json new file mode 100644 index 0000000000..6588b10d9b --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json @@ -0,0 +1,17 @@ +{ + "ENTRY": "FreeRTOS_PrintARPCache", + "CBMCFLAGS": + [ + "--unwind 7", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto" + ], + "DEF": + [ + "ipconfigARP_CACHE_ENTRIES=6" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md new file mode 100644 index 0000000000..2c44908cd3 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_FreeRTOS_PrintARPCache/README.md @@ -0,0 +1,4 @@ +FreeRTOS_PrintARPCache_harness.c is memory safe, +assuming vLoggingPrintf is correct and memory safe. + +FreeRTOS_PrintARPCache does not use multiple configurations. diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json new file mode 100644 index 0000000000..ed1a2aca89 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json @@ -0,0 +1,47 @@ +{ + "ENTRY": "OutputARPRequest", + "MINIMUM_PACKET_BYTES": 50, + "CBMCFLAGS": + [ + "--unwind {MINIMUM_PACKET_BYTES}", + "--unwindset xNetworkBuffersInitialise.0:3,xNetworkBuffersInitialise.1:3,vListInsert.0:3,pxGetNetworkBufferWithDescriptor.0:3,pxGetNetworkBufferWithDescriptor.1:3,vNetworkInterfaceAllocateRAMToBuffers.0:3" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement/BufferAllocation_1.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Source/queue.goto" + ], + "DEF": + [ + { + "minimal_configuration": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=0" + ] + }, + { + "minimal_configuration_minimal_packet_size": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}" + ] + }, + { + "minimal_configuration_linked_rx_messages": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=1" + ] + } + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c new file mode 100644 index 0000000000..3dae34a341 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c @@ -0,0 +1,71 @@ +/* This harness is linked against + * libraries/freertos_plus/standard/freertos_plus_tcp/source/portable/BufferManagement/BufferAllocation_1.goto + */ +#include +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#if( ipconfigUSE_LLMNR == 1 ) + #include "FreeRTOS_DNS.h" +#endif /* ipconfigUSE_LLMNR */ +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" + +void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] ){ + for(int x = 0; x < ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS; x++){ + NetworkBufferDescriptor_t *current = &pxNetworkBuffers[x]; + #ifdef ipconfigETHERNET_MINIMUM_PACKET_BYTES + current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t) + (ipconfigETHERNET_MINIMUM_PACKET_BYTES- sizeof(ARPPacket_t))); + #else + current->pucEthernetBuffer = malloc(sizeof(ARPPacket_t)); + #endif + current->xDataLength = sizeof(ARPPacket_t); + } +} + +/* The code expects that the Semaphore creation relying on pvPortMalloc + is successful. This is checked by an assert statement, that gets + triggered when the allocation fails. Nevertheless, the code is perfectly + guarded against a failing Semaphore allocation. To make the assert pass, + it is assumed for now, that pvPortMalloc doesn't fail. Using a model allowing + failures of the allocation might be possible + after removing the assert in l.105 of BufferAllocation_1.c, from a memory + safety point of view. */ +void *pvPortMalloc( size_t xWantedSize ){ + return malloc(xWantedSize); +} + +/* + * This function is implemented by a third party. + * After looking through a couple of samples in the demos folder, it seems + * like the only shared contract is that you want to add the if statement + * for releasing the buffer to the end. Apart from that, it is up to the vendor, + * how to write this code out to the network. + */ +BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor, BaseType_t bReleaseAfterSend ){ + if( bReleaseAfterSend != pdFALSE ) + { + vReleaseNetworkBufferAndDescriptor( pxDescriptor ); + } +} + +void harness() +{ + BaseType_t xRes = xNetworkBuffersInitialise(); + if(xRes == pdPASS){ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md new file mode 100644 index 0000000000..ea5eac78d4 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md @@ -0,0 +1,27 @@ +This is the memory safety proof for ```FreeRTOS_OutputARPRequest``` +method combined with the BufferAllocation_1.c allocation strategy. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* vPortEnterCritical +* vPortExitCritical +* vPortGenerateSimulatedInterrupt +* vAssertCalled +* xTaskGetSchedulerState +* pvTaskIncrementMutexHeldCount +* xTaskRemoveFromEventList +* xTaskPriorityDisinherit + +This proof checks ```FreeRTOS_OutputARPRequest``` in multiple configurations. +All assume the memory safety of vNetworkInterfaceAllocateRAMToBuffers. +* The ```config_minimal_configuration``` proof sets + ```ipconfigUSE_LINKED_RX_MESSAGES=0```. +* The ```config_minimal_configuration_linked_rx_messages``` proof sets + ```ipconfigUSE_LINKED_RX_MESSAGES=1```. +* The ```minimal_configuration_minimal_packet_size``` proof sets + ```ipconfigETHERNET_MINIMUM_PACKET_BYTES``` to 50. + +All harnesses include the queue.c file, but test only for the happy path. diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json new file mode 100644 index 0000000000..fb5dd4be2c --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json @@ -0,0 +1,48 @@ +{ + "ENTRY": "OutputARPRequest", + "MINIMUM_PACKET_BYTES": 50, + "CBMCFLAGS": + [ + "--unwind {MINIMUM_PACKET_BYTES}", + "--unwindset xNetworkBuffersInitialise.0:3,xNetworkBuffersInitialise.1:3,vListInsert.0:3,pxGetNetworkBufferWithDescriptor.0:3,pxGetNetworkBufferWithDescriptor.1:3,vNetworkInterfaceAllocateRAMToBuffers.0:3" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement/BufferAllocation_2.goto", + "$(FREERTOS)/Source/list.goto", + "$(FREERTOS)/Source/queue.goto" + ], + "DEF": + [ + { + "minimal_configuration": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=0" + ] + }, + { + "minimal_configuration_minimal_packet_size": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigETHERNET_MINIMUM_PACKET_BYTES={MINIMUM_PACKET_BYTES}", + "ipconfigUSE_TCP=1" + ] + }, + { + "minimal_configuration_linked_rx_messages": + [ + "ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS=2", + "configUSE_TRACE_FACILITY=0", + "configGENERATE_RUN_TIME_STATS=0", + "ipconfigUSE_LINKED_RX_MESSAGES=1" + ] + } + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c new file mode 100644 index 0000000000..c047a27608 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c @@ -0,0 +1,54 @@ +/* This harness is linked against + * libraries/freertos_plus/standard/freertos_plus_tcp/source/portable/BufferManagement/BufferAllocation_2.goto + */ +#include +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DHCP.h" +#if( ipconfigUSE_LLMNR == 1 ) + #include "FreeRTOS_DNS.h" +#endif /* ipconfigUSE_LLMNR */ +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" + +void *pvPortMalloc( size_t xWantedSize ){ + return malloc(xWantedSize); +} + + +void vPortFree( void *pv ){ + free(pv); +} + +/* + * This function function writes a buffer to the network. We stub it + * out here, and assume it has no side effects relevant to memory safety. + */ +BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor, BaseType_t bReleaseAfterSend ){ + if( bReleaseAfterSend != pdFALSE ) + { + vReleaseNetworkBufferAndDescriptor( pxDescriptor ); + } +} + +void harness() +{ + BaseType_t xRes = xNetworkBuffersInitialise(); + if(xRes == pdPASS){ + uint32_t ulIPAddress; + FreeRTOS_OutputARPRequest( ulIPAddress ); + } +} + diff --git a/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md new file mode 100644 index 0000000000..5d509a7e83 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md @@ -0,0 +1,49 @@ +This is the memory safety proof for FreeRTOS_OutputARPRequest +method combined with the BufferAllocation_2.c allocation strategy. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* vPortEnterCritical +* vPortExitCritical +* vPortGenerateSimulatedInterrupt +* vAssertCalled +* xTaskGetSchedulerState +* pvTaskIncrementMutexHeldCount +* xTaskRemoveFromEventList +* xTaskPriorityDisinherit + +* pvPortMalloc +* pvPortFree +* xNetworkInterfaceOutput +* vNetworkInterfaceAllocateRAMToBuffers + +This proof disables the tracing library in the header. + +This proof checks FreeRTOS_OutputARPRequest in multiple configuration: + +* The proof in the directory config_minimal_configuration guarantees + that the implementation and interaction between + FreeRTOS_OutputARPRequest and + FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c + are memory save. This proof depends entirely of the implementation + correctness of vNetworkInterfaceAllocateRAMToBuffers. +* The proof in directory minimal_configuration_minimal_packet_size + guarantees that using + FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c + along with the ipconfigETHERNET_MINIMUM_PACKET_BYTES is memory save + as long as TCP is enabled ( ipconfigUSE_TCP 1 ) and + ipconfigETHERNET_MINIMUM_PACKET_BYTES < sizeof( TCPPacket_t ). +* The directory minimal_configuration_minimal_packet_size_no_tcp + reminds that ipconfigETHERNET_MINIMUM_PACKET_BYTES must not be used + if TCP is disabled ( ipconfigUSE_TCP 1 ) along with the + FreeRTOS-Plus-TCP/source/portable/BufferManagement/BufferAllocation_2.c + allocator. +* The proof in directory + config_minimal_configuration_linked_rx_messages guarantees that the + ipconfigUSE_LINKED_RX_MESSAGES define does not interfere with the + memory safety claim. + +All harnesses include the queue.c file, but test only for the happy path. diff --git a/FreeRTOS/Test/CBMC/proofs/CMakeLists.txt b/FreeRTOS/Test/CBMC/proofs/CMakeLists.txt index 2ecda74ab4..aaa2e3c8a6 100644 --- a/FreeRTOS/Test/CBMC/proofs/CMakeLists.txt +++ b/FreeRTOS/Test/CBMC/proofs/CMakeLists.txt @@ -16,6 +16,9 @@ list(APPEND cbmc_compile_definitions list(APPEND cbmc_compile_includes ${CMAKE_SOURCE_DIR}/Source/include ${CMAKE_SOURCE_DIR}/Source/portable/MSVC-MingW + ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement + ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include + ${CMAKE_SOURCE_DIR}/Source/../../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/Compiler/MSVC ${cbmc_dir}/include ${cbmc_dir}/windows ) diff --git a/FreeRTOS/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c b/FreeRTOS/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c new file mode 100644 index 0000000000..cd8e78c969 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/CheckOptions/CheckOptions_harness.c @@ -0,0 +1,113 @@ +/* Standard includes. */ +#include +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_TCP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_TCP_WIN.h" + +#include "cbmc.h" + +void prvCheckOptions( FreeRTOS_Socket_t *pxSocket, + NetworkBufferDescriptor_t *pxNetworkBuffer ); + +// Used in specification and abstraction of CheckOptions inner and outer loops +// Given unconstrained values in harness +size_t buffer_size; +uint8_t *EthernetBuffer; + +// Abstraction of CheckOptions outer loop used in proof of CheckOptions +// Loop variables passed by reference: VAL(var) is (*var). +BaseType_t prvSingleStepTCPHeaderOptions( const unsigned char ** const ppucPtr, + const unsigned char ** const ppucLast, + FreeRTOS_Socket_t ** const ppxSocket, + TCPWindow_t ** const ppxTCPWindow) +{ + // CBMC pointer model (obviously true) + __CPROVER_assume(buffer_size < CBMC_MAX_OBJECT_SIZE); + + // Preconditions + + // pucPtr is a valid pointer + __CPROVER_assert(EthernetBuffer <= OBJ(ppucPtr) && + OBJ(ppucPtr) < EthernetBuffer + buffer_size, + "pucPtr is a valid pointer"); + // pucLast is a valid pointer (or one past) + __CPROVER_assert(EthernetBuffer <= OBJ(ppucLast) && + OBJ(ppucLast) <= EthernetBuffer + buffer_size, + "pucLast is a valid pointer"); + // pucPtr is before pucLast + __CPROVER_assert(OBJ(ppucPtr) < OBJ(ppucLast), + "pucPtr < pucLast"); + + // Record initial values + SAVE_OLDOBJ(ppucPtr, unsigned char *); + SAVE_OLDOBJ(ppucLast, unsigned char *); + + // Model loop body + size_t offset; + BaseType_t rc; + OBJ(ppucPtr) += offset; + + // Postconditions + + // rc is boolean + __CPROVER_assume(rc == pdTRUE || rc == pdFALSE); + // pucPtr advanced + __CPROVER_assume(rc == pdFALSE || OLDOBJ(ppucPtr) < OBJ(ppucPtr)); + // pucLast unchanged + __CPROVER_assume(OBJ(ppucLast) == OLDOBJ(ppucLast)); + // pucPtr <= pucLast + __CPROVER_assume(OBJ(ppucPtr) <= OBJ(ppucLast)); + + return rc; +} + +// Proof of CheckOptions +void harness() +{ + // Buffer can be any buffer of size at most BUFFER_SIZE + size_t offset; + uint8_t buffer[BUFFER_SIZE]; + buffer_size = BUFFER_SIZE - offset; + EthernetBuffer = buffer + offset; + + // pxSocket can be any socket + FreeRTOS_Socket_t pxSocket; + + // pxNetworkBuffer can be any buffer descriptor with any buffer + NetworkBufferDescriptor_t pxNetworkBuffer; + pxNetworkBuffer.pucEthernetBuffer = EthernetBuffer; + pxNetworkBuffer.xDataLength = buffer_size; + + //////////////////////////////////////////////////////////////// + // Specification and proof of CheckOptions + + // CBMC pointer model (obviously true) + __CPROVER_assume(buffer_size < CBMC_MAX_OBJECT_SIZE); + + // Buffer overflow on pathologically small buffers + // Must be big enough to hold pxTCPPacket and pxTCPHeader + __CPROVER_assume(buffer_size > 47); + + // EthernetBuffer is a valid pointer (or one past when buffer_size==0) + __CPROVER_assume(buffer <= EthernetBuffer && + EthernetBuffer <= buffer + BUFFER_SIZE); + + // Loop variables passed by reference + prvCheckOptions(&pxSocket, &pxNetworkBuffer); +} diff --git a/FreeRTOS/Test/CBMC/proofs/CheckOptions/Makefile.json b/FreeRTOS/Test/CBMC/proofs/CheckOptions/Makefile.json new file mode 100644 index 0000000000..185d6fca98 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/CheckOptions/Makefile.json @@ -0,0 +1,20 @@ +{ + "ENTRY": "CheckOptions", + "CBMCFLAGS": "--unwind 1 --unwindset prvCheckOptions.0:41", + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Stream_Buffer.goto", + "$(FREERTOS)/Source/tasks.goto", + "$(FREERTOS)/Source/list.goto" + ], + "ABSTRACTIONS": "", + "BUFFER_SIZE": 100, + "UNWIND_GOTO": 0, + "DEF": + [ + "BUFFER_SIZE={BUFFER_SIZE}" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c b/FreeRTOS/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c new file mode 100644 index 0000000000..74c120e93a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/CheckOptionsInner/CheckOptionsInner_harness.c @@ -0,0 +1,105 @@ +/* Standard includes. */ +#include +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_TCP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_TCP_WIN.h" + +#include "cbmc.h" + +void prvSkipPastRemainingOptions( const unsigned char ** const ppucPtr, + FreeRTOS_Socket_t ** const ppxSocket, + unsigned char * const pucLen ); + +// Given unconstrained values in harness +size_t buffer_size; +uint8_t *EthernetBuffer; + +void harness() +{ + // Buffer can be any buffer of size at most BUFFER_SIZE + size_t offset; + uint8_t buffer[BUFFER_SIZE]; + buffer_size = BUFFER_SIZE - offset; + EthernetBuffer = buffer + offset; + + // pucPtr can be any pointer into buffer + size_t pucPtr_offset; + unsigned char *pucPtr = EthernetBuffer + pucPtr_offset; + + // ucLen can be any byte + unsigned char ucLen; + + // pxSocket can be any socket with some initialized values + FreeRTOS_Socket_t xSocket; + FreeRTOS_Socket_t *pxSocket = &xSocket; + + extern List_t xSegmentList; + vListInitialise(&xSocket.u.xTCP.xTCPWindow.xWaitQueue); + vListInitialise(&xSocket.u.xTCP.xTCPWindow.xTxSegments); + vListInitialise(&xSocket.u.xTCP.xTCPWindow.xPriorityQueue); + vListInitialise(&xSegmentList); + StreamBuffer_t txStreamBuffer; + xSocket.u.xTCP.txStream=&txStreamBuffer; + + // A singleton list + TCPSegment_t segment_w; + vListInitialiseItem(&segment_w.xQueueItem); + vListInitialiseItem(&segment_w.xListItem); + listSET_LIST_ITEM_OWNER(&segment_w.xQueueItem, (void *) &segment_w); + vListInsertEnd(&xSocket.u.xTCP.xTCPWindow.xWaitQueue, &segment_w.xQueueItem); + + // A singleton list + TCPSegment_t segment_t; + vListInitialiseItem(&segment_t.xQueueItem); + vListInitialiseItem(&segment_t.xListItem); + listSET_LIST_ITEM_OWNER(&segment_t.xQueueItem, (void *) &segment_t); + vListInsertEnd(&xSocket.u.xTCP.xTCPWindow.xTxSegments, &segment_t.xQueueItem); + + //////////////////////////////////////////////////////////////// + // Specification and proof of CheckOptions inner loop + + // CBMC pointer model (obviously true) + __CPROVER_assume(buffer_size < CBMC_MAX_OBJECT_SIZE); + + // Preconditions + + // pucPtr is a valid pointer + __CPROVER_assume(EthernetBuffer <= pucPtr && + pucPtr < EthernetBuffer + buffer_size); + // pucPtr + 8 is a valid pointer (xBytesRemaining > ucLen) + __CPROVER_assume(EthernetBuffer <= pucPtr + 8 && + pucPtr + 8 <= EthernetBuffer + buffer_size); + // ucLen >= 8 (while loop condition) + __CPROVER_assume(ucLen >= 8); + + // Record initial values + SAVE_OLDVAL(pucPtr, unsigned char *); + SAVE_OLDVAL(ucLen, unsigned char); + + // Loop variables passed by reference + prvSkipPastRemainingOptions(&pucPtr, &pxSocket, &ucLen); + + // Postconditions + + __CPROVER_assert(pucPtr == OLDVAL(pucPtr) + 8, "pucPtr advanced"); + __CPROVER_assert(ucLen == OLDVAL(ucLen) - 8, "ucLen decremented"); + __CPROVER_assert(EthernetBuffer <= pucPtr && + pucPtr <= EthernetBuffer + buffer_size, + "pucPtr a valid pointer"); +} diff --git a/FreeRTOS/Test/CBMC/proofs/CheckOptionsInner/Makefile.json b/FreeRTOS/Test/CBMC/proofs/CheckOptionsInner/Makefile.json new file mode 100644 index 0000000000..b5b2118b6a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/CheckOptionsInner/Makefile.json @@ -0,0 +1,21 @@ +{ + "ENTRY": "CheckOptionsInner", + "BUFFER_SIZE": 100, + "CBMCFLAGS": [ + "--unwind 1", + "--unwindset prvTCPWindowTxCheckAck.1:2,prvTCPWindowFastRetransmit.2:2" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Stream_Buffer.goto", + "$(FREERTOS)/Source/tasks.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": + [ + "BUFFER_SIZE={BUFFER_SIZE}" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c b/FreeRTOS/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c new file mode 100644 index 0000000000..359546d8a7 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c @@ -0,0 +1,123 @@ +/* Standard includes. */ +#include +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_TCP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_TCP_WIN.h" + +#include "cbmc.h" + +BaseType_t prvSingleStepTCPHeaderOptions( const unsigned char ** const ppucPtr, + const unsigned char ** const ppucLast, + FreeRTOS_Socket_t ** const ppxSocket, + TCPWindow_t ** const ppxTCPWindow); + +// Given unconstrained values in harness +size_t buffer_size; +uint8_t *EthernetBuffer; + +void prvSkipPastRemainingOptions( const unsigned char ** const ppucPtr, + FreeRTOS_Socket_t ** const ppxSocket, + unsigned char * const pucLen ) +{ + // Preconditions + + // pucPtr is a valid pointer + __CPROVER_assert(EthernetBuffer <= OBJ(ppucPtr) && + OBJ(ppucPtr) < EthernetBuffer + buffer_size, + "pucPtr is a valid pointer"); + // pucPtr + 8 is a valid pointer + __CPROVER_assert(EthernetBuffer <= OBJ(ppucPtr) + 8 && + OBJ(ppucPtr) + 8 <= EthernetBuffer + buffer_size, + "pucPtr+8 is a valid pointer"); + // len >= 8 + __CPROVER_assert(OBJ(pucLen) >= 8, "len >= 8"); + + // Record initial values + SAVE_OLDOBJ(ppucPtr, unsigned char *); + SAVE_OLDOBJ(pucLen, unsigned char); + + // Model loop body + OBJ(ppucPtr) += 8; + OBJ(pucLen) -= 8; + + // Postconditions + + __CPROVER_assume(OBJ(ppucPtr) == OLDOBJ(ppucPtr) + 8); + __CPROVER_assume(OBJ(pucLen) == OLDOBJ(pucLen) - 8); + __CPROVER_assume(EthernetBuffer <= OBJ(ppucPtr) && + OBJ(ppucPtr) <= EthernetBuffer + buffer_size); +} + +// Proof of CheckOptions outer loop +void harness() +{ + // Buffer can be any buffer of size at most BUFFER_SIZE + size_t offset; + uint8_t buffer[BUFFER_SIZE]; + buffer_size = BUFFER_SIZE - offset; + EthernetBuffer = buffer + offset; + + // pucPtr and pucLast can be any pointers into buffer + size_t pucPtr_offset; + size_t pucLast_offset; + unsigned char *pucPtr = EthernetBuffer + pucPtr_offset; + unsigned char *pucLast = EthernetBuffer + pucLast_offset; + + // uxNewMSS can by any byte + UBaseType_t uxNewMSS; + + // pxSocket can be any socket + FreeRTOS_Socket_t xSocket; + FreeRTOS_Socket_t *pxSocket = &xSocket; + + // pxTCPWindow can be any window (points into socket) + TCPWindow_t *pxTCPWindow = &xSocket.u.xTCP.xTCPWindow; + + //////////////////////////////////////////////////////////////// + // Specification and proof of CheckOptions outer loop + + // CBMC pointer model (obviously true) + __CPROVER_assume(buffer_size < CBMC_MAX_OBJECT_SIZE); + + // Preconditions + + // pucPtr is a valid pointer + __CPROVER_assume(EthernetBuffer <= pucPtr && + pucPtr < EthernetBuffer + buffer_size); + // pucLast is a valid pointer (or one past) + __CPROVER_assume(EthernetBuffer <= pucLast && + pucLast <= EthernetBuffer + buffer_size); + // pucPtr is before pucLast + __CPROVER_assume(pucPtr < pucLast); + + // Record initial values + SAVE_OLDVAL(pucPtr, uint8_t *); + SAVE_OLDVAL(pucLast, uint8_t *); + + // Loop variables passed by reference + // Return value describes loop exit: break or continue + BaseType_t rc = + prvSingleStepTCPHeaderOptions(&pucPtr, &pucLast, &pxSocket, &pxTCPWindow); + + // Postconditions + __CPROVER_assert(rc == pdFALSE || OLDVAL(pucPtr) < pucPtr, "pucPtr advanced"); + __CPROVER_assert(pucLast == OLDVAL(pucLast), "pucLast unchanged"); + __CPROVER_assert(pucPtr <= pucLast, "pucPtr <= pucLast"); + +} diff --git a/FreeRTOS/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json b/FreeRTOS/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json new file mode 100644 index 0000000000..e09d11dd10 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/CheckOptionsOuter/Makefile.json @@ -0,0 +1,22 @@ +{ + "ENTRY": "CheckOptionsOuter", + "BUFFER_SIZE": 100, + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvSingleStepTCPHeaderOptions.2:32" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_WIN.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Stream_Buffer.goto", + "$(FREERTOS)/Source/tasks.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": + [ + "BUFFER_SIZE={BUFFER_SIZE}" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c new file mode 100644 index 0000000000..afcda5ef35 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c @@ -0,0 +1,101 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_DHCP.h" + +/* + * CBMC automatically unwinds strlen on a fixed string + */ +const char * pcApplicationHostnameHook(void) { + return "hostname"; +} + +/* + * This stub allows us to overcome the unwinding error obtained + * in the do-while loop within function prvCreatePartDHCPMessage. + * The behaviour is similar to the original function, but failed allocations + * are not considered here (this is a safe assumption that avoids the error) + */ +void *FreeRTOS_GetUDPPayloadBuffer( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ) +{ + NetworkBufferDescriptor_t xNetworkBuffer; + void *pvReturn; + + xNetworkBuffer.xDataLength = ipUDP_PAYLOAD_OFFSET_IPv4 + xRequestedSizeBytes; + xNetworkBuffer.pucEthernetBuffer = malloc( xNetworkBuffer.xDataLength ); + pvReturn = (void *) &( xNetworkBuffer.pucEthernetBuffer[ ipUDP_PAYLOAD_OFFSET_IPv4 ] ); + return pvReturn; +} + +/* + * We stub out FreeRTOS_recvfrom to do nothing but return a buffer of + * arbitrary size (but size at most BUFFER_SIZE) containing arbitrary + * data. We need to bound the size of the buffer in order to bound + * the number of iterations of the loop prvProcessDHCPReplies.0 that + * iterates over the buffer contents. The bound BUFFER_SIZE is chosen + * to be large enough to ensure complete code coverage, and small + * enough to ensure CBMC terminates within a reasonable amount of + * time. + */ +int32_t FreeRTOS_recvfrom( + Socket_t xSocket, void *pvBuffer, size_t xBufferLength, + BaseType_t xFlags, struct freertos_sockaddr *pxSourceAddress, + socklen_t *pxSourceAddressLength ) +{ + __CPROVER_assert(xFlags & FREERTOS_ZERO_COPY, "I can only do ZERO_COPY"); + + size_t xBufferSize; + /* A DHCP message (min. size 241B) is preceded by the IP buffer padding (10B) and the UDP payload (42B) */ + __CPROVER_assume(xBufferSize >= ipBUFFER_PADDING + ipUDP_PAYLOAD_OFFSET_IPv4); + /* The last field of a DHCP message (Options) is variable in length, but 6 additional bytes are enough */ + /* to obtain maximum coverage with this proof. Hence, we have BUFFER_SIZE=299 */ + __CPROVER_assume(xBufferSize <= BUFFER_SIZE); + + /* The buffer gets allocated and we set the pointer past the UDP payload (i.e., start of DHCP message) */ + *((char **)pvBuffer) = malloc(xBufferSize) + ipBUFFER_PADDING + ipUDP_PAYLOAD_OFFSET_IPv4; + + return xBufferSize - ipUDP_PAYLOAD_OFFSET_IPv4 - ipBUFFER_PADDING; +} + +/* + * The harness test proceeds to call DHCPProcess with an unconstrained value + */ +void harness() +{ + BaseType_t xReset; + vDHCPProcess( xReset ); +} diff --git a/FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json b/FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json new file mode 100644 index 0000000000..f7260ddc81 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/Makefile.json @@ -0,0 +1,45 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Permission is hereby granted, free of charge, to any person +# obtaining a copy of this software and associated documentation +# files (the "Software"), to deal in the Software without +# restriction, including without limitation the rights to use, copy, +# modify, merge, publish, distribute, sublicense, and/or sell copies +# of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be +# included in all copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +# MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +# NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS +# BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN +# ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +# CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. +# +# http://aws.amazon.com/freertos +# http://www.FreeRTOS.org +# + +{ + "ENTRY": "DHCPProcess", + "CBMCFLAGS": "--unwind 4 --unwindset strlen.0:11,memcmp.0:7,prvProcessDHCPReplies.0:8 --nondet-static", + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto", + "$(FREERTOS)/Source/tasks.goto" + ], +# Minimal buffer size for maximum coverage, see harness for details. + "BUFFER_SIZE": 299, + "DEF": + [ + "BUFFER_SIZE={BUFFER_SIZE}" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/README.md b/FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/README.md new file mode 100644 index 0000000000..0de21e6b1a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DHCP/DHCPProcess/README.md @@ -0,0 +1,28 @@ +This is the memory safety proof for DHCPProcess function, which is the +function that triggers the DHCP protocol. + +The main stubs in this proof deal with buffer management, which assume +that the buffer is large enough to accomodate a DHCP message plus a +few additional bytes for options (which is the last, variable-sized +field in a DHCP message). We have abstracted away sockets, concurrency +and third-party code. For more details, please check the comments on +the harness file. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* FreeRTOS_sendto +* FreeRTOS_setsockopt +* FreeRTOS_socket +* ulRand +* vARPSendGratuitous +* vApplicationIPNetworkEventHook +* vLoggingPrintf +* vPortEnterCritical +* vPortExitCritical +* vReleaseNetworkBufferAndDescriptor +* vSocketBind +* vSocketClose + diff --git a/FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c b/FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c new file mode 100644 index 0000000000..cbde3397b5 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/IsDHCPSocket_harness.c @@ -0,0 +1,49 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_DHCP.h" + +/* + * The harness test proceeds to call IsDHCPSocket with an unconstrained value + */ +void harness() +{ + Socket_t xSocket; + BaseType_t xResult; + + xResult = xIsDHCPSocket( xSocket ); +} diff --git a/FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json b/FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json new file mode 100644 index 0000000000..eac18fd55f --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/Makefile.json @@ -0,0 +1,40 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Permission is hereby granted, free of charge, to any person +# obtaining a copy of this software and associated documentation +# files (the "Software"), to deal in the Software without +# restriction, including without limitation the rights to use, copy, +# modify, merge, publish, distribute, sublicense, and/or sell copies +# of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be +# included in all copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +# MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +# NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS +# BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN +# ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +# CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. +# +# http://aws.amazon.com/freertos +# http://www.FreeRTOS.org +# + +{ + "ENTRY": "IsDHCPSocket", + "CBMCFLAGS": + [ + "--unwind 1" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.goto" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md b/FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md new file mode 100644 index 0000000000..ec2cc5e210 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DHCP/IsDHCPSocket/README.md @@ -0,0 +1 @@ +This is the memory safety proof for IsDCHPSocket. diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c b/FreeRTOS/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c new file mode 100644 index 0000000000..10a81ece8e --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c @@ -0,0 +1,31 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + +/* Function prvParseDNSReply is proven to be correct separately. +The proof can be found here: https://github.com/aws/amazon-freertos/tree/master/tools/cbmc/proofs/ParseDNSReply */ +uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer, + size_t xBufferLength, + BaseType_t xExpected ) {} + +struct xDNSMessage { + uint16_t usIdentifier; + uint16_t usFlags; + uint16_t usQuestions; + uint16_t usAnswers; + uint16_t usAuthorityRRs; + uint16_t usAdditionalRRs; +}; + +typedef struct xDNSMessage DNSMessage_t; + +void harness() { + NetworkBufferDescriptor_t xNetworkBuffer; + xNetworkBuffer.pucEthernetBuffer = malloc(sizeof(UDPPacket_t)+sizeof(DNSMessage_t)); + ulDNSHandlePacket(&xNetworkBuffer); +} diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json b/FreeRTOS/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json new file mode 100644 index 0000000000..6b2530527a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DNS/DNSHandlePacket/Makefile.json @@ -0,0 +1,12 @@ +{ + "ENTRY": "DNShandlePacket", + "CBMCFLAGS": "--unwind 1", + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + "DEF": + [ + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c b/FreeRTOS/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c new file mode 100644 index 0000000000..0aa26dcb69 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DNS/DNSclear/DNSclear_harness.c @@ -0,0 +1,16 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + + +void harness() { + if( ipconfigUSE_DNS_CACHE != 0 ) { + FreeRTOS_dnsclear(); + } + +} diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSclear/Makefile.json b/FreeRTOS/Test/CBMC/proofs/DNS/DNSclear/Makefile.json new file mode 100644 index 0000000000..22f54b0743 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DNS/DNSclear/Makefile.json @@ -0,0 +1,20 @@ +{ + "ENTRY": "DNSclear", + ################################################################ + # This configuration flag uses DNS cache + "USE_CACHE":1, + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + "DEF": + [ + "ipconfigUSE_DNS_CACHE={USE_CACHE}" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c new file mode 100644 index 0000000000..19ada973d6 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c @@ -0,0 +1,49 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_Sockets.h" + +/* This assumes the length of pcHostName is bounded by MAX_HOSTNAME_LEN and the size of UDPPayloadBuffer is bounded by +MAX_REQ_SIZE. */ + +void *safeMalloc(size_t xWantedSize) { + if(xWantedSize == 0) { + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +/* Abstraction of FreeRTOS_GetUDPPayloadBuffer. This should be checked later. For now we are allocating a fixed sized memory of size MAX_REQ_SIZE. */ +void * FreeRTOS_GetUDPPayloadBuffer(size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ) { + void *pvReturn = safeMalloc(MAX_REQ_SIZE); + return pvReturn; +} + +/* Abstraction of FreeRTOS_socket. This abstraction allocates a memory of size Socket_t. */ +Socket_t FreeRTOS_socket( BaseType_t xDomain, BaseType_t xType, BaseType_t xProtocol ) { + Socket_t xSocket = safeMalloc(sizeof(Socket_t)); /* Replaced malloc by safeMalloc */ + return xSocket; +} + +/* This function only uses the return value of prvParseDNSReply. Hence it returns an unconstrained uint32 value */ +uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer, + size_t xBufferLength, + BaseType_t xExpected ) {} + +void harness() { + size_t len; + __CPROVER_assume(len >= 0 && len <= MAX_HOSTNAME_LEN); + char *pcHostName = safeMalloc(len); /* Replaced malloc by safeMalloc */ + if (len && pcHostName) { + pcHostName[len-1] = NULL; + } + if (pcHostName) { /* Guarding against NULL pointer */ + FreeRTOS_gethostbyname(pcHostName); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json b/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json new file mode 100644 index 0000000000..c7722863cd --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName/Makefile.json @@ -0,0 +1,29 @@ +{ + "ENTRY": "DNSgetHostByName", + ################################################################ + # This configuration sets callback to 0. It also sets MAX_HOSTNAME_LEN to 10 and MAX_REQ_SIZE to 50 for performance issues. + # According to the specification MAX_HOST_NAME is upto 255. + "callback": 0, + "MAX_HOSTNAME_LEN": 10, + "MAX_REQ_SIZE": 50, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvProcessDNSCache.0:5,prvGetHostByName.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.1:{HOSTNAME_UNWIND},strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},strcmp.0:{HOSTNAME_UNWIND},strcpy.0:{HOSTNAME_UNWIND}", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + "ipconfigDNS_USE_CALLBACKS={callback}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}", + "MAX_REQ_SIZE={MAX_REQ_SIZE}" + ], + "OPT" : "-m32" +} diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c b/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c new file mode 100644 index 0000000000..d35d2f8c30 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c @@ -0,0 +1,81 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" +#include "list.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + +/* This proof assumes the length of pcHostName is bounded by MAX_HOSTNAME_LEN and the size of UDPPayloadBuffer is bounded by +MAX_REQ_SIZE. This also abstracts the concurrency. */ + +void *safeMalloc(size_t xWantedSize) { /* This returns a NULL pointer if the requested size is 0. + The implementation of malloc does not return a NULL pointer instead returns a pointer for which there is no memory allocation. */ + if(xWantedSize == 0) { + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +/* Abstraction of pvPortMalloc which calls safemalloc internally. */ +void *pvPortMalloc(size_t xWantedSize) { + return safeMalloc(xWantedSize); +} + +/* Abstraction of FreeRTOS_GetUDPPayloadBuffer. +We always return MAX_REQ_SIZE bytes to keep the proof performant. +This is safe because: +- If the caller requested more bytes, then there is a risk that they + will write past the end of the returned buffer. This proof + therefore shows that the code is memory safe even if + xRequestedSizeBytes > MAX_REQ_SIZE. +- If the caller requested fewer bytes, then they will not be + iterating past the end of the buffer anyway.*/ +void * FreeRTOS_GetUDPPayloadBuffer(size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ) { + void *pvReturn = safeMalloc(MAX_REQ_SIZE); + return pvReturn; +} + +/* Abstraction of FreeRTOS_socket. This abstraction allocates a memory of size Socket_t. */ +Socket_t FreeRTOS_socket( BaseType_t xDomain, BaseType_t xType, BaseType_t xProtocol ){ + Socket_t xCreatedSocket = safeMalloc(sizeof(Socket_t)); // replacing malloc with safeMalloc + return xCreatedSocket; +} + +/* This function FreeRTOS_gethostbyname_a only uses the return value of prvParseDNSReply. Hence it returns an unconstrained uint32 value */ +uint32_t prvParseDNSReply( uint8_t *pucUDPPayloadBuffer, + size_t xBufferLength, + BaseType_t xExpected ) {} + +/* Abstraction of xTaskResumeAll from task pool. This also abstracts the concurrency. */ +BaseType_t xTaskResumeAll(void) { } + +/* The function func mimics the callback function.*/ +void func(const char * pcHostName, void * pvSearchID, uint32_t ulIPAddress) { } + +typedef struct xDNS_Callback { + TickType_t xRemaningTime; /* Timeout in ms */ + FOnDNSEvent pCallbackFunction; /* Function to be called when the address has been found or when a timeout has beeen reached */ + TimeOut_t xTimeoutState; + void *pvSearchID; + struct xLIST_ITEM xListItem; + char pcName[ 1 ]; +} DNSCallback_t; + +void harness() { + FOnDNSEvent pCallback = func; + TickType_t xTimeout; + void *pvSearchID; + size_t len; + __CPROVER_assume(len >= 0 && len <= MAX_HOSTNAME_LEN); + char *pcHostName = safeMalloc(len); // replacing malloc with safeMalloc + if (len && pcHostName) { + pcHostName[len-1] = NULL; + } + if (pcHostName) { // Guarding against NULL pointer + FreeRTOS_gethostbyname_a(pcHostName, pCallback, pvSearchID, xTimeout); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json b/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json new file mode 100644 index 0000000000..2152988159 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_a/Makefile.json @@ -0,0 +1,29 @@ +{ + "ENTRY": "DNSgetHostByName_a", + ################################################################ + # This configuration flag sets callback to 1. It also sets MAX_HOSTNAME_LEN to 10 and MAX_REQ_SIZE to 50 for performance issues. + # According to the specification MAX_HOST_NAME is upto 255. + "callback": 1, + "MAX_HOSTNAME_LEN": 10, + "MAX_REQ_SIZE": 50, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvCreateDNSMessage.0:{HOSTNAME_UNWIND},prvCreateDNSMessage.1:{HOSTNAME_UNWIND},prvGetHostByName.0:{HOSTNAME_UNWIND},prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},strcmp.0:{HOSTNAME_UNWIND},xTaskResumeAll.0:{HOSTNAME_UNWIND},xTaskResumeAll.1:{HOSTNAME_UNWIND},strcpy.0:{HOSTNAME_UNWIND}", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + "ipconfigDNS_USE_CALLBACKS={callback}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}", + "MAX_REQ_SIZE={MAX_REQ_SIZE}" + ], + "OPT" : "-m32" +} diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c b/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c new file mode 100644 index 0000000000..1e5832b20d --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c @@ -0,0 +1,49 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" +#include "list.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + + +/* This proof assumes the length of pcHostName is bounded by MAX_HOSTNAME_LEN. This also abstracts the concurrency. */ + +void vDNSInitialise(void); + +void vDNSSetCallBack(const char *pcHostName, void *pvSearchID, FOnDNSEvent pCallbackFunction, TickType_t xTimeout, TickType_t xIdentifier); + +void *safeMalloc(size_t xWantedSize) { /* Returns a NULL pointer if the wanted size is 0. */ + if(xWantedSize == 0) { + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +/* Abstraction of xTaskCheckForTimeOut from task pool. This also abstracts the concurrency. */ +BaseType_t xTaskCheckForTimeOut(TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait) { } + +/* Abstraction of xTaskResumeAll from task pool. This also abstracts the concurrency. */ +BaseType_t xTaskResumeAll(void) { } + +/* The function func mimics the callback function.*/ +void func(const char * pcHostName, void * pvSearchID, uint32_t ulIPAddress) {} + +void harness() { + vDNSInitialise(); /* We initialize the callbacklist in order to be able to check for functions that timed out. */ + size_t pvSearchID; + FOnDNSEvent pCallback = func; + TickType_t xTimeout; + TickType_t xIdentifier; + size_t len; + __CPROVER_assume(len >= 0 && len <= MAX_HOSTNAME_LEN); + char *pcHostName = safeMalloc(len); + if (len && pcHostName) { + pcHostName[len-1] = NULL; + } + vDNSSetCallBack( pcHostName, &pvSearchID, pCallback, xTimeout, xIdentifier); /* Add an item to be able to check the cancel function if the list is non-empty. */ + FreeRTOS_gethostbyname_cancel(&pvSearchID); +} \ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json b/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json new file mode 100644 index 0000000000..5ea658e4a6 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DNS/DNSgetHostByName_cancel/Makefile.json @@ -0,0 +1,28 @@ +{ + "ENTRY": "DNSgetHostByName_cancel", + ################################################################ + # This configuration flag sets callback to 1. It also sets MAX_HOSTNAME_LEN to 10 for performance issues. + # According to the specification MAX_HOST_NAME is upto 255. + "callback": 1, + "MAX_HOSTNAME_LEN": 10, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},vDNSCheckCallBack.0:2,strcpy.0:{HOSTNAME_UNWIND}", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto", + "$(FREERTOS)/Source/tasks.goto", + "$(FREERTOS)/Source/list.goto" + ], + "DEF": + [ + "ipconfigDNS_USE_CALLBACKS={callback}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}" + ], + "OPT" : "-m32" +} \ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c b/FreeRTOS/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c new file mode 100644 index 0000000000..5b725c4ca0 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DNS/DNSlookup/DNSlookup_harness.c @@ -0,0 +1,32 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" +#include "list.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_DNS.h" +#include "FreeRTOS_IP_Private.h" + +/* This assumes that the length of the hostname is bounded by MAX_HOSTNAME_LEN. */ +void *safeMalloc(size_t xWantedSize) { + if(xWantedSize == 0) { + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +void harness() { + if(ipconfigUSE_DNS_CACHE != 0) { + size_t len; + __CPROVER_assume(len >= 0 && len <= MAX_HOSTNAME_LEN); + char *pcHostName = safeMalloc(len); /* malloc is replaced by safeMalloc */ + if (len && pcHostName) { + pcHostName[len-1] = NULL; + } + if (pcHostName) { /* guarding against NULL pointer */ + FreeRTOS_dnslookup(pcHostName); + } + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json b/FreeRTOS/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json new file mode 100644 index 0000000000..2187bb9144 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/DNS/DNSlookup/Makefile.json @@ -0,0 +1,26 @@ +{ + "ENTRY": "DNSlookup", + ################################################################ + # This configuration uses DNS cache and the MAX_HOSTNAME_LEN is set to 255 according to the specification + "MAX_HOSTNAME_LEN": 255, + "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1", + "USE_CACHE": 1, + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvProcessDNSCache.0:5,strcmp.0:{HOSTNAME_UNWIND}", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto", + "$(FREERTOS)/Source/tasks.goto" + ], + "DEF": + [ + "ipconfigUSE_DNS_CACHE={USE_CACHE}", + "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}" + ], + "OPT" : "-m32" +} \ No newline at end of file diff --git a/FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json b/FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json new file mode 100644 index 0000000000..083feb6e2e --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/Makefile.json @@ -0,0 +1,41 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Permission is hereby granted, free of charge, to any person +# obtaining a copy of this software and associated documentation +# files (the "Software"), to deal in the Software without +# restriction, including without limitation the rights to use, copy, +# modify, merge, publish, distribute, sublicense, and/or sell copies +# of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be +# included in all copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +# MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +# NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS +# BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN +# ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +# CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. +# +# http://aws.amazon.com/freertos +# http://www.FreeRTOS.org +# + +{ + "ENTRY": "SendEventToIPTask", + "CBMCFLAGS": [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto", + "$(FREERTOS)/Source/tasks.goto" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/README.md b/FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/README.md new file mode 100644 index 0000000000..4682310df5 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/README.md @@ -0,0 +1,13 @@ +This is the memory safety proof for xSendEventToIPTask, a function used +for sending different events to IP-Task. We have abstracted away queues. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* uxQueueMessagesWaiting +* xQueueGenericSend + +The coverage is imperfect (97%) because xSendEventToIPTask always +calls xSendEventStructToIPTask with xTimeout==0. diff --git a/FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c b/FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c new file mode 100644 index 0000000000..9bdcbf7aff --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c @@ -0,0 +1,44 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" + +// The harness test proceeds to call SendEventToIPTask with an unconstrained value +void harness() +{ + eIPEvent_t eEvent; + xSendEventToIPTask( eEvent ); +} diff --git a/FreeRTOS/Test/CBMC/proofs/MakefileCommon.json b/FreeRTOS/Test/CBMC/proofs/MakefileCommon.json index 9dfe0d1cf5..a210158f83 100644 --- a/FreeRTOS/Test/CBMC/proofs/MakefileCommon.json +++ b/FreeRTOS/Test/CBMC/proofs/MakefileCommon.json @@ -17,8 +17,13 @@ "INC ": [ "$(FREERTOS)/Source/include", "$(FREERTOS)/Source/portable/MSVC-MingW", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/include", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/Compiler/MSVC", + "$(FREERTOS)/../FreeRTOS-Plus/Demo/FreeRTOS_Plus_TCP_Minimal_Windows_Simulator/WinPCap", + "$(FREERTOS)/Demo/Common/include", "$(FREERTOS)/Test/CBMC/include", - "$(FREERTOS)/Test/CBMC/patches" + "$(FREERTOS)/Test/CBMC/patches" ], "CBMCFLAGS ": [ diff --git a/FreeRTOS/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json b/FreeRTOS/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json new file mode 100644 index 0000000000..96eaeec226 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ProcessDHCPReplies/Makefile.json @@ -0,0 +1,43 @@ +# The proof depends on one parameter: +# BUFFER_SIZE is the size of the buffer being parsed +# The buffer size must be bounded because we must bound the number of +# iterations loops iterating over the buffer. + +{ + "ENTRY": "ProcessDHCPReplies", + +################################################################ +# Buffer size +# Reasonable sizes are BUFFER_SIZE > 241 = sizeof(DHCHMessage_t)) +# Sizes smaller than this causes CBMC to fail in simplify_byte_extract + "BUFFER_SIZE": 300, + +################################################################ +# Buffer header: sizeof(DHCHMessage_t) = 241 + "BUFFER_HEADER": 241, + +################################################################ +# Buffer payload + "BUFFER_PAYLOAD": "__eval 1 if {BUFFER_SIZE} <= {BUFFER_HEADER} else {BUFFER_SIZE} - {BUFFER_HEADER} + 2", + +################################################################ + + "CBMCFLAGS": [ + "--unwind 1", + "--unwindset memcmp.0:7,prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DHCP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/portable/BufferManagement/BufferAllocation_2.goto", + "$(FREERTOS)/Source/event_groups.goto", + "$(FREERTOS)/Source/list.goto" + ], + + "DEF": + [ + "BUFFER_SIZE={BUFFER_SIZE}" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/FreeRTOS/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c new file mode 100644 index 0000000000..4b3e161ab6 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c @@ -0,0 +1,64 @@ +/* Standard includes. */ +#include +#include + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "task.h" +#include "queue.h" +#include "semphr.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_TCP_IP.h" +#include "FreeRTOS_DHCP.h" +#include "NetworkInterface.h" +#include "NetworkBufferManagement.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_TCP_WIN.h" + +// Used to model FreeRTOS_recvfrom returning an arbitrary buffer +char read_buffer[BUFFER_SIZE]; + +BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType ); + +// Stub +int32_t FreeRTOS_recvfrom( + Socket_t xSocket, void *pvBuffer, size_t xBufferLength, + BaseType_t xFlags, struct freertos_sockaddr *pxSourceAddress, + socklen_t *pxSourceAddressLength ) +{ + __CPROVER_assert(xFlags & FREERTOS_ZERO_COPY, "I can only do ZERO_COPY"); + + // Choose buffer size + size_t offset; + size_t buffer_size = BUFFER_SIZE - offset; + char *buffer = read_buffer + offset; + __CPROVER_assume(offset <= BUFFER_SIZE); + + // Choose buffer contents + // __CPROVER_havoc_object may not interact well with simplifier + char temporary[BUFFER_SIZE]; + memcpy(read_buffer, temporary, BUFFER_SIZE); + + *((char **)pvBuffer) = buffer; + return buffer_size; +} + +// Stub +void FreeRTOS_ReleaseUDPPayloadBuffer( void *pvBuffer ) +{ + // no-op +} + +void harness() { + // Omitting model of an unconstrained xDHCPData because xDHCPData is + // the source of uninitialized data only on line 647 to set a + // transaction id is an outgoing message + + BaseType_t xExpectedMessageType; + prvProcessDHCPReplies(xExpectedMessageType); +} diff --git a/FreeRTOS/Test/CBMC/proofs/ReadNameField/Makefile.json b/FreeRTOS/Test/CBMC/proofs/ReadNameField/Makefile.json new file mode 100644 index 0000000000..6202ba05cc --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ReadNameField/Makefile.json @@ -0,0 +1,49 @@ +{ + "ENTRY": "ReadNameField", + +################################################################ +# This is the network buffer size. Set to any positive value. + "NETWORK_BUFFER_SIZE" : "10", + +################################################################ +# This is the size of the buffer into which the name is copied. +# Set to any positive value. +# In the source, NAME_SIZE=254 and NETWORK_BUFFER_SIZE >> NAME_SIZE + "NAME_SIZE": "10", + +################################################################ +# Loop prvReadNameField.0: +# "file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 725 +# should be min of buffer size and name size +# but loop must be unwound at least once, so max of this and 1+1 + "READLOOP0": "prvReadNameField.0", + "READLOOP0_UNWIND": "__eval max(2, min({NETWORK_BUFFER_SIZE}, {NAME_SIZE}))", + +################################################################ +# Loop prvReadNameField.1: +# "file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 715 +# should be min of buffer size and name size +# but loop must be unwound at least twice, so max of this and 2+1 + "READLOOP1": "prvReadNameField.1", + "READLOOP1_UNWIND": "__eval max(3, min({NETWORK_BUFFER_SIZE}, {NAME_SIZE}))", + +################################################################ + + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset {READLOOP0}:{READLOOP0_UNWIND},{READLOOP1}:{READLOOP1_UNWIND}" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + + "DEF": + [ + "NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}", + "NAME_SIZE={NAME_SIZE}" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c b/FreeRTOS/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c new file mode 100644 index 0000000000..66a8fe6b83 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/ReadNameField/ReadNameField_harness.c @@ -0,0 +1,99 @@ +/* Standard includes. */ +#include + +/* 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_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DNS.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" +#include "IPTraceMacroDefaults.h" + +#include "cbmc.h" + +uint8_t *prvReadNameField( uint8_t *pucByte, size_t xSourceLen, char *pcName, size_t xDestLen ); + +void harness() { + + // Choose arbitrary buffer of size at most NETWORK_BUFFER_SIZE + uint8_t my_buffer[NETWORK_BUFFER_SIZE]; + size_t my_buffer_offset; + uint8_t *buffer = my_buffer + my_buffer_offset; + size_t buffer_size = NETWORK_BUFFER_SIZE - my_buffer_offset; + __CPROVER_assume(my_buffer_offset <= NETWORK_BUFFER_SIZE); + + // Choose arbitrary name of size at most NAME_SIZE + char my_name[NAME_SIZE]; + size_t my_name_offset; + char *name = my_name + my_name_offset; + size_t name_size = NAME_SIZE - my_name_offset; + __CPROVER_assume(my_name_offset <= NAME_SIZE); + + // Choose arbitrary pointers into buffer and name + size_t buffer_offset; + size_t name_offset; + uint8_t *pucByte = buffer + buffer_offset; + char *pcName = name + name_offset; + __CPROVER_assume(buffer_offset <= NETWORK_BUFFER_SIZE); + __CPROVER_assume(name_offset <= NAME_SIZE); + + // Choose arbitrary values for space remaining in the buffers + size_t xSourceLen; + size_t xDestLen; + + //////////////////////////////////////////////////////////////// + // Specification and proof of prvReadNameField + + // CBMC pointer model (this is obviously true) + __CPROVER_assume(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE); + __CPROVER_assume(NAME_SIZE < CBMC_MAX_OBJECT_SIZE); + + // Preconditions + + // pointers are valid pointers into buffers + __CPROVER_assume(xSourceLen == 0 || + (buffer <= pucByte && pucByte < buffer + buffer_size)); + __CPROVER_assume(name <= pcName && pcName < name + name_size); + + // lengths are valid values for space remaining in the buffers + __CPROVER_assume(pucByte + xSourceLen <= buffer + buffer_size); + __CPROVER_assume(pcName + xDestLen <= name + name_size); + + // CBMC loop unwinding: bounds depend on xSourceLen and xDestLen + __CPROVER_assume(xSourceLen <= NETWORK_BUFFER_SIZE); + __CPROVER_assume(xDestLen <= NAME_SIZE); + + // Buffer overflow via integer overflow in comparison xNameLen < xDestLen - 1 + // In actual code, xDestLen == 254 + __CPROVER_assume(xDestLen > 0); + + // Save values before function call + SAVE_OLDVAL(pucByte, uint8_t *); + SAVE_OLDVAL(pcName, char *); + SAVE_OLDVAL(xSourceLen, size_t); + SAVE_OLDVAL(xDestLen, size_t); + + // function return value is either NULL or the updated value of pucByte + uint8_t *rc = prvReadNameField(pucByte, xSourceLen, pcName, xDestLen); + + // Postconditions + + // pucByte can be advanced one position past the end of the buffer + __CPROVER_assert((rc == 0) || + (rc - OLDVAL(pucByte) >= 1 && + rc - OLDVAL(pucByte) <= OLDVAL(xSourceLen) && + rc - OLDVAL(pucByte) <= OLDVAL(xDestLen)+2 && + pucByte == OLDVAL(pucByte) && + pcName == OLDVAL(pcName) && + buffer <= rc && rc <= buffer + buffer_size), + "updated pucByte"); +} diff --git a/FreeRTOS/Test/CBMC/proofs/SkipNameField/Makefile.json b/FreeRTOS/Test/CBMC/proofs/SkipNameField/Makefile.json new file mode 100644 index 0000000000..cb2e7a9cc1 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/SkipNameField/Makefile.json @@ -0,0 +1,32 @@ +{ + "ENTRY": "SkipNameField", + +################################################################ +# This is the network buffer size. This can be set to any positive value. + "NETWORK_BUFFER_SIZE": 10, + +################################################################ +# Loop prvSkipNameField.0: +# file lib/FreeRTOS-Plus-TCP/source/FreeRTOS_DNS.c line 778 +# bound should be half network buffer size, since chunk length is at least 2 + "SKIPLOOP0": "prvSkipNameField.0", + "SKIPLOOP0_UNWIND": "__eval ({NETWORK_BUFFER_SIZE} + 1) / 2", + +################################################################ + + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset {SKIPLOOP0}:{SKIPLOOP0_UNWIND}" + ], + + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto" + ], + "DEF": + [ + "NETWORK_BUFFER_SIZE={NETWORK_BUFFER_SIZE}" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c b/FreeRTOS/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c new file mode 100644 index 0000000000..1f62b40247 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/SkipNameField/SkipNameField_harness.c @@ -0,0 +1,75 @@ +/* Standard includes. */ +#include + +/* 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_Sockets.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_DNS.h" +#include "NetworkBufferManagement.h" +#include "NetworkInterface.h" +#include "IPTraceMacroDefaults.h" + +#include "cbmc.h" + +uint8_t *prvSkipNameField( uint8_t *pucByte, size_t xSourceLen ); + +void harness() { + + // Choose arbitrary buffer of size at most NETWORK_BUFFER_SIZE + uint8_t my_buffer[NETWORK_BUFFER_SIZE]; + size_t my_buffer_offset; + uint8_t *buffer = my_buffer + my_buffer_offset; + size_t buffer_size = NETWORK_BUFFER_SIZE - my_buffer_offset; + __CPROVER_assume(my_buffer_offset <= NETWORK_BUFFER_SIZE); + + // Choose arbitrary pointer into buffer + size_t buffer_offset; + uint8_t *pucByte = buffer + buffer_offset; + __CPROVER_assume(buffer_offset <= NETWORK_BUFFER_SIZE); + + // Choose arbitrary value for space remaining in the buffer + size_t xSourceLen; + + //////////////////////////////////////////////////////////////// + // Specification and proof of prvSkipNameField + + // CBMC pointer model (this is obviously true) + __CPROVER_assume(NETWORK_BUFFER_SIZE < CBMC_MAX_OBJECT_SIZE); + + // Preconditions + + // pointer is valid pointer into buffer + __CPROVER_assume(xSourceLen == 0 || + (buffer <= pucByte && pucByte < buffer + buffer_size)); + + // length is valid value for space remaining in the buffer + __CPROVER_assume(pucByte + xSourceLen <= buffer + buffer_size); + + // CBMC loop unwinding: bound depend on xSourceLen + __CPROVER_assume(xSourceLen <= NETWORK_BUFFER_SIZE); + + SAVE_OLDVAL(pucByte, uint8_t *); + SAVE_OLDVAL(xSourceLen, size_t); + + // function return value is either NULL or the updated value of pucByte + uint8_t *rc = prvSkipNameField(pucByte, xSourceLen); + + // Postconditions + + // pucByte can be advanced one position past the end of the buffer + __CPROVER_assert((rc == 0) || + (rc - OLDVAL(pucByte) >= 1 && + rc - OLDVAL(pucByte) <= OLDVAL(xSourceLen) && + pucByte == OLDVAL(pucByte) && + buffer <= rc && rc <= buffer + buffer_size), + "updated pucByte"); +} diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json new file mode 100644 index 0000000000..8f2f3037ec --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/Makefile.json @@ -0,0 +1,59 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Permission is hereby granted, free of charge, to any person +# obtaining a copy of this software and associated documentation +# files (the "Software"), to deal in the Software without +# restriction, including without limitation the rights to use, copy, +# modify, merge, publish, distribute, sublicense, and/or sell copies +# of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be +# included in all copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +# MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +# NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS +# BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN +# ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +# CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. +# +# http://aws.amazon.com/freertos +# http://www.FreeRTOS.org +# + +{ + "ENTRY": "TCPHandleState", + "TX_DRIVER":1, + "RX_MESSAGES":1, + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvWinScaleFactor.0:2", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto" + ], + "DEF": + [ + "ipconfigZERO_COPY_TX_DRIVER={TX_DRIVER}", + "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INSTFLAGS": + [ + "--remove-function-body prvTCPPrepareSend", + "--remove-function-body prvTCPReturnPacket" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md new file mode 100644 index 0000000000..8f08c5931d --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/README.md @@ -0,0 +1,22 @@ +This is the memory safety proof for prvTCPHandleState. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* prvTCPPrepareSend (proved independently) +* prvTCPReturnPacket (proved independently) + +* lTCPAddRxdata +* lTCPWindowRxCheck +* lTCPWindowTxAdd +* ulTCPWindowTxAck +* vTCPWindowInit +* xTCPWindowRxEmpty +* xTCPWindowTxDone + +* uxStreamBufferGet +* vReleaseNetworkBufferAndDescriptor +* vSocketWakeUpUser +* xTaskGetTickCount diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c new file mode 100644 index 0000000000..03867685a7 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c @@ -0,0 +1,73 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_TCP_IP.h" + +#include "../../utility/memory_assignments.c" + +/* This proof assumes that prvTCPPrepareSend and prvTCPReturnPacket are correct. +These functions are proved to be correct separately. */ + +BaseType_t publicTCPHandleState( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer ); + +void harness() { + FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + size_t socketSize = sizeof(FreeRTOS_Socket_t); + if (ensure_memory_is_valid(pxSocket, socketSize)) { + /* ucOptionLength is the number of valid bytes in ulOptionsData[]. + ulOptionsData[] is initialized as uint32_t ulOptionsData[ipSIZE_TCP_OPTIONS/sizeof(uint32_t)]. + This assumption is required for a memcpy function that copies uxOptionsLength + data from pxTCPHeader->ucOptdata to pxTCPWindow->ulOptionsData.*/ + __CPROVER_assume(pxSocket->u.xTCP.xTCPWindow.ucOptionLength == sizeof(uint32_t) * ipSIZE_TCP_OPTIONS/sizeof(uint32_t)); + /* uxRxWinSize is initialized as size_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/ + __CPROVER_assume(pxSocket->u.xTCP.uxRxWinSize >= 0 && pxSocket->u.xTCP.uxRxWinSize <= sizeof(size_t)); + /* uxRxWinSize is initialized as uint16_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/ + __CPROVER_assume(pxSocket->u.xTCP.usInitMSS == sizeof(uint16_t)); + } + + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + size_t bufferSize = sizeof(NetworkBufferDescriptor_t); + if(ensure_memory_is_valid(pxNetworkBuffer, bufferSize)) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t)); + } + if (ensure_memory_is_valid(pxSocket, socketSize) && + ensure_memory_is_valid(pxNetworkBuffer, bufferSize) && + ensure_memory_is_valid(pxNetworkBuffer->pucEthernetBuffer, sizeof(TCPPacket_t)) && + ensure_memory_is_valid(pxSocket->u.xTCP.pxPeerSocket, socketSize)) { + + publicTCPHandleState(pxSocket, &pxNetworkBuffer); + + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json new file mode 100644 index 0000000000..5d34818b55 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/Makefile.json @@ -0,0 +1,49 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Permission is hereby granted, free of charge, to any person +# obtaining a copy of this software and associated documentation +# files (the "Software"), to deal in the Software without +# restriction, including without limitation the rights to use, copy, +# modify, merge, publish, distribute, sublicense, and/or sell copies +# of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be +# included in all copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +# MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +# NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS +# BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN +# ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +# CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. +# +# http://aws.amazon.com/freertos +# http://www.FreeRTOS.org +# + +{ + "ENTRY": "TCPPrepareSend", + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto" + ], + "DEF": + [ + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md new file mode 100644 index 0000000000..3234619180 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/README.md @@ -0,0 +1,15 @@ +This is the memory safety proof for prvTCPPrepareSend. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* ulTCPWindowTxGet +* xTCPWindowTxDone + +* xTaskGetTickCount + +* uxStreamBufferGet +* vReleaseNetworkBufferAndDescriptor +* vSocketWakeUpUser diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c new file mode 100644 index 0000000000..9c41d7b7f5 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c @@ -0,0 +1,72 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_TCP_IP.h" +#include "FreeRTOS_Stream_Buffer.h" + +#include "../../utility/memory_assignments.c" + +/* This proof assumes that pxGetNetworkBufferWithDescriptor is implemented correctly. */ +int32_t publicTCPPrepareSend( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer, UBaseType_t uxOptionsLength ); + +/* Abstraction of pxGetNetworkBufferWithDescriptor. It creates a buffer. */ +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + NetworkBufferDescriptor_t *pxBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated (); + size_t bufferSize = sizeof(NetworkBufferDescriptor_t); + if (ensure_memory_is_valid(pxBuffer, bufferSize)) { + /* The code does not expect pucEthernetBuffer to be equal to NULL if + pxBuffer is not NULL. */ + pxBuffer->pucEthernetBuffer = malloc(xRequestedSizeBytes); + pxBuffer->xDataLength = xRequestedSizeBytes; + } + return pxBuffer; +} + +void harness() { + FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + size_t socketSize = sizeof(FreeRTOS_Socket_t); + size_t bufferSize = sizeof(TCPPacket_t); + if (ensure_memory_is_valid(pxNetworkBuffer, sizeof(*pxNetworkBuffer))) { + pxNetworkBuffer->xDataLength = bufferSize; + /* The code does not expect pucEthernetBuffer to be equal to NULL if + pxNetworkBuffer is not NULL. */ + pxNetworkBuffer->pucEthernetBuffer = malloc(bufferSize); + } + UBaseType_t uxOptionsLength; + if(pxSocket) { + publicTCPPrepareSend(pxSocket, &pxNetworkBuffer, uxOptionsLength ); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json new file mode 100644 index 0000000000..e0f4b2403b --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/Makefile.json @@ -0,0 +1,51 @@ +# +# FreeRTOS memory safety proofs with CBMC. +# Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Permission is hereby granted, free of charge, to any person +# obtaining a copy of this software and associated documentation +# files (the "Software"), to deal in the Software without +# restriction, including without limitation the rights to use, copy, +# modify, merge, publish, distribute, sublicense, and/or sell copies +# of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be +# included in all copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +# MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +# NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS +# BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN +# ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +# CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. +# +# http://aws.amazon.com/freertos +# http://www.FreeRTOS.org +# + +{ + "ENTRY": "TCPReturnPacket", + "RX_MESSAGES":1, + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto" + ], + "DEF": + [ + "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}", + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md new file mode 100644 index 0000000000..1efd644d16 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/README.md @@ -0,0 +1,10 @@ +This is the memory safety proof for prvTCPReturnPacket. + +This proof is a work-in-progress. Proof assumptions are described in +the harness. The proof also assumes the following functions are +memory safe and have no side effects relevant to the memory safety of +this function: + +* usGenerateChecksum +* usGenerateProtocolChecksum +* xNetworkInterfaceOutput diff --git a/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c new file mode 100644 index 0000000000..19552565b8 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c @@ -0,0 +1,67 @@ +/* + * FreeRTOS memory safety proofs with CBMC. + * Copyright (C) 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + * + * http://aws.amazon.com/freertos + * http://www.FreeRTOS.org + */ + +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_TCP_IP.h" + +#include "../../utility/memory_assignments.c" + +/* This proof assumes that pxDuplicateNetworkBufferWithDescriptor is implemented correctly. */ + +void publicTCPReturnPacket( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t *pxNetworkBuffer, uint32_t ulLen, BaseType_t xReleaseAfterSend ); + +/* Abstraction of pxDuplicateNetworkBufferWithDescriptor*/ +NetworkBufferDescriptor_t *pxDuplicateNetworkBufferWithDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer, + BaseType_t xNewLength ) { + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + if (ensure_memory_is_valid(pxNetworkBuffer, sizeof(*pxNetworkBuffer))) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t)); + __CPROVER_assume(pxNetworkBuffer->pucEthernetBuffer); + } + return pxNetworkBuffer; +} + +void harness() { + FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated(); + NetworkBufferDescriptor_t *pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated(); + if (ensure_memory_is_valid(pxNetworkBuffer, sizeof(*pxNetworkBuffer))) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t)); + __CPROVER_assume(pxNetworkBuffer->pucEthernetBuffer); + } + uint32_t ulLen; + BaseType_t xReleaseAfterSend; + /* The code does not expect both of these to be equal to NULL at the same time. */ + __CPROVER_assume(pxSocket != NULL || pxNetworkBuffer != NULL); + publicTCPReturnPacket(pxSocket, pxNetworkBuffer, ulLen, xReleaseAfterSend); +} diff --git a/FreeRTOS/Test/CBMC/proofs/make_cbmc_batch_files.py b/FreeRTOS/Test/CBMC/proofs/make_cbmc_batch_files.py old mode 100644 new mode 100755 diff --git a/FreeRTOS/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json b/FreeRTOS/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json new file mode 100644 index 0000000000..9ad1ef4e93 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/parsing/ProcessIPPacket/Makefile.json @@ -0,0 +1,21 @@ +{ + "ENTRY": "ProcessIPPacket", + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto" + ], + "DEF": + [ + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c b/FreeRTOS/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c new file mode 100644 index 0000000000..def244a51a --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c @@ -0,0 +1,29 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" + +/* proof is done separately */ +BaseType_t xProcessReceivedTCPPacket(NetworkBufferDescriptor_t *pxNetworkBuffer) { } + +/* proof is done separately */ +BaseType_t xProcessReceivedUDPPacket(NetworkBufferDescriptor_t *pxNetworkBuffer, uint16_t usPort) { } + +/* This proof was done before. Hence we assume it to be correct here. */ +void vARPRefreshCacheEntry( const MACAddress_t * pxMACAddress, const uint32_t ulIPAddress ) { } + +eFrameProcessingResult_t publicProcessIPPacket( IPPacket_t * const pxIPPacket, NetworkBufferDescriptor_t * const pxNetworkBuffer); + +void harness() { + + NetworkBufferDescriptor_t * const pxNetworkBuffer = malloc(sizeof(NetworkBufferDescriptor_t)); + /* Pointer to the start of the Ethernet frame. It should be able to access the whole Ethernet frame.*/ + pxNetworkBuffer->pucEthernetBuffer = malloc(ipTOTAL_ETHERNET_FRAME_SIZE); + /* Minimum length of the pxNetworkBuffer->xDataLength is at least the size of the IPPacket_t. */ + __CPROVER_assume(pxNetworkBuffer->xDataLength >= sizeof(IPPacket_t) && pxNetworkBuffer->xDataLength <= ipTOTAL_ETHERNET_FRAME_SIZE); + IPPacket_t * const pxIPPacket = malloc(sizeof(IPPacket_t)); + publicProcessIPPacket(pxIPPacket, pxNetworkBuffer); +} diff --git a/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json b/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json new file mode 100644 index 0000000000..901a727295 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json @@ -0,0 +1,31 @@ +{ + "ENTRY": "ProcessReceivedTCPPacket", + "CBMCFLAGS": + [ + "--unwind 1", + "--unwindset prvTCPSendRepeated.0:13", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_TCP_IP.goto" + ], + "INSTFLAGS": + [ + "--remove-function-body prvSingleStepTCPHeaderOptions", + "--remove-function-body prvCheckOptions", + "--remove-function-body prvTCPPrepareSend", + "--remove-function-body prvTCPReturnPacket", + "--remove-function-body prvTCPHandleState" + ], + "DEF": + [ + "FREERTOS_TCP_ENABLE_VERIFICATION" + ], + "INC": + [ + "$(FREERTOS)/tools/cbmc/include" + ] +} + diff --git a/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c b/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c new file mode 100644 index 0000000000..bf84ecf05e --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c @@ -0,0 +1,62 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_TCP_IP.h" +#include "FreeRTOS_Stream_Buffer.h" + +/* This proof assumes FreeRTOS_socket, pxTCPSocketLookup and +pxGetNetworkBufferWithDescriptor are implemented correctly. + +It also assumes prvSingleStepTCPHeaderOptions, prvCheckOptions, prvTCPPrepareSend, +prvTCPHandleState and prvTCPReturnPacket are correct. These functions are +proved to be correct separately. */ + +/* Implementation of safe malloc */ +void *safeMalloc(size_t xWantedSize ){ + if(xWantedSize == 0){ + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +/* Abstraction of FreeRTOS_socket */ +Socket_t FreeRTOS_socket( BaseType_t xDomain, BaseType_t xType, BaseType_t xProtocol) { + return safeMalloc(sizeof(FreeRTOS_Socket_t)); +} + +/* Abstraction of pxTCPSocketLookup */ +FreeRTOS_Socket_t *pxTCPSocketLookup(uint32_t ulLocalIP, UBaseType_t uxLocalPort, uint32_t ulRemoteIP, UBaseType_t uxRemotePort) { + FreeRTOS_Socket_t * xRetSocket = safeMalloc(sizeof(FreeRTOS_Socket_t)); + if (xRetSocket) { + xRetSocket->u.xTCP.txStream = safeMalloc(sizeof(StreamBuffer_t)); + xRetSocket->u.xTCP.pxPeerSocket = safeMalloc(sizeof(StreamBuffer_t)); + } + return xRetSocket; +} + +/* Abstraction of pxGetNetworkBufferWithDescriptor */ +NetworkBufferDescriptor_t *pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes, TickType_t xBlockTimeTicks ){ + NetworkBufferDescriptor_t *pxNetworkBuffer = safeMalloc(sizeof(NetworkBufferDescriptor_t)); + if(pxNetworkBuffer) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(xRequestedSizeBytes); + __CPROVER_assume(pxNetworkBuffer->xDataLength == ipSIZE_OF_ETH_HEADER + sizeof(int32_t)); + } + return pxNetworkBuffer; +} + +void harness() { + NetworkBufferDescriptor_t *pxNetworkBuffer = safeMalloc(sizeof(NetworkBufferDescriptor_t)); + if (pxNetworkBuffer) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(TCPPacket_t)); + } + if (pxNetworkBuffer && pxNetworkBuffer->pucEthernetBuffer) { + xProcessReceivedTCPPacket(pxNetworkBuffer); + + } + +} diff --git a/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json b/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json new file mode 100644 index 0000000000..017f625f00 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json @@ -0,0 +1,23 @@ +{ + "ENTRY": "ProcessReceivedUDPPacket", + "MAX_RX_PACKETS":1, + "USE_LLMNR":1, + "USE_NBNS":1, + "CBMCFLAGS": + [ + "--unwind 1", + "--nondet-static" + ], + "OBJS": + [ + "$(ENTRY)_harness.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_UDP_IP.goto", + "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_IP.goto" + ], + "DEF": + [ + "ipconfigUDP_MAX_RX_PACKETS={MAX_RX_PACKETS}", + "ipconfigUSE_LLMNR={USE_LLMNR}", + "ipconfigUSE_NBNS={USE_NBNS}" + ] +} diff --git a/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c b/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c new file mode 100644 index 0000000000..0082e5d617 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c @@ -0,0 +1,46 @@ +/* FreeRTOS includes. */ +#include "FreeRTOS.h" +#include "queue.h" + +/* FreeRTOS+TCP includes. */ +#include "FreeRTOS_IP.h" +#include "FreeRTOS_IP_Private.h" +#include "FreeRTOS_ARP.h" +#include "FreeRTOS_UDP_IP.h" +#include "FreeRTOS_TCP_IP.h" + +/*This proof assumes that pxUDPSocketLookup is implemented correctly. */ + +/* This proof was done before. Hence we assume it to be correct here. */ +void vARPRefreshCacheEntry(const MACAddress_t * pxMACAddress, const uint32_t ulIPAddress) { } + +/* This proof was done before. Hence we assume it to be correct here. */ +BaseType_t xIsDHCPSocket(Socket_t xSocket) { } + +/* This proof was done before. Hence we assume it to be correct here. */ +uint32_t ulDNSHandlePacket(NetworkBufferDescriptor_t *pxNetworkBuffer) { } + +/* Implementation of safe malloc */ +void *safeMalloc(size_t xWantedSize) { + if(xWantedSize == 0) { + return NULL; + } + uint8_t byte; + return byte ? malloc(xWantedSize) : NULL; +} + +/* Abstraction of pxUDPSocketLookup */ +FreeRTOS_Socket_t *pxUDPSocketLookup( UBaseType_t uxLocalPort ) { + return safeMalloc(sizeof(FreeRTOS_Socket_t)); +} + +void harness() { + NetworkBufferDescriptor_t *pxNetworkBuffer = safeMalloc(sizeof(NetworkBufferDescriptor_t)); + if(pxNetworkBuffer) { + pxNetworkBuffer->pucEthernetBuffer = safeMalloc(sizeof(UDPPacket_t)); + } + uint16_t usPort; + if (pxNetworkBuffer && pxNetworkBuffer->pucEthernetBuffer) { + xProcessReceivedUDPPacket(pxNetworkBuffer, usPort); + } +} diff --git a/FreeRTOS/Test/CBMC/proofs/utility/memory_assignments.c b/FreeRTOS/Test/CBMC/proofs/utility/memory_assignments.c new file mode 100644 index 0000000000..6bcb9319a2 --- /dev/null +++ b/FreeRTOS/Test/CBMC/proofs/utility/memory_assignments.c @@ -0,0 +1,24 @@ +#define ensure_memory_is_valid( px, length ) (px != NULL) && __CPROVER_w_ok((px), length) + +/* Implementation of safe malloc which returns NULL if the requested size is 0. + Warning: The behavior of malloc(0) is platform dependent. + It is possible for malloc(0) to return an address without allocating memory.*/ +void *safeMalloc(size_t xWantedSize) { + return nondet_bool() ? malloc(xWantedSize) : NULL; +} + +/* Memory assignment for FreeRTOS_Socket_t */ +FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated () { + FreeRTOS_Socket_t *pxSocket = safeMalloc(sizeof(FreeRTOS_Socket_t)); + if (ensure_memory_is_valid(pxSocket, sizeof(FreeRTOS_Socket_t))) { + pxSocket->u.xTCP.rxStream = safeMalloc(sizeof(StreamBuffer_t)); + pxSocket->u.xTCP.txStream = safeMalloc(sizeof(StreamBuffer_t)); + pxSocket->u.xTCP.pxPeerSocket = safeMalloc(sizeof(FreeRTOS_Socket_t)); + } + return pxSocket; +} + +/* Memory assignment for FreeRTOS_Network_Buffer */ +NetworkBufferDescriptor_t * ensure_FreeRTOS_NetworkBuffer_is_allocated () { + return safeMalloc(sizeof(NetworkBufferDescriptor_t)); +}