CBMC seems to not detect buffer overflows from read funcs.

[johnfxgalea]

Commit ID: 8360233

CBMC does not detect buffer overflows stemming from read functions. I have provided a simple test case highlighting this issue.

#include <unistd.h>

int main()
{
    char data[20];

    if(read(0, data, 100) < 0)
        printf("An error has occurred");
    else
        printf("Read occurred");

    return 0;
}

Command: cbmc test.c --bounds-check --pointer-check --unwind 100

After inspecting the source file cbmc/src/ansi-c/library/unistd.c, there seems to be dead code at line 216 which aids overcoming the issue. This code is shown below.

#if 0
    size_t i;
    for(i=0; i<nbyte; i++)
    {
      char nondet_char;
      ((char *)buf)[i]=nondet_char;
    }
#else
    char nondet_bytes[nbyte];
    __CPROVER_array_replace((char*)buf, nondet_bytes);
#endif


    __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
    return error ? -1 : nread;
  }

If I set the value in the if statement to 1 and compile, CBMC detects the vulnerability.

Command: cbmc test.c --bounds-check --pointer-check --unwind 100

Not sure if I am missing something here which would otherwise solve the issue.

[tautschnig]

It seems I forgot about read (and possibly others?) in bb8cfaa. A similar fix is required.