Add support for non-deterministic pointer

[zpzigi754]

Requested feature: assuming the validity of pointers
Use case: system verification

Let's say that an object is allocated in one place (place A) and its pointer is passed through an external interface (e.g., user-kernel boundary) to an another place (place B). In this case where place B cannot keep track of place A's objects, how can place B assume that the passed pointer is valid?

If I try to use the passed pointer directly, it generates a series of dereference failure such as

Failed Checks: dereference failure: pointer NULL
Failed Checks: dereference failure: pointer invalid
Failed Checks: dereference failure: deallocated dynamic object
Failed Checks: dereference failure: dead object
Failed Checks: dereference failure: pointer outside object bounds
Failed Checks: dereference failure: invalid integer address

If I treat the passed pointer as dynamic object with __CPROVER_assume(__CPROVER_DYNAMIC_OBJECT(p));,
one failure still remains.

Failed Checks: dereference failure: pointer outside object bounds

How could I remove that remaining failure?

Test case:

# main.rs
pub struct Context {
    pub len: u32,
}

extern "C" {
    fn ffi_CPROVER_DYNAMIC_OBJECT(p: usize);
}

fn entry(a0: usize) -> Result<usize, ()> {
    unsafe { ffi_CPROVER_DYNAMIC_OBJECT(a0) };     // without this, more pointer-related errors would be generated

    let ctx = a0 as *mut Context;
    unsafe {
        if (*ctx).len > 10 {                // this is the violating condition
            return Err(());
        }
    }
    Ok((0))
}

#[kani::proof]
#[kani::unwind(64)]
fn main() {
    let r0 = kani::any();      // let's say that this value is passed from an external interface (e.g., hardware)
                               // and we want to assume the pointer's validity after some sanity checks 
    let ret = entry(r0);
}

To run the harness with the CPROVER functions, I've used the below stub

# stub64.c
struct Unit ffi_CPROVER_DYNAMIC_OBJECT(unsigned long p) {
    __CPROVER_assume(__CPROVER_DYNAMIC_OBJECT(p));
}

with the command cargo kani --enable-unstable --c-lib stub64.c.

[zhassan-aws]

@remi-delmas-3000 @tautschnig

My understanding is that __CPROVER_is_fresh was introduced for this purpose, but looks like it cannot be used outside of contracts?

[zpzigi754]

In my trial, using __CPROVER_is_fresh outside of contracts didn't work.

[feliperodri]

__CPROVER_is_fresh was only designed to be used inside function contracts. @zhassan-aws @zpzigi754

You can see documentation for __CPROVER_is_fresh here.

I'm not sure what you are trying to achieve with ffi_CPROVER_DYNAMIC_OBJECT either. CBMC needs an allocation using malloc for every pointer. CBMC doesn't allow assumptions about pointer allocations. I think what you want is to design a function that allocates a0 using malloc.

cc. @tautschnig

[zhassan-aws]

You can also perform the pointer allocation in the harness, e.g.

use std::alloc::{alloc, dealloc, Layout};

pub struct Context {
    pub len: u32,
}

fn entry(a0: usize) -> Result<usize, ()> {
    let ctx = a0 as *mut Context;
    unsafe {
        if (*ctx).len > 10 {
            // this is the violating condition
            return Err(());
        }
    }
    Ok(0)
}

#[kani::proof]
#[kani::unwind(64)]
fn main() {
    let layout = Layout::new::<Context>();
    let ptr = unsafe { alloc(layout) };
    unsafe {
        (*(ptr as *mut Context)).len = kani::any();
    }
    let r0 = ptr as usize;
    //let r0 = kani::any();      // let's say that this value is passed from an external interface (e.g., hardware)
    //                           // and we want to assume the pointer's validity after some sanity checks
    let ret = entry(r0);
    unsafe {
        dealloc(ptr, layout);
    }
}

Does this achieve what you're looking for?

[zpzigi754]

@zhassan-aws, thank you a lot for the concrete example.
I guess that the suggestion looks similar to one of the alternative I have been using (assigning a local object in the harness).

pub struct Context {
    pub len: u32,
}

fn entry(a0: usize) -> Result<usize, ()> {
    let ctx = a0 as *mut Context;
    unsafe {
        if (*ctx).len > 10 {
            // this is the violating condition
            return Err(());
        }
    }
    Ok(0)
}

#[kani::proof]
#[kani::unwind(64)]
fn main() {
    let mut ctx = Context {
        len: kani::any(),
    };
    let r0 = &mut ctx as *mut Context as usize;
    let ret = entry(r0);
}

One problem in either using the local assignment or using alloc() is that it uses the object allocated from the receiver (B), not the object allocated from the sender (A). I think that assuming the validity of the passed object (pointer) is a bit different in semantic.

[zpzigi754]

__CPROVER_is_fresh was only designed to be used inside function contracts. @zhassan-aws @zpzigi754

You can see documentation for __CPROVER_is_fresh here.

I'm not sure what you are trying to achieve with ffi_CPROVER_DYNAMIC_OBJECT either. CBMC needs an allocation using malloc for every pointer. CBMC doesn't allow assumptions about pointer allocations. I think what you want is to design a function that allocates a0 using malloc.

cc. @tautschnig

Thank you for the comment and the reference. What I want is giving an assumption about the pointer allocations, which might be against the CBMC's general discipline about dealing with pointers. Using malloc() could be a good option to use, but I hesitate using it because in my opinion it is semantically different.

[zhassan-aws]

I guess that the suggestion looks similar to one of the alternative I have been using (assigning a local object in the harness).

Yes, the only difference is that in one, the pointer points to the stack (local variable), and in the other, the pointer points to the heap.

I think that assuming the validity of the passed object (pointer) is a bit different in semantic.

Can you clarify the semantics you're trying to achieve? Are you looking to create a pointer whose value itself is arbitrary? Is a model of the Sender included in the program?

[zpzigi754]

Can you clarify the semantics you're trying to achieve? Are you looking to create a pointer whose value itself is arbitrary? Is a model of the Sender included in the program?

Sure. Creating a pointer whose value itself is arbitrary is exactly what I want. The model of the Sender is not included in the program.

The below is the semantics I have in mind.

[semantics]

• the target object should be valid (accessible) for the entire lifetime of the harness or a user-specified scope.
• the target object should not be overwrapped with any other existing or future allocated objects
• the target object should be readable and also could be writable with an additional option
• the target object's location should be arbitrary

[optional]

• the target object is actually in a different address space (different heap space)

[zhassan-aws]

I see, thanks for the clarification. AFAIK, this cannot be achieved from Kani today as CBMC manages the addresses that are given to pointers. Some of the semantics you mention are achieved by __CPROVER_is_fresh though, so it might be possible through CBMC's contracts support.

CC @remi-delmas-3000 @tautschnig