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.)
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
$ git submodule update --init
$ mkdir build
$ cd build
$ cmake -G Ninja -DQSYM_BACKEND=ON ..
$ ninjaNext, 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
$ makeThis 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.
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.)
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.
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.