|
| 1 | +# SymQEMU |
| 2 | + |
| 3 | +This is SymQEMU, a binary-only symbolic executor based on QEMU and SymCC. It |
| 4 | +currently extends QEMU 7.2 and works with the most recent version of SymCC. |
| 5 | +(See README.orig for QEMU's original README file.) |
| 6 | + |
| 7 | +## How to build |
| 8 | + |
| 9 | +SymQEMU requires [SymCC](https://github.com/eurecom-s3/symcc), so please |
| 10 | +download and build SymCC first. For best results, configure it with the QSYM |
| 11 | +backend as explained in the README. For the impatient, here's a quick summary of |
| 12 | +the required steps that may or may not work on your system: |
| 13 | + |
| 14 | +``` shell |
| 15 | +$ git clone https://github.com/eurecom-s3/symcc.git |
| 16 | +$ cd symcc |
| 17 | +$ git submodule update --init |
| 18 | +$ mkdir build |
| 19 | +$ cd build |
| 20 | +$ cmake -G Ninja -DQSYM_BACKEND=ON .. |
| 21 | +$ ninja |
| 22 | +``` |
| 23 | + |
| 24 | +Next, make sure that QEMU's build dependencies are installed. Most package |
| 25 | +managers provide a command to get them, e.g., `apt build-dep qemu` on Debian and |
| 26 | +Ubuntu, or `dnf builddep qemu` on Fedora and CentOS. |
| 27 | + |
| 28 | +We've extended QEMU's configuration script to accept pointers to SymCC's source |
| 29 | +and binaries. The following invocation is known to work on Debian 10, Arch and |
| 30 | +Fedora 33: |
| 31 | + |
| 32 | +``` shell |
| 33 | + |
| 34 | +$ ../configure \ |
| 35 | + --audio-drv-list= \ |
| 36 | + --disable-sdl \ |
| 37 | + --disable-gtk \ |
| 38 | + --disable-vte \ |
| 39 | + --disable-opengl \ |
| 40 | + --disable-virglrenderer \ |
| 41 | + --disable-werror \ |
| 42 | + --target-list=x86_64-linux-user \ |
| 43 | + --symcc-source=</path/to/symcc>/sources \ |
| 44 | + --symcc-build=</path/to/symcc>/build |
| 45 | + |
| 46 | +$ make |
| 47 | +``` |
| 48 | + |
| 49 | +This will build a relatively stripped-down emulator targeting 64-bit x86 |
| 50 | +binaries. We also have experimental support for AARCH64. Working with 32-bit |
| 51 | +target architectures is possible in principle but will require a bit of work |
| 52 | +because the current implementation assumes that we can pass around host pointers |
| 53 | +in guest registers. |
| 54 | + |
| 55 | +## Running SymQEMU |
| 56 | + |
| 57 | +If you built SymQEMU as described above, the binary will be in |
| 58 | +`x86_64-linux-user/symqemu-x86_64`. For a quick test, try the following: |
| 59 | + |
| 60 | +``` shell |
| 61 | +$ mkdir /tmp/output |
| 62 | +$ echo test | x86_64-linux-user/symqemu-x86_64 /bin/cat -t - |
| 63 | +This is SymCC running with the QSYM backend |
| 64 | +Reading program input until EOF (use Ctrl+D in a terminal)... |
| 65 | +[STAT] SMT: { "solving_time": 0, "total_time": 93207 } |
| 66 | +[STAT] SMT: { "solving_time": 480 } |
| 67 | +[INFO] New testcase: /tmp/output/000000 |
| 68 | +... |
| 69 | +``` |
| 70 | +
|
| 71 | +This runs your system's `/bin/cat` with options that make it inspect each |
| 72 | +character on standard input to check whether or not it's in the non-printable |
| 73 | +range. In `/tmp/output`, the default location for test cases generated by |
| 74 | +SymQEMU, you'll find versions of the input (i.e., "test") containing |
| 75 | +non-printable characters in various positions. |
| 76 | +
|
| 77 | +This is a very basic use of symbolic execution. See SymCC's documentation for |
| 78 | +more advanced scenarios. Since SymQEMU is based on it, it understands all the |
| 79 | +same |
| 80 | +[settings](https://github.com/eurecom-s3/symcc/blob/master/docs/Configuration.txt), |
| 81 | +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 |
| 82 | +prefix the target command with `x86_64-linux-user/symqemu-x86_64`. (Note that |
| 83 | +you'll have to run AFL in QEMU mode by adding `-Q` to its command line; the |
| 84 | +fuzzing helper will automatically pick up the setting and use QEMU mode too.) |
| 85 | +
|
| 86 | +## Documentation |
| 87 | +
|
| 88 | +The [paper](http://www.s3.eurecom.fr/tools/symbolic_execution/symqemu.html) |
| 89 | +contains details on how SymQEMU works. A large part of the implementation is the |
| 90 | +run-time support in `accel/tcg/tcg-runtime-sym.{c,h}` (which delegates any |
| 91 | +actual symbolic computation to SymCC's symbolic backend), and we have modified |
| 92 | +most code-generating functions in `tcg/tcg-op.c` to emit calls to the runtime. |
| 93 | +For development, configure with `--enable-debug` for run-time assertions; there |
| 94 | +are tests for the symbolic run-time support in `tests/check-sym-runtime.c`. |
| 95 | +
|
| 96 | +## License |
| 97 | +
|
| 98 | +SymQEMU extends the QEMU emulator, and our contributions to previously existing |
| 99 | +files adopt those files' respective licenses; the files that we have added are |
| 100 | +made available under the terms of the GNU General Public License as published by |
| 101 | +the Free Software Foundation, either version 2 of the License, or (at your |
| 102 | +option) any later version. |
0 commit comments