Buffer Overflow

[shivani]

Hello,

I am using a simple sample code to check whether CBMC checks for Buffer Overflow or not.

#include<stdio.h>
#include<string.h>
void function(char *str) {
   char buffer[16];

   strcpy(buffer,str);
}

int main() {
  char large_string[256];
  int i;

  for( i = 0; i < 255; i++)
    large_string[i] = 'A';

  function(large_string);
}


Even though the plugin checks for the function and for bounds of the destination string, it declares those properties as successful.


Does CBMC not check for buffer overflows when using functions  like strcpy and gets ?

[Peter Schrammel]

Hi,

I'm not sure which options you checked when you ran it and what number of unwindings you specified. So, please provide us with this information next time.

For this example to perform a correct buffer overflow check, you require
- "bounds-check" and "pointer-check" options

- set unwind to at least 256

- do NOT check no-unwinding-assertions (unless you know what it is doing)

If you are wondering why CBMC reports an error even though you used char buffer[256], you may want to make sure that large_string is actually filled with a proper string, i.e. it contains the null character.

Best wishes,

Peter

--

---
You received this message because you are subscribed to the Google Groups "CProver Support" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cprover-suppo...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[shivani]

Hello Peter,
Thanks for the suggestions. Running CBMC from command line with the options you suggested works. (Eclipse plugin is not detecting errors in any programs)
But I checked another program with a gets() function. In case of gets() function it isn't giving any errors. So does this mean gets() isn't supported by strcpy() is?

Thanks for your time,
Shivani

[Peter Schrammel]

Hi Shivani,

if you sent me a screenshot of the CBMC external tool configuration I might be able to figure out why the plugin is not detecting anything.

Regarding gets(), please send me the sample program that doesn't work.

Thanks,

Peter

[shivani]

#include <stdio.h>
#include <string.h>

int main(void)
{
    char buff[15];
    int pass = 0;

    printf("\n Enter the password : \n");
    gets(buff);

    if(strcmp(buff, "thegeekstuff"))
    {
        printf ("\n Wrong Password \n");
    }
    else
    {
        printf ("\n Correct Password \n");
        pass = 1;
    }

    if(pass)
    {
       /* Now Give root or admin rights to user*/
        printf ("\n Root privileges given to the user \n");
    }

    return 0;
}

Using this command ->  cbmc ff.c --pointer-check --bounds-check --unwind 16
Output is successful verification.

I have attached the screenshot of eclipse configuration and also the file. Again the output is successful verification.

Thanks and regards,
Shivani

[Peter Schrammel]

Can you scroll down, please, and send me the lower bit of the configuration too?

Thanks,

Peter

[shivani]

PFA.
If possible, please let me know about the problem with the gets() code as well. (It isn't working even from command line).
Thanks and regards,
Shivani.

[Peter Schrammel]

Hello,

1) CBMC does not provide an implementation for gets. Mind the warning

**** WARNING: no body for function gets

when running CBMC. So, it will not check it and you cannot expect it to find an error.

But you can easily provide an implementation yourself. For example, a suitable implementation could be:

char *gets(char *str)
{
  __CPROVER_assert(0,"BUFFER OVERFLOW");
}

2) Only tick the boxes for options that you need (pointer-check, bounds-check, ...). "cover-assertions" does something completely different (namely checking whether assertions are reachable at all; i.e. CBMC does *not* check whether or not the assertions hold).

Peter

--