How to verify a pointer from an external interface?

[zpzigi754]

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 can I remove that remaining failure?
Also, I wonder that treating the passed pointer with __CPROVER_assume(__CPROVER_DYNAMIC_OBJECT(p)); is okay.

CBMC version: cbmc-5.77.0
Operating system: Ubuntu 20.04

[tautschnig]

I'd say there are three possible avenues:

1. Use contracts, and specifically __CPROVER_is_fresh. See https://diffblue.github.io/cbmc/contracts-memory-predicates.html.
2. Manually generate a harness that builds an object to whatever the appropriate assumptions. See https://model-checking.github.io/cbmc-training/cbmc/overview/proof-harnesses.html#allocating-data.
3. Automatically generate a harness using goto-harness. See https://diffblue.github.io/cbmc/cprover-manual/md_goto_harness.html.

Would any of these address your problem? Else you may have to provide us with a bit more detail. (Also to be noted: CBMC does not currently feature an object factory that will lazily create objects on an as-needed basis, which perhaps is what you were trying to use.)

[zpzigi754]

@tautschnig, thank you a lot for the useful reference! It really helped.

I think that the first suggestion (__CPROVER_is_fresh) seems the more appropriate one in my situation. However, __CPROVER_is_fresh does not affect the result (invalid pointer), maybe because it can only be used in a function contract.

I've reduced my problem into a minimal one for kani input.

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

extern "C" {
    fn ffi_CPROVER_is_fresh(address: usize, size: usize);
    fn ffi_CPROVER_DYNAMIC_OBJECT(p: usize);
}

fn entry(a0: usize) -> Result<usize, ()> {
    unsafe { ffi_CPROVER_is_fresh(a0, core::mem::size_of::<Context>()) };
    unsafe { ffi_CPROVER_DYNAMIC_OBJECT(a0) };

    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 ret = entry(r0);
}

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

# stub64.c
struct Unit ffi_CPROVER_is_fresh(unsigned long address, unsigned long size) {
    __CPROVER_assume(__CPROVER_is_fresh(address, size));
}

struct Unit ffi_CPROVER_DYNAMIC_OBJECT(unsigned long p) {
    __CPROVER_assume(__CPROVER_DYNAMIC_OBJECT(p));
}

with the command cargo kani --enable-unstable --no-undefined-function-checks --c-lib stub64.c.

The below is the generated c file for cbmc (--gen-c).

struct Context
{
  // len
  unsigned int len;
};

struct () ffi_CPROVER_DYNAMIC_OBJECT(unsigned long int p)
{
  __CPROVER_assume(IS_DYNAMIC_OBJECT((const void *)p));
}

struct () ffi_CPROVER_is_fresh(unsigned long int address, unsigned long int size)
{
  __CPROVER_bool return_value___CPROVER_is_fresh=__CPROVER_is_fresh((const void *)address, size);
  __CPROVER_assume(return_value___CPROVER_is_fresh);
}

struct core::result::Result<usize, ()> entry(unsigned long int a0)
{
  struct core::result::Result<usize, ()> var_0;
  struct () var_2;
  unsigned long int var_3;
  unsigned long int var_4;
  struct () var_5;
  unsigned long int var_6;
  struct Context *ctx;
  unsigned long int var_8;
  _Bool var_9;
  unsigned int var_10;

bb0:
  ;
  var_3 = a0;
  var_4=core::mem::size_of::<Context>();

bb1:
  ;
  ffi_CPROVER_is_fresh(var_3, var_4);

bb2:
  ;
  var_6 = a0;
  ffi_CPROVER_DYNAMIC_OBJECT(var_6);

bb3:
  ;
  var_8 = a0;
  ctx = (struct Context *)var_8;
  var_10 = ctx->len;                        // this is the violating condition
  var_9 = var_10 > 10;
  if(!(var_9 == 0))
  {
    goto bb4;

  bb4:
    ;
    var_0 = nondet_1();
    var_0.case = 1;
    goto bb6;
  }


bb5:
  ;
  var_0 = nondet_1();
  var_0.cases.Ok.0 = 0;
  var_0.case = 0;

bb6:
  ;
  return var_0;
}

struct () main(void)
{
  struct () var_0;
  unsigned long int r0;
  struct core::result::Result<usize, ()> ret;
  unsigned long int var_3;

bb0:
  ;
  r0=kani::any::<usize>();

bb1:
  ;
  var_3 = r0;
  ret=entry(var_3);

bb2:
  ;
  return Void();
}

[tautschnig]

Yes, __CPROVER_is_fresh will only be useable in the context of function contracts. It might be best to create an issue against Kani to discuss how we might make this work with Rust/Kani.

[zpzigi754]

Thank you for the suggestion. I've created an issue on kani, too.