SymQEMU: Compilation-based symbolic execution for binaries

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
$ 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.

Owner
Stand-alone projects developed by eurecom-s3. Make sure to also visit https://github.com/avatarone and https://github.com/avatartwo
null
Comments
  • recipe for target 'tcg/tcg.o' failed

    recipe for target 'tcg/tcg.o' failed

    I got an error when compiling symqume, and I searched google but no luck. Thanks!

    make[1]: Leaving directory '/home/ubuntu/sym/symqume/symqemu/slirp' LEX convert-dtsv0-lexer.lex.c make[1]: flex: Command not found BISON dtc-parser.tab.c make[1]: bison: Command not found LEX dtc-lexer.lex.c make[1]: flex: Command not found CC alpha-softmmu/tcg/tcg.o In file included from /usr/include/sched.h:29:0, from /usr/include/pthread.h:23, from /usr/include/glib-2.0/glib/deprecated/gthread.h:128, from /usr/include/glib-2.0/glib.h:108, from /home/ubuntu/sym/symqume/symqemu/include/glib-compat.h:32, from /home/ubuntu/sym/symqume/symqemu/include/qemu/osdep.h:140, from /home/ubuntu/sym/symqume/symqemu/tcg/tcg.c:28: /home/ubuntu/sym/symqume/symqemu/tcg/tcg.c: In function ‘tcg_context_init’: /home/ubuntu/sym/symqume/symqemu/tcg/tcg.c:1000:9: error: ‘ArchCPU {aka struct AlphaCPU}’ has no member named ‘env_exprs’ offsetof(ArchCPU, env_exprs) - offsetof(ArchCPU, env), "env"); ^ /home/ubuntu/sym/symqume/symqemu/rules.mak:69: recipe for target 'tcg/tcg.o' failed

  • GPL-v3-or-later license on new files is incompatible with GPL-v2-only license of some existing QEMU files

    GPL-v3-or-later license on new files is incompatible with GPL-v2-only license of some existing QEMU files

    Hi; it looks like you've licensed the new files you've added as GPL-v3-or-later (eg accel/tcg/tcg-runtime-sym.c). Unfortunately the GPLv3 is not compatible with the GPLv2, and some existing parts of QEMU are licensed as GPLv2-only (not v2-or-later) (eg util/qemu-sockets.c).

    I'm guessing this was unintentional -- the easiest fix would be for you to relicense the code you've added as GPL-v2-or-later.

  • nil pointer of _sym_expr

    nil pointer of _sym_expr

    I'm currently reading the source code of symqemu to understand how it works by printing some information about the instrumented symbolic expressions.

    // In accel/tcg/tcg-runtime-sym.c
    // Here I try to print arg1_expr and arg2_expr
    static void *sym_setcond_internal(CPUArchState *env,
                                      uint64_t arg1, void *arg1_expr,
                                      uint64_t arg2, void *arg2_expr,
                                      int32_t cond, uint64_t result,
                                      uint8_t result_bits)
    {
        printf("[debug] In Runtime: pc:0x%lx,expr1:%p,expr2:%p\n",get_pc(env),arg1_expr,arg2_expr);
        BINARY_HELPER_ENSURE_EXPRESSIONS;
        printf("[debug] calling sym_setcond_internal...success!\n");
        printf("[debug] After ensure_expr: expr1:%p,expr2:%p\n",arg1_expr,arg2_expr);
        printf("arg1 expr:%s\n",_sym_expr_to_string(arg1_expr));
        printf("arg2 expr:%s\n",_sym_expr_to_string(arg2_expr));
    ...
    

    However, when I run the modified symqemu on arbitrary binary, I noticed there are lots of nil pointers:

    image

    I wonder why would that happen? What does it mean when a sym_expr is nil? Does it mean that symqemu fails to build symbolic expressions for some variables in tcg ir?

  • sym_load_guest_internal does not distinguish signed and unsigned values

    sym_load_guest_internal does not distinguish signed and unsigned values

    We found that the movsx assembly instruction is not correctly translated by syqemu. More specifically, the movsx istruction copies the contents of the source operand to the destination operand with sign extension, however, the translated tcg ops conduct a zero extension, as shown below:

    // g_26 is an int8_t variable 
    // the value of g_26 is 0xae
    0x40126D: movsx   r9d, g_26
    // will be translated into -->
     ---- 000000000040126d 0000000000000018
     movi_i64 tmp2_expr,$0x0
     movi_i64 tmp2,$0x404044
     qemu_ld_i64 tmp0,tmp2,sb,0
     movi_i64 tmp12_expr,$0x0
     movi_i64 tmp12,$0x0
     movi_i64 tmp13_expr,$0x0
     movi_i64 tmp13,$0x1
     call sym_load_guest_i64,$0x1,$1,tmp0_expr,env,tmp2,tmp2_expr,tmp13,tmp12
     movi_i64 tmp12_expr,$0x0
     movi_i64 tmp12,$0x4
     call sym_zext,$0x5,$1,r9_expr,tmp0_expr,tmp12
     ext32u_i64 r9,tmp0
    
    

    The sym_zext and ext32u_i64 at the end is inconsitent with the semantic of movsx instruction and could lead to inaccurate symbolic constraints.

    After cheking the source code of symqemu, we found that the sym_load_guest_internal function does not distinguish between the signed value and the unsigned value and it will zero extend the loaded value whenever the load_length is not equal to result_length. This behavior is unusual and potentially buggy.

  • The idv/idiv instruction is not handled correctly

    The idv/idiv instruction is not handled correctly

    We found a possible bug while using symqemu to execute following program:

    #include <unistd.h>
    #include "csmith.h"
    /* --- GLOBAL VARIABLES --- */
    static uint16_t g_5[4] = {2,2,6,2};
    static int16_t g_81 = 5;
    static int32_t g_318 = 6;
    /* --- FORWARD DECLARATIONS --- */
    static uint32_t  func_1();
    static uint8_t  func_2(int16_t  p_3, uint16_t  p_4);
    
    static uint32_t  func_1()
    { /* block id 0 */
        int32_t *l_317 = &g_318;
        *l_317 = func_2(g_5, g_5[3]) != 0;
    }
    static uint8_t  func_2(int16_t  p_3, uint16_t  p_4)
    { /* block id 1 */
        if (g_5[3])
        { /* block id 3 */
            int32_t l_152[7][2] ;
            l_152[6][0] = 0 > (5 % (0 , p_4) != g_81);
        }
    }
    /* 
     */
    void  main ()
    {
        read(STDIN_FILENO, &g_5, sizeof(g_5));
        read(STDIN_FILENO, &g_81, sizeof(g_81));
        read(STDIN_FILENO, &g_318, sizeof(g_318));
        int print_hash_value = 0;
        func_1();
        exit(0);
    }
    

    If we compile this code with clang-10, the % operation at line 21 will be trasnlated into idiv assembly instruction.

    .text:0000000000401210 55                                      push    rbp
    .text:0000000000401211 48 89 E5                                mov     rbp, rsp
    .text:0000000000401214 66 89 7D FC                             mov     [rbp+var_4], di
    .text:0000000000401218 66 89 75 FA                             mov     [rbp+var_6], si
    .text:000000000040121C 66 83 3C 25 3E 40 40 00+                cmp     word_40403E, 0
    .text:0000000000401225 0F 84 3D 00 00 00                       jz      loc_401268
    .text:000000000040122B 31 C0                                   xor     eax, eax
    .text:000000000040122D 0F B7 4D FA                             movzx   ecx, [rbp+var_6]
    .text:0000000000401231 BA 05 00 00 00                          mov     edx, 5
    .text:0000000000401236 89 45 BC                                mov     [rbp+var_44], eax
    .text:0000000000401239 89 D0                                   mov     eax, edx
    .text:000000000040123B 99                                      cdq
    .text:000000000040123C F7 F9                                   idiv    ecx
    .text:000000000040123E 0F BF 0C 25 40 40 40 00                 movsx   ecx, g_81
    .text:0000000000401246 39 CA                                   cmp     edx, ecx
    .text:0000000000401248 40 0F 95 C6                             setnz   sil
    .text:000000000040124C 40 80 E6 01                             and     sil, 1
    .text:0000000000401250 40 0F B6 CE                             movzx   ecx, sil
    .text:0000000000401254 8B 55 BC                                mov     edx, [rbp+var_44]
    .text:0000000000401257 39 CA                                   cmp     edx, ecx
    .text:0000000000401259 40 0F 9F C6                             setnle  sil
    .text:000000000040125D 40 80 E6 01                             and     sil, 1
    .text:0000000000401261 40 0F B6 CE                             movzx   ecx, sil
    .text:0000000000401265 89 4D F0                                mov     [rbp+var_10], ecx
    

    However, we noticed that the idiv instruction will be translated into a function call to idivl_EAX by QEMU (see the translation), and this kind of translation is not handled by symqemu, i.e., the divisor and dividend are treated as concrete values, the tcg_gen_div_i32 function defined at tcg-op.c is not used.

    For example, the above idiv ecx instruction will be converted to following tcg ops by symqemu:

    ...
    
    ---- 000000000040123b 0000000000000031
     movi_i64 tmp12,$0x4                      pref=0x40
     call sym_sext,$0x5,$1,tmp0_expr,rax_expr,tmp12  dead: 1 2  pref=none
     movi_i64 tmp12_expr,$0x0                 pref=0x2
     movi_i64 tmp12,$0x1f                     pref=0x4
     call sym_arithmetic_shift_right_i64,$0x5,$1,tmp0_expr,rdx,tmp0_expr,tmp12,tmp12_expr  dead: 1 2 3 4  pref=none
     movi_i64 tmp12,$0x4                      pref=0x40
     call sym_zext,$0x5,$1,rdx_expr,tmp0_expr,tmp12  sync: 0  dead: 0 1 2  pref=none
     movi_i64 rdx,$0x0                        sync: 0  dead: 0  pref=0xffff
    
     ---- 000000000040123c 0000000000000031
     call idivl_EAX,$0x0,$0,env,rcx           dead: 0 1
    
     ---- 000000000040123e 0000000000000031
     movi_i64 tmp2_expr,$0x0                  pref=0xf038
     movi_i64 tmp2,$0x404040                  pref=0xf038
     qemu_ld_i64 tmp0,tmp2,lesw,0             pref=0xf038
     movi_i64 tmp12,$0x0                      pref=0x100
     movi_i64 tmp13,$0x2                      pref=0x2
     call sym_load_guest_i64,$0x1,$1,tmp0_expr,env,tmp2,tmp2_expr,tmp13,tmp12  dead: 2 3 4 5  pref=none
     movi_i64 tmp12,$0x4                      pref=0x40
     call sym_zext,$0x5,$1,rcx_expr,tmp0_expr,tmp12  dead: 1 2  pref=none
     ext32u_i64 rcx,tmp0                      dead: 1  pref=0xf03c
    
     ...
    

    The rdx will be updated by idivl_EAX, but the rdx_expr is not updated, so the symbolic chain is broken, and some variables become constant in constraints generated by symqemu.

    The same issue exists for the div instruction.

  • Missing arithmetic operations in constraints

    Missing arithmetic operations in constraints

    Hi, we tried to execute a simple program with symqemu:

    #include <unistd.h>
    #include <stdint.h>
    
    static int8_t g_36 = 0;
    static uint16_t g_431 = 3;
    
    static int16_t  func_20();
    
    static int32_t  func_1()
    { 
        int32_t l_458 = 4;
        l_458 = func_20(2, g_36 ^ (- 56 * g_431) % (uint32_t)-1L) != (g_431 >> 2 < 2 < 0 && 5);
    }
    
    static int16_t  func_20(int32_t  p_21, uint32_t  p_22)
    {
        return p_22;
    }
    
    int main () {
        read(STDIN_FILENO, &g_36, sizeof(g_36));
        read(STDIN_FILENO, &g_431, sizeof(g_431));
        func_1();
    }
    

    However, we found that given the input where g_36 = 0 and g_431 = 0, the generated constraint were different from what we expected:

    // command: command: cat test0.input | ./symqemu/build_simple/x86_64-linux-user/symqemu-x86_64 testcase.out
    (set-logic QF_AUFBV)
    (declare-fun g_431$0 () (_ BitVec 8))
    (declare-fun g_431$1 () (_ BitVec 8))
    (declare-fun g_36$0 () (_ BitVec 8))
    // assert (g_431 >> 2 < 2)
    (assert (let ((a!1 (concat ((_ extract 31 0)
                         (bvashr (concat #x0000 g_431$1 g_431$0 #x00000000)
                                 #x0000000000000022))
                       #x00000000)))
      (not (bvsle #x0000000000000002 (bvashr a!1 #x0000000000000020)))))
    // assert (g_431 >> 2 < 2 >= 0)
    (assert (let ((a!1 (concat ((_ extract 31 0)
                         (bvashr (concat #x0000 g_431$1 g_431$0 #x00000000)
                                 #x0000000000000022))
                       #x00000000)))
    (let ((a!2 (concat #b0000000000000000000000000000000
                       (ite (bvsle #x0000000000000002
                                   (bvashr a!1 #x0000000000000020))
                            #b0
                            #b1)
                       #x00000000)))
      (bvsle #x0000000000000000 (bvashr a!2 #x0000000000000020)))))
    // cannot understand the following constraints regarding g_36
    // no multiplication and modules operations are found
    (assert (let ((a!1 (bvashr (concat #xff
                               ((_ extract 7 7) g_36$0)
                               (bvnot ((_ extract 6 6) g_36$0))
                               ((_ extract 5 5) g_36$0)
                               (bvnot ((_ extract 4 3) g_36$0))
                               ((_ extract 2 0) g_36$0)
                               #x000000000000)
                       #x0000000000000030)))
    (let ((a!2 ((_ extract 31 0)
                 (bvashr (concat ((_ extract 15 0) a!1) #x000000000000)
                         #x0000000000000030))))
      (not (= a!2 #x00000000)))))
    (check-sat)
    (exit)
    

    For example, we cannot find the corresponding multiplication operation and modulus operation in the constraint. Can you kindly explain why? Is this as expected or a bug?

    Further, I logged the result of each cmp instruction. When given the input g_36 = 1 and g_431 = 0, the executable takes exactly the same branches at each cmp instruction, however, the generated constraints are not the same as above.

    // command: cat test3.input | ./symqemu/build_simple/x86_64-linux-user/symqemu-x86_64 testcase.out
    (set-logic QF_AUFBV)
    (declare-fun g_431$0 () (_ BitVec 8))
    (declare-fun g_431$1 () (_ BitVec 8))
    (declare-fun g_36$0 () (_ BitVec 8))
    // assert (g_431 >> 2 < 2)
    (assert (let ((a!1 (concat ((_ extract 31 0)
                         (bvashr (concat #x0000 g_431$1 g_431$0 #x00000000)
                                 #x0000000000000022))
                       #x00000000)))
      (not (bvsle #x0000000000000002 (bvashr a!1 #x0000000000000020)))))
    // assert (g_431 >> 2 < 2 >= 0)
    (assert (let ((a!1 (concat ((_ extract 31 0)
                         (bvashr (concat #x0000 g_431$1 g_431$0 #x00000000)
                                 #x0000000000000022))
                       #x00000000)))
    (let ((a!2 (concat #b0000000000000000000000000000000
                       (ite (bvsle #x0000000000000002
                                   (bvashr a!1 #x0000000000000020))
                            #b0
                            #b1)
                       #x00000000)))
      (bvsle #x0000000000000000 (bvashr a!2 #x0000000000000020)))))
    // not the same as above, even always take the same branch
    (assert (let ((a!1 (concat ((_ extract 15 0)
                         (bvashr (concat #x00 g_36$0 #x000000000000)
                                 #x0000000000000030))
                       #x000000000000)))
      (not (= ((_ extract 31 0) (bvashr a!1 #x0000000000000030)) #x00000000))))
    (check-sat)
    (exit)
    

    I'm wondering if symqemu mis-handles the multiplication operation and modulus operation.

    The source code is compiled with clang-10 with option -O0. The compiled executable file and inputs to generated the above constraints are attached. output-186.zip

    Thanks.

  • wrong symbolic branch address used in backend

    wrong symbolic branch address used in backend

    Hi,

    I noticed that when invoking get_pc(env) at sym_setcond_internal. The result of get_pc(env) is the old pc from the previous tb. I tried to update. Could you help me to verify my fix at https://github.com/sgzeng/symqemu/commit/405f4329f51ffe8a88fc2e8b5306a8572ec089dc Thanks!

  • wrong basic block address used in backend

    wrong basic block address used in backend

    Hi,

    In include/exec/gen-icount.h, I noticed that the value passed to gen_helper_sym_notify_block is the address of the TB pointer. I'm wondering if using the simulated TB address would make more sense. Could you help me to verify my fix at: https://github.com/sgzeng/symqemu/commit/1bc3860c3b50710ecbd28857217679c591ce828c

C++-based high-performance parallel environment execution engine for general RL environments.
C++-based high-performance parallel environment execution engine for general RL environments.

EnvPool is a highly parallel reinforcement learning environment execution engine which significantly outperforms existing environment executors. With

Aug 17, 2022
Kokkos C++ Performance Portability Programming EcoSystem: The Programming Model - Parallel Execution and Memory Abstraction

Kokkos: Core Libraries Kokkos Core implements a programming model in C++ for writing performance portable applications targeting all major HPC platfor

Aug 10, 2022
Powerful multi-threaded coroutine dispatcher and parallel execution engine

Quantum Library : A scalable C++ coroutine framework Quantum is a full-featured and powerful C++ framework build on top of the Boost coroutine library

Jul 25, 2022
Exploration of x86-64 ISA using speculative execution.

Haruspex /həˈrʌspeks/ A religious official in ancient Rome who predicted the future or interpreted the meaning of events by examining the insides of b

Aug 8, 2022
Termite-jobs - Fast, multiplatform fiber based job dispatcher based on Naughty Dogs' GDC2015 talk.

NOTE This library is obsolete and may contain bugs. For maintained version checkout sx library. until I rip it from there and make a proper single-hea

Jan 9, 2022
OpenCL based GPU accelerated SPH fluid simulation library

libclsph An OpenCL based GPU accelerated SPH fluid simulation library Can I see it in action? Demo #1 Demo #2 Why? Libclsph was created to explore the

Jul 27, 2022
checkedthreads: no race condition goes unnoticed! Simple API, automatic load balancing, Valgrind-based checking

checkedthreads checkedthreads is a fork-join parallelism framework for C and C++ providing: Automated race detection using debugging schedulers and Va

Jul 27, 2022
C++20 coroutines-based cooperative multitasking library

?? Coop Coop is a C++20 coroutines-based library to support cooperative multitasking in the context of a multithreaded application. The syntax will be

Aug 11, 2022
RocketOS is a Unix based OS that uses legacy BIOS and GRUB and is written in C17. It is being developed for educational purposes primarily, but it still is a serious project. It is currently in its infancy.

RocketOS What is RocketOS? RocketOS is a Unix based OS that uses legacy BIOS and GRUB and is written in C17. It is being developed for educational pur

Jul 17, 2022
A C++20 coroutine library based off asyncio
A C++20 coroutine library based off asyncio

kuro A C++20 coroutine library, somewhat modelled on Python's asyncio Requirements Kuro requires a C++20 compliant compiler and a Linux OS. Tested on

Jul 19, 2022
C++20 Coroutine-Based Synchronous Parser Combinator Library

This library contains a monadic parser type and associated combinators that can be composed to create parsers using C++20 Coroutines.

Aug 7, 2022
A C++17 message passing library based on MPI

MPL - A message passing library MPL is a message passing library written in C++17 based on the Message Passing Interface (MPI) standard. Since the C++

Jul 13, 2022
High Performance Linux C++ Network Programming Framework based on IO Multiplexing and Thread Pool

Kingpin is a C++ network programming framework based on TCP/IP + epoll + pthread, aims to implement a library for the high concurrent servers and clie

Jul 16, 2022
Arcana.cpp - Arcana.cpp is a collection of helpers and utility code for low overhead, cross platform C++ implementation of task-based asynchrony.

Arcana.cpp Arcana is a collection of general purpose C++ utilities with no code that is specific to a particular project or specialized technology are

Aug 10, 2022
Lucy job system - Fiber-based job system with extremely simple API

Lucy Job System This is outdated compared to Lumix Engine. Use that instead. Fiber-based job system with extremely simple API. It's a standalone versi

Mar 11, 2022
Elle - The Elle coroutine-based asynchronous C++ development framework.
Elle - The Elle coroutine-based asynchronous C++ development framework.

Elle, the coroutine-based asynchronous C++ development framework Elle is a collection of libraries, written in modern C++ (C++14). It contains a rich

Jul 29, 2022
DwThreadPool - A simple, header-only, dependency-free, C++ 11 based ThreadPool library.
DwThreadPool - A simple, header-only, dependency-free, C++ 11 based ThreadPool library.

dwThreadPool A simple, header-only, dependency-free, C++ 11 based ThreadPool library. Features C++ 11 Minimal Source Code Header-only No external depe

May 29, 2022
A modern thread pool implementation based on C++20
A modern thread pool implementation based on C++20

thread-pool A simple, functional thread pool implementation using pure C++20. Features Built entirely with C++20 Enqueue tasks with or without trackin

Aug 5, 2022
C++14 coroutine-based task library for games

SquidTasks Squid::Tasks is a header-only C++14 coroutine-based task library for games. Full project and source code available at https://github.com/we

Aug 16, 2022