# symqemu

**Repository Path**: boss-ding/symqemu

## Basic Information

- **Project Name**: symqemu
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: GPL-2.0
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2023-11-02
- **Last Updated**: 2024-05-30

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# 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](https://github.com/eurecom-s3/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:

``` shell
$ 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:

``` shell
$ ../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:

``` shell
$ 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](https://github.com/eurecom-s3/symcc/blob/master/docs/Configuration.txt),
and you can even run SymQEMU with `symcc_fuzzing_helper` for [hybrid fuzzing](https://github.com/eurecom-s3/symcc/blob/master/docs/Fuzzing.txt): 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](http://www.s3.eurecom.fr/tools/symbolic_execution/symqemu.html)
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.