SymQEMU

This is SymQEMU, a binary-only symbolic executor based on QEMU and SymCC. It currently extends QEMU 4.1.1 and works with the most recent version of SymCC. (See README.orig for QEMU's original README file.)

How to build

SymQEMU requires SymCC, so please download and build SymCC first. For best results, configure it with the QSYM backend as explained in the README. For the impatient, here's a quick summary of the required steps that may or may not work on your system:

$ git clone https://github.com/eurecom-s3/symcc.git
$ cd symcc
$ git submodule update --init
$ mkdir build
$ cd build
$ cmake -G Ninja -DQSYM_BACKEND=ON ..
$ ninja

Next, make sure that QEMU's build dependencies are installed. Most package managers provide a command to get them, e.g., apt build-dep qemu on Debian and Ubuntu, or dnf builddep qemu on Fedora and CentOS.

We've extended QEMU's configuration script to accept pointers to SymCC's source and binaries. The following invocation is known to work on Debian 10, Arch and Fedora 33:

$ ../configure                                                    \
      --audio-drv-list=                                           \
      --disable-bluez                                             \
      --disable-sdl                                               \
      --disable-gtk                                               \
      --disable-vte                                               \
      --disable-opengl                                            \
      --disable-virglrenderer                                     \
      --disable-werror                                            \
      --target-list=x86_64-linux-user                             \
      --enable-capstone=git                                       \
      --symcc-source=</path/to/symcc>/sources                     \
      --symcc-build=</path/to/symcc>/build
$ make

This will build a relatively stripped-down emulator targeting 64-bit x86 binaries. We also have experimental support for AARCH64. Working with 32-bit target architectures is possible in principle but will require a bit of work because the current implementation assumes that we can pass around host pointers in guest registers.

Running SymQEMU

If you built SymQEMU as described above, the binary will be in x86_64-linux-user/symqemu-x86_64. For a quick test, try the following:

$ mkdir /tmp/output
$ echo test | x86_64-linux-user/symqemu-x86_64 /bin/cat -t -
This is SymCC running with the QSYM backend
Reading program input until EOF (use Ctrl+D in a terminal)...
[STAT] SMT: { "solving_time": 0, "total_time": 93207 }
[STAT] SMT: { "solving_time": 480 }
[INFO] New testcase: /tmp/output/000000
...

This runs your system's /bin/cat with options that make it inspect each character on standard input to check whether or not it's in the non-printable range. In /tmp/output, the default location for test cases generated by SymQEMU, you'll find versions of the input (i.e., "test") containing non-printable characters in various positions.

This is a very basic use of symbolic execution. See SymCC's documentation for more advanced scenarios. Since SymQEMU is based on it, it understands all the same settings, and you can even run SymQEMU with symcc_fuzzing_helper for hybrid fuzzing: just prefix the target command with x86_64-linux-user/symqemu-x86_64. (Note that you'll have to run AFL in QEMU mode by adding -Q to its command line; the fuzzing helper will automatically pick up the setting and use QEMU mode too.)

Documentation

The paper contains details on how SymQEMU works. A large part of the implementation is the run-time support in accel/tcg/tcg-runtime-sym.{c,h} (which delegates any actual symbolic computation to SymCC's symbolic backend), and we have modified most code-generating functions in tcg/tcg-op.c to emit calls to the runtime. For development, configure with --enable-debug for run-time assertions; there are tests for the symbolic run-time support in tests/check-sym-runtime.c.

License

SymQEMU extends the QEMU emulator, and our contributions to previously existing files adopt those files' respective licenses; the files that we have added are made available under the terms of the GNU General Public License as published by the Free Software Foundation, either version 2 of the License, or (at your option) any later version.