Fix CBMC proofs for DNS by tony-josi-aws · Pull Request #718 · FreeRTOS/FreeRTOS-Plus-TCP

tony-josi-aws · 2023-02-14T19:21:24Z

This PR fixes the build issues and proof failures for the DNS CBMC proofs post the IPv6 changes.

Test Steps

cd test/cbmc/proofs/
python run-cbmc-proofs.py

Related Issue

Failing CBMC proofs

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

Prior to this commit, CBMC would emit logging information in plain text format, which does not contain information required for the CBMC VSCode debugger. This commit makes CBMC use XML instead of plain text. Co-authored-by: Mark Tuttle <tuttle@acm.org>

AniruddhaKanhere · 2023-02-15T23:02:29Z

                    {
                        #if ( ipconfigUSE_IPv6 != 0 )
-                            if( ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 )
+                            if( ( ppxAddressInfo != NULL) && ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 )


Suggested change

if( ( ppxAddressInfo != NULL) && ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 )

if( ( ppxAddressInfo != NULL ) &&

( ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 ) )

Updated all formatting issues

AniruddhaKanhere · 2023-02-15T23:03:23Z

+    BaseType_t ret;
    int len;

+    __CPROVER_assume( len > sizeof(DNSMessage_t) && len < CBMC_MAX_OBJECT_SIZE );


Suggested change

__CPROVER_assume( len > sizeof(DNSMessage_t) && len < CBMC_MAX_OBJECT_SIZE );

__CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) &&

( len < CBMC_MAX_OBJECT_SIZE ) );

AniruddhaKanhere · 2023-02-15T23:04:09Z

-    Socket_t sock;
+
+    Socket_t sock = safeMalloc( sizeof(struct xSOCKET) );
+    __CPROVER_assume(sock != NULL); 


Suggested change

__CPROVER_assume(sock != NULL);

__CPROVER_assume( sock != NULL );

AniruddhaKanhere · 2023-02-15T23:06:16Z

+    pxNetworkBuffer->pucEthernetBuffer = ( (uint8_t *) malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET ) ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
+    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );


Why are we assuming this? Why cannot malloc fail? In actual scenario, it can fail and in this proof it should fail too. And we need to make the code robust to check this if we are not doing that already.

AniruddhaKanhere · 2023-02-15T23:07:10Z

+    __CPROVER_assume( pxNetworkBuffer != NULL );
+
+    pxNetworkBuffer->pucEthernetBuffer = ( (uint8_t *) malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET ) ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
+    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );


Similarly this should not be here. Malloc can fail in real life.

AniruddhaKanhere · 2023-02-15T23:07:37Z

+{
+
+    Socket_t sock = safeMalloc( sizeof(struct xSOCKET) );
+    __CPROVER_assume(sock != NULL); 


Similar comment here. Do we have a justification for the malloc not to fail?

AniruddhaKanhere · 2023-02-21T01:14:07Z

 Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks );
 void DNS_CloseSocket( Socket_t xDNSSocket );
-void DNS_ReadReply( Socket_t xDNSSocket,
+BaseType_t DNS_ReadReply( const ConstSocket_t xDNSSocket,


Do we need const ConstSocket_t? Or should ConstSocket_t be enough?

AniruddhaKanhere · 2023-02-21T01:18:58Z

+NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
+                                                              TickType_t xBlockTimeTicks )
+{
+    NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) malloc( sizeof( NetworkBufferDescriptor_t ) );


Why are we using malloc and safeMalloc? Why not stick to one?

AniruddhaKanhere · 2023-02-21T01:26:48Z

+    will be less than ipconfigENDPOINT_DNS_ADDRESS_COUNT  */
+    __CPROVER_assume( pxNetworkEndPoints->ipv6_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); 
+    __CPROVER_assume( pxNetworkEndPoints->ipv4_settings.ucDNSIndex < ipconfigENDPOINT_DNS_ADDRESS_COUNT ); 
+    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );


Why assume when you can set it to NULL directly?

AniruddhaKanhere · 2023-02-21T01:29:27Z

+                      "Precondition: pcHostName != NULL" );
+    __CPROVER_assert( pvSearchID != NULL,
+                      "Precondition: pvSearchID != NULL" );
+}


Any asserts on the pxAddressInfo pointer?

AniruddhaKanhere · 2023-02-21T01:32:00Z

+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+
+    //pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;


Unused comment?

AniruddhaKanhere · 2023-02-22T00:25:26Z

 {
    size_t len;

+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );


Here again we are using safeMalloc. Why not use malloc only?

…lus-TCP into fix_cbmc_proof_dns

