S2E Question (about execute klee)

[bamiiii]

hello

I have a question about S2E, so I contacted you. I understood that the function of S2E is to let Concrete Execution do Qemu and Symbolic Execution do in Klee. But, how does Klee's Symbolic Environment get runtime information (global variables, etc.) of the path Qemu ran? Klee starts at the midpoint and I would like to know how to synchronize the previous Runtime information.

thank you

[vitalych]

KLEE as used in S2E doesn't know anything about the program's variables. It doesn't even know what program is running. All it does is interpret a stream of x86 instructions translated to LLVM. The LLVM bitcode you will see is a representation of machine instructions. That bitcode operates on emulated physical memory and CPU registers.

[bamiiii]

Thank you for your reply. However, the paper states that Qemu's Runtime data has been made available to Klee. Our project also aims to enable the Virtual Simulator to synchronize runtime data (Memory, Register, etc.) with Klee.

https://llvm.org/pubs/2009-06-HotDep-SymbolicExec.pdf (Selective Symbolic Execution) "The key element that makes S2E practical is our shared representation of machine state, used jointly by QEMU and KLEE. The original QEMU virtual machine manages the state of the virtual CPU, VMphysical memory, and VMdevices. KLEE operates on roughly the same type of state, but uses different data structures. We modified QEMU to use KLEE’s state store, such that the symbolic domain (KLEE) can be kept synchronized with the concrete one (QEMU) with no copying. The concrete state can now be forked whenever required by the symbolic execution. By operating directly on the VM’s physical memory (instead of the guest OS’ virtual memory), S2E can seamlessly support IPC and shared memory both within and between the concrete and symbolic domains. Zero-copy and the direct representation of physical memory sets S2E apart from Bitscope [2]."

[vitalych]

Yes, the paper is correct. KLEE operates on physical memory and cpu registers. These are stored in memory objects like any other variable that KLEE would operate on.

[bamiiii]

I think that technique is very good. We are similarly trying to run Klee while sharing the Virtual Simulator's memory area. I am trying to find out how the S2E researchers implemented it in the documentation. Is there any document or code that I can refer to?

[vitalych]

There is no documentation for that unfortunately, you need to look at the code. You can also read the TOCS paper about it, it's more detailed than the asplos paper.

[bamiiii]

I am referring to "http://s2e.systems/docs/". Where can I find the TOCS documentation you mentioned?

[vitalych]

In the list of publications at the bottom of the page

[bamiiii]

Thanks for the kind explanation. I will try to read and understand the documentation. But can I leave a question about the code later?

[vitalych]

Closing for now. Any general questions should be sent to the s2e-dev mailing list.