CBMC (Dynamic memory allocations ----- Malloc issues)

[sa]

Hello everyone,

I am trying to work on different allocation strategy for malloc in C. 

When i used CBMC i figured out that it uses a big chunck of memory and allocates memory one after the other to each object or variable

incase it is out of memory then it starts rellocating from beginning.

It would be really helpful if somebody can guide me on the following...

 

1. I want find a way so that i can allocate memory to a interger pointer *p1 and *q1 using nondet_int(); 

2. and want to perform a check if the memory allocated to *p1 is between range (0 to 255)

3. and for q between p-q <4 && q between range (0 to 255)

4. and also check if p=q if i free p after allocation and then allocate q.

Thanks in advance... 

[Michael Tautschnig]

Hello,

On Mon, Mar 27, 2017 at 1:39:49 -0700, sa wrote:
[...]

> It would be really helpful if somebody can guide me on the following...
>
> 1. I want find a way so that i can allocate memory to a interger pointer
> *p1 and *q1 using nondet_int();

Is it memory allocation or initialisation that you are asking about? If you want
to allocate memory, where it supposed to be allocated from - the stack or the
heap?

> 2. and want to perform a check if the memory allocated to *p1 is between
> range (0 to 255)
> 3. and for q between p-q <4 && q between range (0 to 255)
> 4. and also check if p=q if i free p after allocation and then allocate q.

Are you asking about the memory allocation (the address) or the value?

Best,
Michael

[Martin Nyx Brain]

On Mon, 2017-03-27 at 01:39 -0700, sa wrote:
> Hello everyone,
>
> I am trying to work on different allocation strategy for malloc in C.

Depending on what you are trying to achieve, may I recommend Doug Lea's
malloc as a reasonable starting place.

> When i used CBMC i figured out that it uses a big chunck of memory and
> allocates memory one after the other to each object or variable
> incase it is out of memory then it starts rellocating from beginning.

Is this CBMC or your allocator?

> It would be really helpful if somebody can guide me on the following...
>
> 1. I want find a way so that i can allocate memory to a interger pointer
> *p1 and *q1 using nondet_int();

nondet_int isn't a CBMC built-in; you can make it do whatever you want.
The important things to understand are:

A. If CBMC doesn't have a body for a function, it's return value will be
non-deterministic (and CBMC will print a warning).

B. If the function name starts with "nondet" the warning is skipped.

> 2. and want to perform a check if the memory allocated to *p1 is between
> range (0 to 255)
> 3. and for q between p-q <4 && q between range (0 to 255)
> 4. and also check if p=q if i free p after allocation and then allocate q.

If you want to allocate memory in your model I would recommend using
malloc / free as you will then get leak checking and the rest of the
memory allocation checks.

Cheers,
- Martin

[sa]

Dear Michael

Firstly thanks for replying and asking these questions...

> It would be really helpful if somebody can guide me on the following...
>  
> 1. I want find a way so that i can allocate memory to a interger pointer
> *p1 and *q1 using nondet_int();

Is it memory allocation or initialisation that you are asking about? If you want
to allocate memory, where it supposed to be allocated from - the stack or the
heap?

 i need to allocate memory to integer pointers using malloc. I need to allocate from heap and not the stack.

 

> 2. and want to perform a check if the memory allocated to *p1 is between
> range (0 to 255)
> 3. and for q between p-q <4 && q between range (0 to 255)
> 4. and also check if p=q if i free p after allocation and then allocate q.

Are you asking about the memory allocation (the address) or the value?

 

I need to allocate memory from heap and then check the starting address and ending address of heap and see how where memory is allocated to p and then to q.

(different scenarios like

1. allocate for p and q with free and check how its allocated

2. allocate for p and then free p and allocate for q and check if the memory allocated for p and q was same

3. allocate memory for p and allocate memory for q then free p and allocate again for p1 and check if p==p1

 ) 

[sa]

Dear Martin,

Thanks for ur suggestions and i have answered ur questions so that it would be clear and you can guide me through this topic.

On Monday, 27 March 2017 13:38:14 UTC+2, martin...@cs.ox.ac.uk wrote:

On Mon, 2017-03-27 at 01:39 -0700, sa wrote:
> Hello everyone,
>
> I am trying to work on different allocation strategy for malloc in C.

Depending on what you are trying to achieve, may I recommend Doug Lea's
malloc as a reasonable starting place.

