Merge branch 'qemu_7_2' into qemu_8_1 · eurecom-s3/symqemu@23e570b (original) (raw)
``
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, 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
`+
`
``
81
`` +
and you can even run SymQEMU with symcc_fuzzing_helper for hybrid fuzzing: 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
`
``
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.
`