under constrained symbolic execution

[Zoe Patrick]

Hi all, I wonder if s2e supports under constrained symbolic execution - similar to UC-KLEE. If not, any place suggested to be modified?

[Vitaly Chipounov]

Hi,

S2E does not currently support under constrained symbolic execution as implemented in UC-KLEE. There are quite a few challenges to implement it:

- Unlike KLEE, S2E does not have any type information about the program, this is a problem for lazy input initialization. You will have to think about how to do it for binaries, perhaps with the help of debug information if available.
- S2E runs by default an entire VM, which makes it awkward to run individual functions in isolation. That's fairly simple to solve though, e.g., with PyKVM [1] , which allows you to run small bits of binary code without any OS.

If you have source code available, it makes more sense to use UC-KLEE than S2E in my opinion. More details about your project would be needed to make a proper choice.

Vitaly

[1] https://github.com/S2E/PyKVM

On 2/27/21 9:02 AM, Zoe Patrick wrote:

Hi all, I wonder if s2e supports under constrained symbolic execution - similar to UC-KLEE. If not, any place suggested to be modified? --
--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/47dcc938-a352-4d3d-91a7-df575dc9e2fdn%40googlegroups.com.