On-Demand Symbolic Execution
In this demo, we show that MOSE can automatically
migrate applications (along with the guest VM) from QEMU/KVM to S2E and
then begin symbolic analysis in S2E. The demo application first runs
concretely to draw a garden on the screen; then it can follow two
possible code paths (one path draws a bunny and the other path draws a
truck), depending on the value of a control variable. We mark the
control variable as symbolic, in order for S2E to automatically explore
both code paths. For more
information please refer to our ACSAC'15 paper [1].
Watch the live demo by clicking here. Source code of the program used in the demo.
Paper:
Jinpeng Wei, Lok Yan, and Muhammad Azizul Hakim. "MOSE: Live Migration Based On-the-Fly Software Emulation". Proceedings of the 31st Annual Computer Security Applications Conference (ACSAC 2015), pages 221–230. Download (529 KB). Acceptance rate: 47/193 = 24.4%.