SE4VM-QTest

SE4VM-QTest is able to detect device hanging flaw casuse by infinite loops in the implementation of virtual devices as well as generate and demonstra te the problematic inputs and their damages to VM environments.

This is achieved by combining the ability of partialy execute the selected code provided by QEMU's QTest framework and the S2E symbolic execution engine

QTEST

QTest Can be used directly to test part of the qemu implementation without running a full guest. Achieved by intercepting the init process of QEMU and replace the normal execution routine with test module's run routine.

We modified QTest framework to make it work with symbolic execution engine and created test cases based on QTest framework to find device hanging flaws in QEMU's virtual devices.

S2E symbolic execution engine

We chose S2E as the symbolic execution engine. S2E is a platform for writing tools that analyze the properties and behavior of software systems. S2E helps make analyses based on symbolic execution practical for large software that runs in real environments, without requiring explicit modeling of these environments.

Test framework

Compilation and Running

• Testing Environment

  The testing environment setup consists of compiling the symbolic execution engine and building the QEMU binary to be tested.

  Checkout S2E from https://github.com/dslab-epfl/s2e and build S2E following the documentation https://github.com/dslab-epfl/s2e/blob/master/docs/BuildingS2E.rst

  Our QTest and test cases are based on a modified version of QEMU-1.7.2, you can download the tar ball from here: QEMU-1.7.2.tgz

• Execute the test

  • Get the s2e management scripts from git repo

    git clone -b s2e-scripts --single-branch https://github.com/kangliuga/SE4VM

  • Get the S2E guest image

    git clone -b s2e-scripts --single-branch https://github.com/kangliuga/SE4VM

  • Start the Test engine with the management script

    

  • Inside s2e guest image, run our qtest test case for ne2000 device

    

• Results

  • This screenshot shows the framework is injecting symbolic values to 3 of the registers of the ne2000 device

    

  • The framework together with the test case is able to detect device hanging flaws casuesd by infinite loop in the ne2000 virtual device