[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 <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

-------------- next part --------------
HTML attachment scrubbed and removed