S2E Modifications to QEMU

[Yingtong Liu]

Hi,

I am trying to make s2e work for another architecture. As a starting point, I want to look at all the s2e specific components being added on top of qemu. Since you put all the S2E specific modifications into a separated library, it's kind of hard to trace all the components you've modified to qemu, especially when I barely know nothing about qemu source code. 

Is there any source code level introduction about s2e? Like what are the exect components being modified/added to qemu and where are the functions located? Reading the paper didn't help that much since it's too vague and general. Any useful meterials or suggestions are appreciated. Thank you! 

[Vitaly Chipounov]

Hi,

Unfortunately there isn't much documentation available yet on the interals of S2E yet, you will have to read the code. Documenting the architecture in details has been on my todo list for a while, I hope to get to it at some point.
Fortunately, you do no need to read all the code. What you want is to understand for now is how libcpu and libtcg work as well as how libs2e glues them together and how it communicates with QEMU. You don't need to know much about libs2ecore and the other repos (at least not before you can actually run some ARM code in concrete mode).

So, build S2E in debug mode and use GDB to single step through various components. This way you will understand how guest code is translated, what happens with memory accesses, how are interrupts handled, etc.

To add a new architecture to libcpu, you will need to add a target-arm folder (similar to target-i386) as well as update the build system to compile the right files. You can't have multiple targets in the same binary for now.

First start by making the arm-softmmu build work. Similar to i386-softmmu, it does not link with any S2E code, it's self-contained libs2e, libtcg, libcpu.

Once this works and you can boot the guest properly, move on to arm-s2e-softmmu.

Regarding QEMU, you will need to add KVM ARM extensions to support symbolic execution. Have a look at the last few commits in the qemu repo in order to understand how it is done for i386 [1]. The changes should be minimal.

There are some ARM-related branches in different repos already, I don't know if they are firther developed [2], you might want to have a look at them.
Finally, if you want to re-use code from QEMU, make sure it is LGPL/MIT/BSD, do not use any GPL code or code that depends on GPL components.

I hope this helps.

Vitaly

[1] https://github.com/S2E/qemu/commits/v1.0.50-se
[2] https://github.com/S2E/libcpu/commits/improvement/arm-support

--
--
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+unsubscribe@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+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Yingtong Liu]

Hi Vitaly,

Thank you so much for the detailed explaination! It's much clear how to start now. 

I have another question though. Do you know which part of the source code is modifying the semantics of qemu virtual memory in order to make it can be understood by both qemu and klee? Thanks again. 

[Vitaly Chipounov]

I have no idea. Just kidding. First, some clarifications about terminology. In S2E 2.0, QEMU is just a KVM client. S2E exposes a KVM-comptible interface (note that S2E does not actually use KVM hardware virtualization). QEMU doesn't know anything about virtual memory when running in KVM mode. QEMU's job in this case is to:
- allocate chunks of memory for guest RAM and virtual devices
- register these chunks with the KVM host (which is provided by libs2e)
- handle callbacks when guest code reads/writes a device register (the KVM host will exit to QEMU if it encounters an instruction that touches virtual device memory).
In KVM mode, QEMU doesn't know it talks to S2E. Likewise, S2E doesn't know the KVM client is QEMU. QEMU and S2E are completely decoupled. The job of QEMU is to provide virtual hardware, while S2E provides (symbolic) CPU emulation. So there is no such thing as virtual memory in QEMU anymore.

Actual CPU emulation is handled by libcpu. We designed a clean interface to interface libcpu with symbolic execution engines (which could be S2E or your own if you wish to write one). The interface definition is located in [1]. You could put breakpoints at this interface to see how communication goes. In general, libcpu and KLEE are not aware of each other. They are glued together by libs2ecore.

Vitaly

[1] https://github.com/S2E/libcpu/blob/master/include/cpu/se_libcpu.h#L42

[Yingtong Liu]

Much more clear! Thank you Vitaly. I will dig more.