Re: [klee-dev] Question on use-after-free detection.

[Frank Busse]

Hi,

On Sat, 2 Jan 2021 19:31:02 +
Cristian Cadar  wrote:

> You are right, KLEE doesn't catch this use-after-free bug currently,
> as it doesn't implement a quarantine.

Just a remark: KLEE's deterministic allocation mode (--allocate-determ)
implements an el cheapo arena allocator and just increments addresses.
Hence, in that mode it finds the bug.


Kind regards,

Frank

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Question on use-after-free detection.

[Cristian Cadar]

You are right, KLEE doesn't catch this use-after-free bug currently, as 
it doesn't implement a quarantine.  It wouldn't it be too hard to add 
this though (you might want to refer to the ASan paper for details).


Best,
Cristian

On 02/01/2021 18:16, Yoonseok Ko wrote:

Hello,

  I have an additional question on this comment: 
https://github.com/klee/klee/issues/1254 



  @ccadar mentioned that KLEE already finds the kind of bugs that 
AddressSanitizer detects, but I don't clearly understand.


  For example, consider the following code fragment:
```
  int *o1 = (int*)malloc(4);
  free(o1);
  int *o2 = (int*)malloc(4);
  *o1 = 10; /* use-after-free */
```

The code uses the memory block allocated to the object 'o1' after it is 
freed (at line 2).

ASan simply detects and reports it as 'use-after-free'.

But, KLEE does not report an alarm when the second `malloc` allocates 
the same memory block as allocated by the first `malloc`.
Since KLEE simply relies on the standard malloc semantics, the same 
memory block can be allocated.
And, when there is a memory access, KLEE only checks whether the 
dereferenced memory block is *currently* valid.

So, the last line `*o1 = 10` is valid because `o2 == o1`.

Do you support any other mechanism to catch such an issue?

Thank you.

Best regards,
Yoonseok


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] Question on use-after-free detection.

[Yoonseok Ko]

Hello,

 I have an additional question on this comment: 
https://github.com/klee/klee/issues/1254 


 @ccadar mentioned that KLEE already finds the kind of bugs that 
AddressSanitizer detects, but I don't clearly understand.

 For example, consider the following code fragment:
```
 int *o1 = (int*)malloc(4);
 free(o1);
 int *o2 = (int*)malloc(4);
 *o1 = 10; /* use-after-free */
```

The code uses the memory block allocated to the object 'o1' after it is freed 
(at line 2).
ASan simply detects and reports it as 'use-after-free'.

But, KLEE does not report an alarm when the second `malloc` allocates the same 
memory block as allocated by the first `malloc`.
Since KLEE simply relies on the standard malloc semantics, the same memory 
block can be allocated.
And, when there is a memory access, KLEE only checks whether the dereferenced 
memory block is *currently* valid.
So, the last line `*o1 = 10` is valid because `o2 == o1`.

Do you support any other mechanism to catch such an issue?

Thank you.

Best regards,
Yoonseok

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev