Adding FreeRTOS+TCP CBMC proofs to FreeRTOS/FreeRTOS (#56)
ParseDNSReply is to be added in the next PR.pull/59/head
AniruddhaKanhere
5 years ago
committed by
GitHub
parent
40a31b6d35
commit
4db195c916
@ -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 */
|
||||
@ -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();
|
||||
}
|
||||
@ -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":
|
||||
[
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,2 @@
|
||||
Assuming that xNetworkInterfaceOutput is memory safe,
|
||||
this harness proves the memory safety of the vARPAgeCache function.
|
||||
@ -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 );
|
||||
}
|
||||
@ -0,0 +1,15 @@
|
||||
{
|
||||
"ENTRY": "ARPGenerateRequestPacket",
|
||||
"CBMCFLAGS":
|
||||
[
|
||||
"--unwind 1"
|
||||
],
|
||||
"OBJS":
|
||||
[
|
||||
"$(ENTRY)_harness.goto",
|
||||
"$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto"
|
||||
],
|
||||
"DEF":
|
||||
[
|
||||
]
|
||||
}
|
||||
@ -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.
|
||||
@ -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 );
|
||||
}
|
||||
@ -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"
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
@ -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.
|
||||
@ -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 );
|
||||
}
|
||||
@ -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"
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,4 @@
|
||||
ARPGetCacheEntryByMac is memory safe,
|
||||
if it is enabled.
|
||||
|
||||
ARPGetCacheEntryByMac does not use multiple configurations internally.
|
||||
@ -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 );
|
||||
}
|
||||
@ -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"]}
|
||||
]
|
||||
}
|
||||
@ -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.
|
||||
@ -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 );
|
||||
}
|
||||
@ -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"]}
|
||||
]
|
||||
}
|
||||
@ -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.
|
||||
@ -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();
|
||||
}
|
||||
@ -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":
|
||||
[
|
||||
]
|
||||
}
|
||||
@ -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.
|
||||
@ -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();
|
||||
}
|
||||
|
||||
@ -0,0 +1,15 @@
|
||||
{
|
||||
"ENTRY": "ClearARP",
|
||||
"CBMCFLAGS":
|
||||
[
|
||||
"--unwind 1"
|
||||
],
|
||||
"OBJS":
|
||||
[
|
||||
"$(ENTRY)_harness.goto",
|
||||
"$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto"
|
||||
],
|
||||
"DEF":
|
||||
[
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,2 @@
|
||||
This proof demonstrates the memory safety of the ClearARP function in the FreeRTOS_ARP.c file.
|
||||
No restrictions are made.
|
||||
@ -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"]
|
||||
}
|
||||
]
|
||||
}
|
||||
@ -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 );
|
||||
}
|
||||
@ -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.
|
||||
@ -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();
|
||||
}
|
||||
@ -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"
|
||||
]
|
||||
}
|
||||
@ -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.
|
||||
@ -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"
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,71 @@
|
||||
/* This harness is linked against
|
||||
* libraries/freertos_plus/standard/freertos_plus_tcp/source/portable/BufferManagement/BufferAllocation_1.goto
|
||||
*/
|
||||
#include <stdint.h>
|
||||
#include <stdio.h>
|
||||
|
||||
/* 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 );
|
||||
}
|
||||
}
|
||||
@ -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.
|
||||
@ -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"
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,54 @@
|
||||
/* This harness is linked against
|
||||
* libraries/freertos_plus/standard/freertos_plus_tcp/source/portable/BufferManagement/BufferAllocation_2.goto
|
||||
*/
|
||||
#include <stdint.h>
|
||||
#include <stdio.h>
|
||||
|
||||
/* 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 );
|
||||
}
|
||||
}
|
||||
|
||||
@ -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.
|
||||
@ -0,0 +1,113 @@
|
||||
/* Standard includes. */
|
||||
#include <stdint.h>
|
||||
#include <stdio.h>
|
||||
|
||||
/* 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);
|
||||
}
|
||||
@ -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}"
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,105 @@
|
||||
/* Standard includes. */
|
||||
#include <stdint.h>
|
||||
#include <stdio.h>
|
||||
|
||||
/* 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");
|
||||
}
|
||||
@ -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}"
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,123 @@
|
||||
/* Standard includes. */
|
||||
#include <stdint.h>
|
||||
#include <stdio.h>
|
||||
|
||||
/* 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");
|
||||
|
||||
}
|
||||
@ -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}"
|
||||
]
|
||||
}
|
||||
@ -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 <stdint.h>
|
||||
|
||||
/* 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 );
|
||||
}
|
||||
@ -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}"
|
||||
]
|
||||
}
|
||||
@ -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
|
||||
|
||||
@ -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 <stdint.h>
|
||||
|
||||
/* 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 );
|
||||
}
|
||||
@ -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"
|
||||
]
|
||||
}
|
||||
@ -0,0 +1 @@
|
||||
This is the memory safety proof for IsDCHPSocket.
|
||||
@ -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);
|
||||
}
|
||||
@ -0,0 +1,12 @@
|
||||
{
|
||||
"ENTRY": "DNShandlePacket",
|
||||
"CBMCFLAGS": "--unwind 1",
|
||||
"OBJS":
|
||||
[
|
||||
"$(ENTRY)_harness.goto",
|
||||
"$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_DNS.goto"
|
||||
],
|
||||
"DEF":
|
||||
[
|
||||
]
|
||||
}
|
||||
@ -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();
|
||||
}
|
||||
|
||||
}
|
||||
@ -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}"
|
||||
]
|
||||
}
|
||||
@ -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);
|
||||
}
|
||||
}
|
||||
@ -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"
|
||||
}
|
||||
@ -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);
|
||||
}
|
||||
}
|
||||
@ -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"
|
||||
}
|
||||
@ -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);
|
||||
}
|
||||
@ -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"
|
||||
}
|
||||
@ -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);
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -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"
|
||||
}
|
||||
@ -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"
|
||||
]
|
||||
}
|
||||
@ -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.
|
||||
@ -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 <stdint.h>
|
||||
|
||||
/* 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 );
|
||||
}
|
||||
@ -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}"
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,64 @@
|
||||
/* Standard includes. */
|
||||
#include <stdint.h>
|
||||
#include <stdio.h>
|
||||
|
||||
/* 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);
|
||||
}
|
||||
@ -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}"
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,99 @@
|
||||
/* Standard includes. */
|
||||
#include <stdint.h>
|
||||
|
||||
/* FreeRTOS includes. */
|
||||
#include "FreeRTOS.h"
|
||||
#include "task.h"
|
||||
#include "queue.h"
|
||||
#include "list.h"
|
||||
#include "semphr.h"
|
||||
|
||||
/* FreeRTOS+TCP includes. */
|
||||
#include "FreeRTOS_IP.h"
|
||||
#include "FreeRTOS_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");
|
||||
}
|
||||
@ -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}"
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,75 @@
|
||||
/* Standard includes. */
|
||||
#include <stdint.h>
|
||||
|
||||
/* FreeRTOS includes. */
|
||||
#include "FreeRTOS.h"
|
||||
#include "task.h"
|
||||
#include "queue.h"
|
||||
#include "list.h"
|
||||
#include "semphr.h"
|
||||
|
||||
/* FreeRTOS+TCP includes. */
|
||||
#include "FreeRTOS_IP.h"
|
||||
#include "FreeRTOS_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");
|
||||
}
|
||||
@ -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"
|
||||
]
|
||||
}
|
||||
@ -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
|
||||
@ -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);
|
||||
|
||||
}
|
||||
}
|
||||
@ -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"
|
||||
]
|
||||
}
|
||||
@ -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
|
||||
@ -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 );
|
||||
}
|
||||
}
|
||||
@ -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"
|
||||
]
|
||||
}
|
||||
@ -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
|
||||
@ -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);
|
||||
}
|
||||
@ -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"
|
||||
]
|
||||
}
|
||||
@ -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);
|
||||
}
|
||||
@ -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"
|
||||
]
|
||||
}
|
||||
|
||||
@ -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);
|
||||
|
||||
}
|
||||
|
||||
}
|
||||
@ -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}"
|
||||
]
|
||||
}
|
||||
@ -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);
|
||||
}
|
||||
}
|
||||
@ -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));
|
||||
}
|
||||
Loading…
Reference in New Issue