[klee-dev] KLEE on ASAN-enabled binaries

[Alexandre Adamski]

> This won't work properly I'm afraid. When compiling with ASan a bunch
> of extra calls are emitted to the sanitizer runtime libraries that are
> part of project compiler-rt. KLEE doesn't
> have an implementation for these so attempting to call these from
> within KLEE will fail.

I came to the same conclusion after trying to make it work for a whole
day. But I now I know precisely why it won't work so I can stop trying.

> I have to ask though. Why would you want to use KLEE on "ASan-ified"
> LLVM IR? KLEE already detects the kind of memory errors that ASan can
> find.

I actually thought that using KLEE on ASanified IR would enable it to
detect more memory issues. But if that is wrong, then I don't need to
care about ASAN at all.

Thank you for your detailed answer.

On 22/06/2017 01:22, Dan Liew wrote:
> On 19 June 2017 at 15:48, Alexandre Adamski <aadamski at quarkslab.com> wrote:
>> Hello there,
>>
>> I was wondering: it is possible to use KLEE on a binary compiled with
>> AddressSanitizer? Obviously using WLLVM to get the LLVM IR.
> This won't work properly I'm afraid. When compiling with ASan a bunch
> of extra calls are emitted to the sanitizer runtime libraries that are
> part of project compiler-rt. KLEE doesn't
> have an implementation for these so attempting to call these from
> within KLEE will fail.
>
> Even if the runtime issue was fixed there's also the problem of ASan's
> shadow memory. I'm not sure how well KLEE would cope with having this.
>
> I have to ask though. Why would you want to use KLEE on "ASan-ified"
> LLVM IR? KLEE already detects the kind of memory errors that ASan can
> find.
>
> On they other using like UBSan makes sense because KLEE can't catch
> all the issues UBSan can catch. Support for a small subset of UBSan
> runtime calls is already present in KLEE and more can be easily added.