Why did S2E choose Klee as symbolic execution backend?

[Riyad Parvez]

Hi,

S2E dynamically translates x86 to llvm IR for symbolic execution using Klee. FuzzBall: https://github.com/bitblaze-fuzzball/fuzzball does symbolic execution on x86 binary. So if S2E used fuzzball for symbolic execution, there won't be overhead for x86 to llvm IR dynamic translation. My question is why did S2E chose Klee instead of FuzzBall?

Thanks

[Vitaly Chipounov]

Hi,

This is a very good question.  S2E is based on QEMU in order to be able to do full-system symbolic execution. It was therefore natural to leverage QEMU's dynamic binary translator and its own IR (rather than using some other translator or IR like Vine). In principle, S2E could directly interpret QEMU's IR without using LLVM/KLEE. However, this would prevent S2E from symbolically executing more complex instructions. The DBT generates calls to helpers when it encounters instructions that are hard to translate (e.g., memory access, divisions, etc.). Helpers are bits of C code that emulate the behavior of complex instructions (e.g., see op_helper.c). It is much easier to compile these C helpers to LLVM and use an off-the-shelf execution engine like KLEE.

It is true that generating LLVM from x86 adds overhead. What we could do is use QEMU's TCI backend instead of LLVM. But we'd still need LLVM and KLEE to execute the helpers (unless we write a compiler to turn the helpers into TCI code).

Vitaly

--
--
You received this message because you are a member of the S2E Developer Forum.
To post to this group, send email to s2e...@googlegroups.com
To unsubscribe from this group, send email to s2e-dev+u...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/s2e-dev

---
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.