[klee-dev] KLEE on ASAN-enabled binaries

[Dan Liew]

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.