* Use CBMC XML output to enable VSCode debugger (FreeRTOS#673) Prior to this commit, CBMC would emit logging information in plain text format, which does not contain information required for the CBMC VSCode debugger. This commit makes CBMC use XML instead of plain text. Co-authored-by: Mark Tuttle <tuttle@acm.org> * wip * wip DNSgetHostByName * wip DNSgetHostByName * fixed cbmc proof for DNS_ReadNameField * wip DNSgetHostByName_a_harness * Fix CBMC prooff for DNSgetHostByName * wip fix DNSgetHostByName_a CBMC proof * fixed cbmc target func not called issue in DNSclear * fixed cbmc target func not called issue in DNSlookup * fix DNSgetHostByName_a CBMC proof * update comments * more asserts * fixing formatting * updating as per review comments * fix dns after review comments * adding more asserts * adds more asserts * minor fix * fixing comments * fixing comments * fixing minor issue * fixing DNS_ReadReply() signature * making code more consistant * adding more asserts * making code more consistent --------- Co-authored-by: Kareem Khazem <karkhaz@amazon.com> Co-authored-by: Mark Tuttle <tuttle@acm.org>

* updating doxygen config * fixing doxygen comments * adding IPv6 files and fixing comments * fix doxygen cfg and file names in comments * wip doxygen v6 docs * adding doxygen comments * include RA src file to doxgendocs generation * fix spell check issues * Uncrustify: triggered by comment. * fix minor build issue * fix spell check issues * Uncrustify: triggered by comment * fix trailing white space * Dev integration hein.v8 (#738) * Updating tcp utilities * Some more change in dev_integration_hein.v8 * In FreeRTOS_DNS_Parser.c : use 'ipUDP_PAYLOAD_OFFSET_IPv4' in stead of 'ipIP_PAYLOAD_OFFSET' * And a few more corrections * Changes to WinPCap network interface, removed debugging code * After applying uncrustify * Oops, I forgot the push changes in include files. * Now removing it, hopefully --------- Co-authored-by: Nikhil Kamath <110539926+amazonKamath@users.noreply.github.com> Co-authored-by: Monika Singh <108652024+moninom1@users.noreply.github.com> * Fix CBMC proofs for DNS (#718) * Use CBMC XML output to enable VSCode debugger (#673) Prior to this commit, CBMC would emit logging information in plain text format, which does not contain information required for the CBMC VSCode debugger. This commit makes CBMC use XML instead of plain text. Co-authored-by: Mark Tuttle <tuttle@acm.org> * wip * wip DNSgetHostByName * wip DNSgetHostByName * fixed cbmc proof for DNS_ReadNameField * wip DNSgetHostByName_a_harness * Fix CBMC prooff for DNSgetHostByName * wip fix DNSgetHostByName_a CBMC proof * fixed cbmc target func not called issue in DNSclear * fixed cbmc target func not called issue in DNSlookup * fix DNSgetHostByName_a CBMC proof * update comments * more asserts * fixing formatting * updating as per review comments * fix dns after review comments * adding more asserts * adds more asserts * minor fix * fixing comments * fixing comments * fixing minor issue * fixing DNS_ReadReply() signature * making code more consistant * adding more asserts * making code more consistent --------- Co-authored-by: Kareem Khazem <karkhaz@amazon.com> Co-authored-by: Mark Tuttle <tuttle@acm.org> * Uncrustify: triggered by comment * fixing formatting --------- Co-authored-by: GitHub Action <action@github.com> Co-authored-by: Hein Tibosch <hein_tibosch@yahoo.es> Co-authored-by: Nikhil Kamath <110539926+amazonKamath@users.noreply.github.com> Co-authored-by: Monika Singh <108652024+moninom1@users.noreply.github.com> Co-authored-by: Kareem Khazem <karkhaz@amazon.com> Co-authored-by: Mark Tuttle <tuttle@acm.org>

karkhaz and others added 13 commits February 8, 2023 10:09

wip

e703699

wip DNSgetHostByName

ba95154

wip DNSgetHostByName

7d09c1e

fixed cbmc proof for DNS_ReadNameField

c243eee

wip DNSgetHostByName_a_harness

ae10fc0

Fix CBMC prooff for DNSgetHostByName

f07501f

Merge branch 'dev/IPv6_integration' into fix_cbmc_proof_dns

e08f38e

wip fix DNSgetHostByName_a CBMC proof

fd1690e

fixed cbmc target func not called issue in DNSclear

241535f

fixed cbmc target func not called issue in DNSlookup

8dac64d

fix DNSgetHostByName_a CBMC proof

88f699f

update comments

07e208a

tony-josi-aws requested a review from a team as a code owner February 14, 2023 19:21

more asserts

e3d4b4c

AniruddhaKanhere reviewed Feb 15, 2023

View reviewed changes

tony-josi-aws added 9 commits February 16, 2023 15:28

fixing formatting

22e6eb6

updating as per review comments

3a9405d

fix dns after review comments

6e229f9

adding more asserts

45910b3

adds more asserts

cb85b0c

minor fix

653c089

fixing comments

3680cac

fixing comments

93b9c21

fixing minor issue

d6ebdab

AniruddhaKanhere reviewed Feb 21, 2023

View reviewed changes

tony-josi-aws added 4 commits February 21, 2023 15:58

Merge branch 'dev/IPv6_integration' into fix_cbmc_proof_dns

5f9ad1d

fixing DNS_ReadReply() signature

89955c6

making code more consistant

5661ba2

adding more asserts

ff8c448

AniruddhaKanhere reviewed Feb 22, 2023

View reviewed changes

tony-josi-aws added 3 commits February 22, 2023 09:10

making code more consistent

7d454ec

Merge branch 'dev/IPv6_integration' of github.com:FreeRTOS/FreeRTOS-P…

4c4023b

…lus-TCP into fix_cbmc_proof_dns

Merge branch 'dev/IPv6_integration' into fix_cbmc_proof_dns

74d8bd1

shubnil approved these changes Feb 23, 2023

View reviewed changes

tony-josi-aws merged commit e9bb577 into FreeRTOS:dev/IPv6_integration Feb 23, 2023

	if( ( ppxAddressInfo != NULL) && ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 )
	if( ( ppxAddressInfo != NULL ) &&
	( ( *ppxAddressInfo )->ai_family == FREERTOS_AF_INET6 ) )

	__CPROVER_assume( len > sizeof(DNSMessage_t) && len < CBMC_MAX_OBJECT_SIZE );
	__CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) &&
	( len < CBMC_MAX_OBJECT_SIZE ) );

	__CPROVER_assume(sock != NULL);
	__CPROVER_assume( sock != NULL );

		pxNetworkBuffer->pucEthernetBuffer = ( (uint8_t *) malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET ) ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
		__CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );

Conversation

tony-josi-aws commented Feb 14, 2023

Test Steps

Related Issue

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants