Open zpzigi754 opened 1 year ago
@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?
In my trial, using __CPROVER_is_fresh
outside of contracts didn't work.
__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
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?
@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.
__CPROVER_is_fresh
was only designed to be used inside function contracts. @zhassan-aws @zpzigi754You 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 usingmalloc
for every pointer. CBMC doesn't allow assumptions about pointer allocations. I think what you want is to design a function that allocatesa0
usingmalloc
.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.
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?
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]
[optional]
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
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
If I treat the passed pointer as dynamic object with
__CPROVER_assume(__CPROVER_DYNAMIC_OBJECT(p));
, one failure still remains.How could I remove that remaining failure?
Test case:
To run the harness with the CPROVER functions, I've used the below stub
with the command
cargo kani --enable-unstable --c-lib stub64.c
.