I will surely read and try to understand this...  

> When i used CBMC i figured out that it uses a big chunck of memory and
> allocates memory one after the other to each object or variable
> incase it is out of memory then it starts rellocating from beginning.

Is this CBMC or your allocator?

its CBMC's allocator that i m trying to use.. 

> It would be really helpful if somebody can guide me on the following...
>  
> 1. I want find a way so that i can allocate memory to a interger pointer
> *p1 and *q1 using nondet_int();

nondet_int isn't a CBMC built-in; you can make it do whatever you want.
The important things to understand are:

A. If CBMC doesn't have a body for a function, it's return value will be
non-deterministic (and CBMC will print a warning).

B. If the function name starts with "nondet" the warning is skipped.

> 2. and want to perform a check if the memory allocated to *p1 is between
> range (0 to 255)
> 3. and for q between p-q <4 && q between range (0 to 255)
> 4. and also check if p=q if i free p after allocation and then allocate q.

If you want to allocate memory in your model I would recommend using
malloc / free as you will then get leak checking and the rest of the
memory allocation checks.

My aim here is to write some formula's or constraints like

(1. for p1 using malloc, anywhere in the heap  ---------p1 belongs between 0 to 255

 2. p2 using malloc ------p1-p2 <4 && p2 Belongs between  0 to255)

and implement them so that the memory allocated using malloc is random and not as obvious as it is in CBMC. 

If i have not mistaken then CBMC just allocates memory chunk after chunk when i use malloc, i want to make this allocation random so that vulnerability doesnt occur. Please let me know if there is a way to do this.

Thanks in advance...

Regards,

Sa

[Martin Nyx Brain]

On Mon, 2017-03-27 at 05:26 -0700, sa wrote:
> Dear Martin,
<snip>

> > > 2. and want to perform a check if the memory allocated to *p1 is between
> > > range (0 to 255)
> > > 3. and for q between p-q <4 && q between range (0 to 255)
> > > 4. and also check if p=q if i free p after allocation and then allocate
> > q.
> >
> > If you want to allocate memory in your model I would recommend using
> > malloc / free as you will then get leak checking and the rest of the
> > memory allocation checks.
> >

> > *My aim here is to write some formula's or constraints like*
> *(1. for p1 using malloc, anywhere in the heap ---------p1 belongs between
> 0 to 255*
> * 2. p2 using malloc ------p1-p2 <4 && p2 Belongs **between ** 0 to255)*

Pointer arithmetic like this is supported but malloc will return
non-overlapping segments so I'm not sure this can occur.

> *and implement them so that the memory allocated using malloc is random and
> not as obvious as it is in CBMC. *
> *If i have not mistaken then CBMC just allocates memory chunk after chunk

> when i use malloc, i want to make this allocation random so that
> vulnerability doesnt occur. Please let me know if there is a way to do

> this.*
>
> *Thanks in advance...*

So the way memory allocation is modelled in CPROVER is that it uses a
number of 'blocks' each of which is writable at a (large) number of
offsets. Each call to malloc (__CPROVE_malloc specifically) creates a
new one of these. Reads and writes need to know the block and offset.
So that pointer arithmetic works easily and so that some type unsafe
access to pointers work, we pack these into pointer values. This will
give the impression of sequentially allocated blocks while in practice
the memory model doesn't assume a contiguous address space. It's not an
ideal system but it works reasonably well. Errors that could result in
memory "corruption" can be caught with --bounds-check and
--pointer-check.

Your question seems to be about the particular bit patterns used for
pointers. I'm not sure these are actually accessible in ISO C without
undefined behaviour. Thus programs that depend on these are likely to
be non-portable (at best) or unstable (at worst) given things like ASLR.

Changing the bit pattern we use would be possible but might require
changes at the encoding level which is not simple. Alternatively,
allocate one block with malloc and then hand out parts of it as you
want, giving the non-deterministic behaviour you want.

Cheers,
- Martin

[sa]

Dear Martin,

Thanks for your explanation, will try the things that you have suggested and get back :)...

Regards,

Sa

[Martin Nyx Brain]

On Tue, 2017-03-28 at 07:02 -0700, sa wrote:
> Dear Martin,
>

> Thanks for your explanation, will try the things that you have suggested
> and get back :)...

I guess the key point is that we had people want to prove properties
about the specific (bit) values of pointers, so we fix them in a
relatively simple fashion.

Cheers,
- Martin