^       —————.   —.—  .     .  —.—  .     .  .—————    .    .
   ———      |     |   |   |     |   |   ||    |  |         |    |
  —(o)—     |     |   |   |     |   |   |  |  |  |————     '————|
 ———————    |     |   |    |   |    |   |    ||  |              |
—————————   —————'   —'—     '     —'—  '     '  '—————         '

This page provides complementary material for the paper submitted to QRS 2020 .

Benchmarks

In this section input programs for the evaluation part of the paper are provided. After extracting files from the archive, please read included QRS.README on how to interpret test cases and other provided files: tests.

Toolchain sources

In our submission we mention several tools that are used in our approach or later in evalution. Here source code for used tools with simple build/usage instructions are provided.

McSema & Remill

To build McSema and Remill from sources consult their READMEs (depending whether you also chose to build dependencies manually it can be rather long process).

In our evaluation we used McSema with Dyninst frontend and since we slightly modified it when dealing with global constructors, we recommend to use it if possible (in every other aspect IDA Pro frontend should do equivalent job, sometimes maybe even better).

Since McSema is designed to work with multiple frontends, the decompilation process is done in two commands (first converts binary -> CFG, second CFG -> LLVM IR):

$ mcsema-dyninst-disass \
    --output main.cfg --binary main.out \
    --std_defs $MCSEMA_SOURCE_DIR/tools/mcsema-disass/defs/linux.txt
$ mcsema-lift \
    --unfold --divine \
    --explicit_args --arch amd64 --os linux --cfg main.cfg \
    --abi_libraries abi.bc \
    --output lifted.bc

To get bitcode in more SSA friendly form described in the paper only required options are --unfold and --explicit_args + all the option required by McSema itself (e.g --arch).

However we added some extra options compared to upstream McSema that further improve the IR for verification:

--divine, --klee produces bitcode for given verifier

--ctors handles global ctors/dtors in more SSA friendly manner (requires Dyninst frontend)

--dbg_info tries to annotate the bitcode with !dbg metadata. Unfortunately this option does not work very well, and often instruction may end up on one line above/below the original one, which hinders some test cases (error is find on different line than expected even though it is correct).

DIVINE

To build from the provided source, you will need some prerequisites, namely a C++11 compiler such as reasonably recent GCC (>= 4.9) or Clang (>= 3.2), make, CMake (>= 3.2), libedit, perl, and about 12GB of disk space and 4GB RAM.

You should extract the archive and then run make divine in its main directory. This should build DIVINE into _build.release/tools subdirectory by default. For more details, please refer to the manual.

To verify decompiled bitcode extra command line flag --mcsema is required, since the decompiled bitcode contains a lot of unusual constructs (although still valid IR) and DIVINE needs to be more careful when doing LLVM transformations.

For example to verify lifted.bc with symbolic domain following command can be used:

$ divine check --lamp symbolic --mcsema lifted.bc

To refine indirect calls one must first run refine command - it accepts almost identical arguments as check, therefore to remove indirect calls the following invocation may be used

$ divine refine --refinement rewirecalls --output refined.compiled.bc compiled.bc

Please note that the bitcode does not have to be decompiled, the refinement works on any bitcode. Although if the bitcode is decompiled, --mcsema still needs to be used.

To invoke the test suite used in the paper please follow the QRS.README inside the archive, as it is slightly more complex process.

KLEE

Current upstream KLEE should work as well, (in the time of evaluation the one extra functionality required was not yet merged, however it is now). Since big part of chosen benchmarks use some non-trivial external function, uclibc (see KLEE documentation) was used as its libc library.

There are no special build or usage instructions; decompiled bitcode can be passed the same way as compiled one.