Comparison with other tools and frameworks

This page situates GREASE in the landscape of similar program analysis tools. These comparisons mostly aim to highlight which tools might be relevant for a given use-case rather than provide apples-to-apples comparisons of similar features. We have limited experience with (and correspondingly, limited understanding of) many of the tools listed here.

GREASE focuses on providing an out-of-the-box under-constrained symbolic execution tool that allows analysts to find and fix bugs. The tool provides a command line interface that allows engineers to directly symbolically execute arbitrary functions within a target binary or LLVM program and find bugs. This capability arises from a focus on scalable and relatively automated techniques (under-constrained symbolic execution), and the use of a generic symbolic execution framework and memory model that enables support for both binaries and LLVM programs, and wrapping these capabilities in an easy to use interface.

Below we highlight some general categories of tools that offer points of comparison.

• Binary analysis frameworks: angr, Macaw, BAP, and binsec. These frameworks are typically libraries that provide core binary analysis capabilities. Example capabilities include disassembly, control flow recovery, lifting and simplification, variable recovery, and type inference. Frameworks often include symbolic semantics for some intermediate representation. Macaw and angr both support forward symbolic execution of binaries from an entrypoint. This approach on its own suffers from path explosion in complex programs, typically requiring the user to configure the analysis in some way for programs of moderate scale. In binary analysis frameworks, this configuration is typically done by configuring the library manually with some interesting state and direction which requires expert analysis. These frameworks are also limited to performing analysis directly on a binary, preventing these tools from taking advantage of additional structure provided by source code (for instance types and segmented memory models). These frameworks, however, are a key component of building a tool like GREASE that can perform underconstrained symbolic execution on binaries. GREASE uses Macaw as the underlying binary analysis framework, which handles code recovery and symbolic semantics.

• Source analyzers/symbolic execution engines: KLEE performs forward symbolic execution on LLVM bitcode. Compared to binary analysis tools, performing analysis on LLVM IR allows KLEE to use more efficient memory models that split memory into separate abstract objects. Unfortunately, the tight integration of KLEE with LLVM means that KLEE cannot perform analysis on binaries. The tool also suffers from path explosion on large programs when exploring from an entrypoint.

• Source-level under-constrained symbolic execution engines: UC-Crux and UC-KLEE perform under-constrained symbolic execution on LLVM IR, enabling automated symbolic execution of arbitrary functions within a target binary with minimal configuration. Due to the use of LLVM, these tools are limited to programs where the source code is available and can be compiled to LLVM bitcode or a whole program lifting to LLVM.

• Fuzzers: Fuzzers like AFL, AFL++, and LibAFL exercise a program by generating random inputs targeting a given harness. An advantage of fuzzers is that they provide concrete inputs that trigger a given bug from defined harnesses. Sufficiently constrained harnesses are less likely to report false positives than under-constrained symbolic execution. Fuzzers also can sometimes explore deeper paths (with less breadth) than symbolic execution given precise seed inputs, because concrete inputs limit fanout. Unfortunately, using fuzzers requires defining a harness that transforms bytes into valid input for a target function. Lack of sufficiently broad fuzzing harnesses is often a constraining factor in project coverage. Under-constrained symbolic execution, on the other hand, can be targeted at an arbitrary function in a target program without prior configuration. The inferred preconditions effectively act as an automatically generated harness for the target function. Additionally, symbolic execution can achieve greater breadth by directly exploring and solving for paths that fuzzers would struggle to generate random inputs for (e.g. specific strings or arithmetic checks). Specialized fuzzing techniques can help fuzzers discover inputs that exercise hard to reach paths (e.g. TraceCMP), however, in general many complex branch conditions can block fuzzers.