Undetected pointer representation overflows

[remi-delmas-3000]

On the example below, --pointer-overflow-check --unsigned-overflow-check --signed-overflow-check all pass but some of the manually written assertions fail, showing that not all possible pointer overflows are detected.

In theory p + offset can overflow the pointer width representation and also cause an overflow in the internal pointer representation of CBMC.

The full width 64bit offset value seems preserved as long as no intermediate variable assignment occurs, even through round-trip pointer-integer-pointer conversions.

Any downstream property about pointer q or the variable r would potentially be meaningless since they end up representing a different pointer value or integer value that what it came from.

All problems go away if we assume that size <= __CPROVER_max_malloc_size.

CBMC should either check that all allocations are within [0, __CPROVER_max_malloc_size], or detect all pointer overflows.

#include <stdlib.h>
#include <assert.h>
int main()
{
    size_t size;
    char *p = malloc(size);
    size_t offset;
    __CPROVER_assume(offset <= size);

    assert(__CPROVER_POINTER_OBJECT(p + offset) == __CPROVER_POINTER_OBJECT(p)); // SUCCESS
    assert(__CPROVER_POINTER_OFFSET(p + offset) == offset);                      // SUCCESS

    // through an intermediate variable
    char *q = p + offset;
    assert(__CPROVER_POINTER_OBJECT(q) == __CPROVER_POINTER_OBJECT(p)); // SUCCESS
    assert(__CPROVER_POINTER_OFFSET(q) == offset);                      // FAILURE

    // through a cast
    assert(__CPROVER_POINTER_OBJECT(p) == __CPROVER_POINTER_OBJECT((char *)(size_t)(p + offset)));          // SUCCESS
    assert(__CPROVER_POINTER_OBJECT(p + offset) == __CPROVER_POINTER_OBJECT((char *)(size_t)(p + offset))); // SUCCESS
    assert(__CPROVER_POINTER_OFFSET(p + offset) == __CPROVER_POINTER_OFFSET((char *)(size_t)(p + offset))); // SUCCESS

    // through a intermediate variable and cast
    size_t r = (size_t)q;
    assert(__CPROVER_POINTER_OBJECT(p) == __CPROVER_POINTER_OBJECT((char *)r));          // SUCCESS
    assert(__CPROVER_POINTER_OBJECT(p + offset) == __CPROVER_POINTER_OBJECT((char *)r)); // SUCCESS
    assert(__CPROVER_POINTER_OFFSET(p + offset) == __CPROVER_POINTER_OFFSET((char *)r)); // FAILURE

    return 0;
}

** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 31 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 36 max allocation may fail: SUCCESS

ptr_conversion.c function main
[main.assertion.1] line 10 assertion __CPROVER_POINTER_OBJECT(p + offset) == __CPROVER_POINTER_OBJECT(p): SUCCESS
[main.pointer_arithmetic.1] line 10 pointer arithmetic: pointer NULL in p + (signed long int)offset: SUCCESS
[main.pointer_arithmetic.2] line 10 pointer arithmetic: pointer invalid in p + (signed long int)offset: SUCCESS
[main.pointer_arithmetic.3] line 10 pointer arithmetic: deallocated dynamic object in p + (signed long int)offset: SUCCESS
[main.pointer_arithmetic.4] line 10 pointer arithmetic: dead object in p + (signed long int)offset: SUCCESS
[main.pointer_arithmetic.5] line 10 pointer arithmetic: pointer outside object bounds in p + (signed long int)offset: SUCCESS
[main.pointer_arithmetic.6] line 10 pointer arithmetic: invalid integer address in p + (signed long int)offset: SUCCESS
[main.assertion.2] line 11 assertion __CPROVER_POINTER_OFFSET(p + offset) == offset: SUCCESS
[main.assertion.3] line 15 assertion __CPROVER_POINTER_OBJECT(q) == __CPROVER_POINTER_OBJECT(p): SUCCESS
[main.assertion.4] line 16 assertion __CPROVER_POINTER_OFFSET(q) == offset: FAILURE
[main.assertion.5] line 19 assertion __CPROVER_POINTER_OBJECT(p) == __CPROVER_POINTER_OBJECT((char *)(size_t)(p + offset)): SUCCESS
[main.assertion.6] line 20 assertion __CPROVER_POINTER_OBJECT(p + offset) == __CPROVER_POINTER_OBJECT((char *)(size_t)(p + offset)): SUCCESS
[main.assertion.7] line 21 assertion __CPROVER_POINTER_OFFSET(p + offset) == __CPROVER_POINTER_OFFSET((char *)(size_t)(p + offset)): SUCCESS
[main.assertion.8] line 25 assertion __CPROVER_POINTER_OBJECT(p) == __CPROVER_POINTER_OBJECT((char *)r): SUCCESS
[main.assertion.9] line 26 assertion __CPROVER_POINTER_OBJECT(p + offset) == __CPROVER_POINTER_OBJECT((char *)r): SUCCESS
[main.assertion.10] line 27 assertion __CPROVER_POINTER_OFFSET(p + offset) == __CPROVER_POINTER_OFFSET((char *)r): FAILURE

** 2 of 18 failed (2 iterations)
VERIFICATION FAILED

CBMC version: 5.93.0
Operating system:
Exact command line resulting in the issue: cbmc --pointer-overflow-check --signed-overflow-check --unsigned-overflow-check main.c
What behaviour did you expect: pointer overflow checks fail
What happened instead: pointer overflow checks succeed

[thomasspriggs]

--malloc-fail-assert can be used to switch on the assertions for the size passed to malloc. Alternatively if the code under analysis includes error handling for null returns from malloc, then you can use --malloc-fail-null to return a null from malloc instead of failing the assert in the model of malloc.

@remi-delmas-3000 Can you confirm whether one or more of the already existing malloc command line arguments resolves this issue for you. For reference with version 6 we are currently discussing switching the appropriate malloc checks on by default rather than leaving them off by default.

[remi-delmas-3000]

@thomasspriggs switching on malloc-fail-null by default is the right thing to do.

However --malloc-fail-assert silently imposes some constraints on variables used as malloc arguments and can effectively hide problems in downstream code:

int main() {
    size_t size;
    char *p = malloc(size);

    if (size > __CPROVER_max_malloc_size) {
       // a bug that depends on the value of size_t
        assert(0);
    }

    if (!p) {
        return 1;
    }
    /// we should only assume that `size <= __CPROVER_max_malloc_size` holds from here
  return 0;
}

with --malloc-fail-assert, the assert(0) below is unreachable even though no constraint is explicitly added to size in the code.

with --malloc-fail-null, it is falsifiable as expected.