Overview

grease is a CLI tool that analyzes binaries using under-constrained symbolic execution. grease supports analysis of ELF executables or shared objects containing ARMv7l, PowerPC, or x86_64 code. grease can also analyze LLVM bitcode.

GREASE logo

Demo

Consider the following function derived from libpng. Can you spot the bug?1

void /* PRIVATE */
png_check_chunk_length(png_const_structrp png_ptr, const unsigned int length)
{
   png_alloc_size_t limit = PNG_UINT_31_MAX;

# ifdef PNG_SET_USER_LIMITS_SUPPORTED
   if (png_ptr->user_chunk_malloc_max > 0 &&
       png_ptr->user_chunk_malloc_max < limit)
      limit = png_ptr->user_chunk_malloc_max;
# elif PNG_USER_CHUNK_MALLOC_MAX > 0
   if (PNG_USER_CHUNK_MALLOC_MAX < limit)
      limit = PNG_USER_CHUNK_MALLOC_MAX;
# endif
   if (png_ptr->chunk_name == png_IDAT)
   {
      png_alloc_size_t idat_limit = PNG_UINT_31_MAX;
      size_t row_factor =
         (png_ptr->width * png_ptr->channels * (png_ptr->bit_depth > 8? 2: 1)
          + 1 + (png_ptr->interlaced? 6: 0));
      if (png_ptr->height > PNG_UINT_32_MAX/row_factor)
         idat_limit=PNG_UINT_31_MAX;
      else
         idat_limit = png_ptr->height * row_factor;
      row_factor = row_factor > 32566? 32566 : row_factor;
      idat_limit += 6 + 5*(idat_limit/row_factor+1); /* zlib+deflate overhead */
      idat_limit=idat_limit < PNG_UINT_31_MAX? idat_limit : PNG_UINT_31_MAX;
      limit = limit < idat_limit? idat_limit : limit;
   }
   // ...
}

grease can:

$ clang test.c -o test
$ grease test

Finished analyzing 'png_check_chunk_length'. Possible bug(s):

At 0x100011bd:
div: denominator was zero
Concretized arguments:

rcx: 0000000000000000
rdx: 0000000000000000
rsi: 0000000000000000
rdi: 000000+0000000000000000
r8: 0000000000000000
r9: 0000000000000000
r10: 0000000000000000

000000: 54 41 44 49 01 00 00 00 f9 ff ff ff 00 00 00 00 00 80

This output says that png_check_chunk_length will divide by zero when rdi points to an allocation holding the bytes 54 41 44 .... Indeed, if we add the following main function:

int main() {
  char data[] = {0x54, 0x41, 0x44, 0x49, 0xf9, 0x00, 0x00, 0x00, 0x01, 0xb7, 0x3e, 0x9b, 0x00, 0x00, 0x00, 0x00, 0x00, 0x80};
  png_check_chunk_length((png_const_structrp)data, 0);
  return 0;
}

We see exactly what grease described:

$ clang test.c -o test
$ ./test
Floating point exception (core dumped)
1

This test-case is based on CVE-2018-13785. The complete example and accompanying license and copyright notice are available at tests/refine/neg/libpng-cve-2018-13785/test.c in the GREASE source repository.

Algorithm

The analysis performed is roughly the following:

  • The binary is disassembled and converted into a control-flow graph IR.
  • grease symbolically simulates the entrypoint using the most general possible preconditions (all registers hold fresh symbolic variables).
  • If an out-of-bounds memory read or write occurs, the precondition is refined by growing allocated / initialized memory. For example, if an out-of-bounds read occurs at an offset of the address in r8, we refine the precondition to make sure that r8 points to a region of initialized memory big enough to contain the offset.
  • This process of simulation and refinement repeats itself until either (1) no errors occur (in which case we move on) or (2) errors occur and we do not have heuristics to refine based on any of the errors (in which case we concretize the arguments, report an error, and exit).
  • Now that we have found a memory layout that allows us to simulate the entrypoint without error, we instrument the control-flow graph with new instructions that encode further assertions.
  • Finally, we run the instrumented control-flow graph with the inferred memory layout precondition. If all collected assertions pass, we report that the property holds. Otherwise, we report that the property does not hold.

For more details, see Refinement.

Acknowledgements

This material is based upon work supported by the Defense Advanced Research Projects Agency under Contract No. W31P4Q-22-C-0017 and W31P4Q-23-C-0020

Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Defense Advanced Research Projects Agency or the U.S. Government.

Copyright (c) Galois, Inc. 2024.

Installation

Currently, the only supported methods of installation are to build a binary or Docker container from source.

Build a binary from source

See the developer's guide.

Build a Docker container

$ docker build . -t grease:latest

Overrides

Overrides are models of functions that can be called during symbolic execution. Overrides can be used to model the effect of external functions, e.g., functions from dynamically-linked libraries. They can also be used to replace the definitions of complex functions in the target program with simpler models.

Some overrides are built-in to grease, e.g., for some functions from libc, such as malloc. Users may also provide overrides, which take priority over both built-in overrides and functions defined in the program under analysis.

User-provided overrides are written in the Crucible S-expression syntax. Each language supported by GREASE extends this base S-expression language with additional types and operations, see macaw-symbolic-syntax for binaries and crucible-llvm-syntax for LLVM for further information about these extensions.

LLVM example

As an example, consider the following C program in the file prog.c:

#include <stdio.h>
extern void *id_ptr(void*);
int main() {
  int x;
  int *y = id_ptr(&x);
  *y = 5;
  printf("%i\n", x);
  return 0;
}

If we compile this program to LLVM and disassemble it like so:1

clang -g -emit-llvm -O1 -c -fno-discard-value-names prog.c
llvm-dis prog.bc

Then the LLVM disassembly looks something like this:

define i32 @main() {
entry:
  %x = alloca i32, align 4
  %0 = bitcast i32* %x to i8*
  %call = call i8* @id_ptr(i8* nonnull %0)
  ; -- snip --
  ret i32 0
}

; -- snip --

declare i8* @id_ptr(i8*)

Since @id_ptr is not accompanied by a definition, GREASE fails to execute this function:

grease prog.bc

-- snip --
Failed to infer precondition.

If id_ptr is supposed to be the identity function on (64-bit) pointers, we can write the following LLVM override in id_ptr.llvm.cbl:

(defun @id_ptr ((p (Ptr 64))) (Ptr 64)
  (start start:
    (return p)))

and pass it to GREASE, which can then successfully execute the target function:

grease prog.bc --overrides id_ptr.llvm.cbl

5
-- snip --
All goals passed!

Note that the --overrides flag may be passed multiple times (e.g., --overrides foo.llvm.cbl --overrides bar.llvm.cbl) to supply multiple overrides.

Override file naming conventions

While GREASE does not enforce this convention, it is strongly encouraged to name override files as follows:

  • *.armv7l.cbl for ARM overrides
  • *.llvm.cbl for LLVM overrides
  • *.ppc32.cbl for PPC32 overrides
  • *.x86.cbl for x86_64 overrides

This naming scheme matches convention that GREASE requires for simulating S-expression programs.

Each <name>.*.cbl file is required to define a function named @<name>. This is referred to as the file's public function, which is treated as an override during simulation. All other functions defined in the file are referred to as auxiliary functions. Auxiliary functions are not treated as overrides during simulation, and they are effectively private to the file that defines them.

1

The only flags that are strictly necessary here are -c and -emit-llvm, the other flags aid the readability of the LLVM code.

Overrides and forward declarations

It is possible for user-defined overrides to have forward declarations to other functions. For example, this override defines a id_ptr2 function, which invokes a forward declaration to id_ptr:

(declare @id_ptr ((p (Ptr 64))) (Ptr 64))

(defun @id_ptr2 ((p (Ptr 64))) (Ptr 64)
  (start start:
    (let res (funcall @id_ptr p))
    (return res)))

This id_ptr2 override can then be combined with the id_ptr override above like so:

grease prog.bc --overrides id_ptr.llvm.cbl --overrides id_ptr2.llvm.cbl

grease will ensure that the forward declaration to id_ptr is resolved to the public function of the same name. If grease cannot find a public function for an override named id_ptr, then grease will raise an error.

Built-in overrides

In addition to the user-defined overrides described above, GREASE also provides a number of built-in overrides that are built directly into the tool. For various reasons, these overrides are not defined using S-expression syntax. Unlike user-defined overrides, these overrides are always enabled by default, without needing the user to explicitly enable them. If a user supplies an override of the same name as a built-in override, then the user-supplied override takes precedence over the built-in override.

The following is a complete list of built-in overrides, given with C-like type signatures:

  • i8* @memcpy( i8*, i8*, size_t )
  • i8* @__memcpy_chk ( i8*, i8*, size_t, size_t )
  • i8* @memmove( i8*, i8*, size_t )
  • i8* @memset( i8*, i32, size_t )
  • i8* @__memset_chk( i8*, i32, size_t, size_t )
  • i8* @calloc( size_t, size_t )
  • i8* @realloc( i8*, size_t )
  • i8* @malloc( size_t )
  • i32 @posix_memalign( i8**, size_t, size_t )
  • void @free( i8* )
  • i32 @printf( i8*, ... )
  • i32 @__printf_chk( i32, i8*, ... )
  • i32 @putchar( i32 )
  • i32 @puts( i8* )
  • size_t @strlen( i8* )
  • double @ceil( double )
  • float @ceilf( float )
  • double @floor( double )
  • float @floorf( float )
  • float @fmaf( float, float, float )
  • double @fma( double, double, double )
  • i32 @isinf( double )
  • i32 @__isinf( double )
  • i32 @__isinff( float )
  • i32 @isnan( double )
  • i32 @__isnan( double )
  • i32 @__isnanf( float )
  • i32 @__isnand( double )
  • double @sqrt( double )
  • float @sqrtf( float )
  • double @sin( double )
  • float @sinf( float )
  • double @cos( double )
  • float @cosf( float )
  • double @tan( double )
  • float @tanf( float )
  • double @asin( double )
  • float @asinf( float )
  • double @acos( double )
  • float @acosf( float )
  • double @atan( double )
  • float @atanf( float )
  • double @sinh( double )
  • float @sinhf( float )
  • double @cosh( double )
  • float @coshf( float )
  • double @tanh( double )
  • float @tanhf( float )
  • double @asinh( double )
  • float @asinhf( float )
  • double @acosh( double )
  • float @acoshf( float )
  • double @atanh( double )
  • float @atanhf( float )
  • double @hypot( double, double )
  • float @hypotf( float, float )
  • double @atan2( double, double )
  • float @atan2f( float, float )
  • float @powf( float, float )
  • double @pow( double, double )
  • double @exp( double )
  • float @expf( float )
  • double @log( double )
  • float @logf( float )
  • double @expm1( double )
  • float @expm1f( float )
  • double @log1p( double )
  • float @log1pf( float )
  • double @exp2( double )
  • float @exp2f( float )
  • double @log2( double )
  • float @log2f( float )
  • double @exp10( double )
  • float @exp10f( float )
  • double @__exp10( double )
  • float @__exp10f( float )
  • double @log10( double )
  • float @log10f( float )
  • void @__assert_rtn( i8*, i8*, i32, i8* )
  • void @__assert_fail( i8*, i8*, i32, i8* )
  • void @abort()
  • void @exit( i32 )
  • i8* @getenv( i8* )
  • i32 @htonl( i32 )
  • i16 @htons( i16 )
  • i32 @ntohl( i32 )
  • i16 @ntohs( i16 )
  • i32 @abs( i32 )
  • i32 @labs( i32 )
  • i64 @labs( i64 )
  • i64 @llabs( i64 )
  • i32 @__cxa_atexit( void (i8*)*, i8*, i8* )

For LLVM programs (but not binaries), the following built-in overrides are also available:

  • i8* @memcpy( i8*, i8*, size_t )
  • i8* @__memcpy_chk ( i8*, i8*, size_t, size_t )
  • i8* @memmove( i8*, i8*, size_t )
  • i8* @memset( i8*, i32, size_t )
  • i8* @__memset_chk( i8*, i32, size_t, size_t )
  • i8* @calloc( size_t, size_t )
  • i8* @realloc( i8*, size_t )
  • i8* @malloc( size_t )
  • i32 @posix_memalign( i8**, size_t, size_t )
  • void @free( i8* )
  • i32 @printf( i8*, ... )
  • i32 @__printf_chk( i32, i8*, ... )
  • i32 @putchar( i32 )
  • i32 @puts( i8* )
  • size_t @strlen( i8* )
  • double @ceil( double )
  • float @ceilf( float )
  • double @floor( double )
  • float @floorf( float )
  • float @fmaf( float, float, float )
  • double @fma( double, double, double )
  • i32 @isinf( double )
  • i32 @__isinf( double )
  • i32 @__isinff( float )
  • i32 @isnan( double )
  • i32 @__isnan( double )
  • i32 @__isnanf( float )
  • i32 @__isnand( double )
  • double @sqrt( double )
  • float @sqrtf( float )
  • double @sin( double )
  • float @sinf( float )
  • double @cos( double )
  • float @cosf( float )
  • double @tan( double )
  • float @tanf( float )
  • double @asin( double )
  • float @asinf( float )
  • double @acos( double )
  • float @acosf( float )
  • double @atan( double )
  • float @atanf( float )
  • double @sinh( double )
  • float @sinhf( float )
  • double @cosh( double )
  • float @coshf( float )
  • double @tanh( double )
  • float @tanhf( float )
  • double @asinh( double )
  • float @asinhf( float )
  • double @acosh( double )
  • float @acoshf( float )
  • double @atanh( double )
  • float @atanhf( float )
  • double @hypot( double, double )
  • float @hypotf( float, float )
  • double @atan2( double, double )
  • float @atan2f( float, float )
  • float @powf( float, float )
  • double @pow( double, double )
  • double @exp( double )
  • float @expf( float )
  • double @log( double )
  • float @logf( float )
  • double @expm1( double )
  • float @expm1f( float )
  • double @log1p( double )
  • float @log1pf( float )
  • double @exp2( double )
  • float @exp2f( float )
  • double @log2( double )
  • float @log2f( float )
  • double @exp10( double )
  • float @exp10f( float )
  • double @__exp10( double )
  • float @__exp10f( float )
  • double @log10( double )
  • float @log10f( float )
  • void @__assert_rtn( i8*, i8*, i32, i8* )
  • void @__assert_fail( i8*, i8*, i32, i8* )
  • void @abort()
  • void @exit( i32 )
  • i8* @getenv( i8* )
  • i32 @htonl( i32 )
  • i16 @htons( i16 )
  • i32 @ntohl( i32 )
  • i16 @ntohs( i16 )
  • i32 @abs( i32 )
  • i32 @labs( i32 )
  • i64 @labs( i64 )
  • i64 @llabs( i64 )
  • i32 @__cxa_atexit( void (i8*)*, i8*, i8* )
  • void @llvm.lifetime.start( i64, i8* )
  • void @llvm.lifetime.end( i64, i8* )
  • void @llvm.assume ( i1 )
  • void @llvm.trap()
  • void @llvm.ubsantrap( i8 )
  • i8* @llvm.stacksave()
  • void @llvm.stackrestore( i8* )
  • void @llvm.memmove.p0i8.p0i8.i32( i8*, i8*, i32, i32, i1 )
  • void @llvm.memmove.p0i8.p0i8.i32( i8*, i8*, i32, i1 )
  • void @llvm.memmove.p0.p0.i32( ptr, ptr, i32, i1 )
  • void @llvm.memmove.p0i8.p0i8.i64( i8*, i8*, i64, i32, i1 )
  • void @llvm.memmove.p0i8.p0i8.i64( i8*, i8*, i64, i1 )
  • void @llvm.memmove.p0.p0.i64( ptr, ptr, i64, i1 )
  • void @llvm.memset.p0i8.i64( i8*, i8, i64, i32, i1 )
  • void @llvm.memset.p0i8.i64( i8*, i8, i64, i1 )
  • void @llvm.memset.p0.i64( ptr, i8, i64, i1 )
  • void @llvm.memset.p0i8.i32( i8*, i8, i32, i32, i1 )
  • void @llvm.memset.p0i8.i32( i8*, i8, i32, i1 )
  • void @llvm.memset.p0.i32( ptr, i8, i32, i1 )
  • void @llvm.memcpy.p0i8.p0i8.i32( i8*, i8*, i32, i32, i1 )
  • void @llvm.memcpy.p0i8.p0i8.i32( i8*, i8*, i32, i1 )
  • void @llvm.memcpy.p0.p0.i32( ptr, ptr, i32, i1 )
  • void @llvm.memcpy.p0i8.p0i8.i64( i8*, i8*, i64, i32, i1 )
  • void @llvm.memcpy.p0i8.p0i8.i64( i8*, i8*, i64, i1 )
  • void @llvm.memcpy.p0.p0.i64( ptr, ptr, i64, i1 )
  • i32 @llvm.objectsize.i32.p0i8( i8*, i1 )
  • i32 @llvm.objectsize.i32.p0i8( i8*, i1, i1 )
  • i32 @llvm.objectsize.i32.p0i8( i8*, i1, i1, i1 )
  • i32 @llvm.objectsize.i32.p0( ptr, i1, i1, i1 )
  • i64 @llvm.objectsize.i64.p0i8( i8*, i1 )
  • i64 @llvm.objectsize.i64.p0i8( i8*, i1, i1 )
  • i64 @llvm.objectsize.i64.p0i8( i8*, i1, i1, i1 )
  • i64 @llvm.objectsize.i64.p0( ptr, i1, i1, i1 )
  • void @llvm.prefetch.p0i8( i8*, i32, i32, i32 )
  • void @llvm.prefetch.p0( ptr, i32, i32, i32 )
  • void @llvm.prefetch( i8*, i32, i32, i32 )
  • float @llvm.copysign.f32( float, float )
  • double @llvm.copysign.f64( double, double )
  • float @llvm.fabs.f32( float )
  • double @llvm.fabs.f64( double )
  • float @llvm.ceil.f32( float )
  • double @llvm.ceil.f64( double )
  • float @llvm.floor.f32( float )
  • double @llvm.floor.f64( double )
  • float @llvm.sqrt.f32( float )
  • double @llvm.sqrt.f64( double )
  • float @llvm.sin.f32( float )
  • double @llvm.sin.f64( double )
  • float @llvm.cos.f32( float )
  • double @llvm.cos.f64( double )
  • float @llvm.pow.f32( float, float )
  • double @llvm.pow.f64( double, double )
  • float @llvm.exp.f32( float )
  • double @llvm.exp.f64( double )
  • float @llvm.log.f32( float )
  • double @llvm.log.f64( double )
  • float @llvm.exp2.f32( float )
  • double @llvm.exp2.f64( double )
  • float @llvm.log2.f32( float )
  • double @llvm.log2.f64( double )
  • float @llvm.log10.f32( float )
  • double @llvm.log10.f64( double )
  • i1 @llvm.is.fpclass.f32( float, i32 )
  • i1 @llvm.is.fpclass.f64( double, i32 )
  • float @llvm.fma.f32( float, float, float )
  • double @llvm.fma.f64( double, double, double )
  • float @llvm.fmuladd.f32( float, float, float )
  • double @llvm.fmuladd.f64( double, double, double )
  • <2 x i64> @llvm.x86.pclmulqdq(<2 x i64>, <2 x i64>, i8)
  • void @llvm.x86.sse2.storeu.dq( i8*, <16 x i8> )

For binaries (but not LLVM programs), the following built-in overrides are also available:

  • void @__stack_chk_fail()
  • void @__stack_chk_fail_local()

The types in the list above represent Crucible types according to the following schema:

  • double: (there is no syntax for this Crucible type)
  • float: (there is no syntax for this Crucible type)
  • i<N>: (Ptr <N>)
  • <<LANES> x i<N>>: (there is no syntax for this Crucible type)
  • ptr: (Ptr <word-size>)
  • size_t: (Ptr <word-size>)
  • <T>*: (Ptr <word-size>)
  • void: Unit

where <word-size> is:

  • 32 for AArch32
  • 64 for LLVM
  • 32 for PPC32
  • 64 for PPC64
  • 64 for x86_64

They may be called from user-defined overrides.

The following overrides merit a bit of discussion:

  • abort

    Terminate grease by raising an error. Note that this termination is immediate, so grease will not attempt to detect issues in any code following the call to abort.

  • free

    Free a pointer that was allocated using malloc.

  • malloc

    Allocate a fresh pointer of the given size in the underlying memory model. This pointer is assumed not to alias with any pointers allocated by previous calls to malloc.

Startup overrides

Startup overrides are a special form of override that runs before the execution of an entrypoint function. A startup override can be thought of as overriding the part of grease that creates the initial arguments that are passed to the entrypoint function before simulating it. While grease's default heuristics can often figure out the right argument values to pass to the function, there are times when it can be convenient to have finer-grained control over this process. Some examples:

  1. Triggering a bug requires an extremely large memory allocation. For instance, imagine that a bug is only triggered when a pointer argument points to an allocation of size 2^^64 bytes in size. Because grease's default heuristics increase the size of allocations one byte at a time, a grease user would have a wait a very long time in order for the heuristics to discover that the memory allocation must be of size 2^^64 (assuming that grease does not time out or trigger its recursion limit before then).

  2. Triggering a bug requires multiple arguments to be related to each other in a way that is not captured by grease's heuristics. For example, it is somewhat commonplace for C functions to pass pairs of arguments where one argument is a buffer (call it buf) and another argument is the size of buf (call it buf_sz). One would expect that the size of the allocation that buf points to would always be equal to buf_sz, but grease's heuristics do not guarantee this property: grease is liable to increase the size of buf in a way that does not respect the value of buf_sz.

In such scenarios, it can be helpful to use a startup override to carefully dictate what the initial arguments to the function should be. To do so, one can use the --symbol-startup-override SYMBOL:FILE or --address-startup-override ADDR:FILE command-line arguments. These are like --symbol and --address, respectively, except that they each take an additional FILE argument (separated from the function symbol or address by a : character) representing the path to the startup override file.

Like other forms of overrides, startup overrides are expected to be written in Crucible S-expression syntax. They must also adhere to the following constraints:

  1. There must be a function named "startup" contained in the file. The startup function will be invoked at startup right before invoking the entrypoint function with the argument values that the startup override produces.

  2. The type of the startup function has very particular requirements:

    • If the input program is a binary or a Macaw S-expression program, then startup must take a register struct as input and return a register struct as output. For example, on x86-64 the argument and result type must be X86Regs.

    • If the input program is LLVM bitcode or an LLVM S-expression program, then startup must take the same argument types as the entrypoint function, and it must return a struct containing the same argument types. For example, if the entrypoint function is an LLVM function with the type signature i8 foo(i16, i32), then the startup override must have the type (defun @startup ((x (Ptr 16)) (y (Ptr 32))) (Struct (Ptr 16) (Ptr 32)) ...).

In both cases, the arguments to the startup override consist of the "default" initial arguments that grease would normally pass directly to the entrypoint function, and the return value is what will actually be passed to the entrypoint function.

Note that:

  • Unlike other forms of overrides, startup overrides do not require their file paths to have particular naming conventions.

  • Just like how the entrypoint function can be invoked multiple times during the refinement process, the startup override can also be invoked multiple times during refinement. As a result, it is possible for the startup override to be supplied different arguments each time it is is invoked during refinement.

Usage

Prerequisites

GREASE requires one of the following SMT solvers at run-time:

  • cvc4 1.8 or greater
  • cvc5 1.0.5 or greater
  • yices 2.6.2 or greater
  • z3 4.8.14 or greater

They are already installed in the GREASE Docker image. By default, grease will default to yices unless you manually specify a solver using the --solver option.

Running a standalone binary

$ grease -- <filename>

By default, GREASE analyzes every known function in the input program. You can use one of the following flags to specify specific entrypoints:

  • --symbol: Analyze a function with a specific symbol name (e.g., main).
  • --address: Analyze a function at a specific address.
  • --{symbol,address}-startup-override: Like --{symbol,address}, but with a particular startup override. (For more information on startup overrides, see the overrides section.)
  • --core-dump: Analyze the function most likely to contain the address where the core was dumped in the supplied core dump file.

By default, GREASE will treat <filename> as an ELF file and read the ELF headers to determine whether it is AArch32, PowerPC, or x86_64. This behavior can be overridden if <filename> ends in one of the following suffixes:

  • .armv7l.elf: 32-bit ARM ELF executable
  • .ppc32.elf: 32-bit PowerPC ELF executable
  • .ppc64.elf: 64-bit PowerPC ELF executable
  • .x64.elf: x86_64 ELF executable
  • .bc: LLVM bitcode

or one of the following, which are mostly useful for GREASE developers:

  • .armv7l.cbl: 32-bit ARM CFG written in macaw-symbolic Crucible syntax
  • .ppc32.cbl: 32-bit PowerPC CFG written in macaw-symbolic Crucible syntax
  • .x64.cbl: x86_64 CFG written in macaw-symbolic Crucible syntax
  • .llvm.cbl: LLVM CFG written in crucible-llvm syntax

(Note that .ppc64.cbl files are not currently supported, as grease's 64-bit PowerPC frontend currently requires a binary in order to work. See this upstream issue for more details.)

Running the Docker image

$ docker run --rm -v "$PWD:$PWD" -w "$PWD" grease:latest <filename> --symbol <entrypoint>

Ghidra plugin

GREASE includes support for integrating with the Ghidra software reverse engineering suite via a plugin. The plugin works interfaces with a local GREASE installation and presents the results of GREASE's analysis to the user using Ghidra's graphical user interface.

Prerequisites

You will need to download Ghidra. You will also need to build a grease binary from source as described in the developers' guide.

You may optionally specify the path to your grease binary by setting the GHIDRA_GREASE_BIN environment variable. If not set, the Ghidra plugin will prompt for the path to your grease binary.

Similarly, you may optionally specify a directory containing GREASE override files by setting the GHIDRA_GREASE_OVERRIDES environment variable. If not set, the Ghidra plugin will prompt for a directory.

Plugin installation

Before starting, make sure you have installed Ghidra and built GREASE from source, as described in the "Prerequisites" section above. Then perform the following steps:

  1. In Ghidra, use CodeBrowser Script Manager -> Manage Script Directories to add the <grease>/ghidra_scripts/ path (where <grease> is the path to your grease checkout).
  2. In the Ghidra Script Manager, find grease.py and check the In Tool checkbox to add GREASE Analysis to the Tools menu.

Plugin usage

After opening a binary in Ghidra, use Tools -> GREASE Analysis to start the Ghidra plugin. If you haven't defined GHIDRA_GREASE_BIN or GHIDRA_GREASE_OVERRIDES environment variables by this point, the plugin will prompt you with a windows to locate the grease binary's location and the GREASE override directory's locations, respectively.

The plugin will then prompt you to select function(s) to analyze. After picking the function(s) of interest and clicking OK, the plugin will analyze the function(s) using GREASE and display the results graphically. For example, the screenshot below demonstrates the results of running the Ghidra plugin on a main function with an uninitialized stack read at address 0x0010113b:

GREASE Ghidra plugin example

Limitations

GREASE is subject to a variety of limitations. They can be characterized according to several criteria:

  • Are the issues fundamental, i.e., inherent to the overall approach? Or are they incidental, and could be solved given enough engineering?
  • Are they threats to correctness, i.e., could they induce GREASE to report a falsehood?
  • Are they threats to completeness, i.e., could they cause GREASE to fail to analyze (part of) a given program, or to only analyze part of its behavior?

The following table characterizes several of GREASE's limitations, which are described in more detail below.

LimitationFundamentalCorrectnessCompleteness
Path explosionYNY
k-boundingYNY
External codeYYY
Scalability of SMTYNY
Analyzing binariesYYN
AliasingNYY
Code discoveryNNY
HeuristicsNYY
Features of binariesNNY
Quirks of machine codeNNY

Fundamental limitations

The limitations described in this section are fundamental to GREASE's analysis, and are rooted in theorems in computability and complexity theory. No amount of engineering effort could result in fully general, automated solutions to these problems. However, real progress can be made by introducing heuristics for common cases, or resorting to human insight and input.

Path explosion

Like many program analyses, GREASE suffers from the path explosion problem:

path explosion is a fundamental problem that limits the scalability and/or completeness of certain kinds of program analyses, including fuzzing, symbolic execution, and path-sensitive static analysis. Path explosion refers to the fact that the number of control-flow paths in a program grows exponentially ("explodes") with an increase in program size and can even be infinite in the case of programs with unbounded loop iterations. Therefore, any program analysis that attempts to explore control-flow paths through a program will [...] have exponential runtime in the length of the program1

1

https://en.wikipedia.org/wiki/Path_explosion

GREASE's under-constrained symbolic execution (uc-symex) attempts to mitigate the impact of path explosion relative to traditional symbolic execution (symex). By starting at an arbitrary function (instead of only at main, as in traditional symex), GREASE can achieve higher coverage of the program under analysis. However, uc-symex is still subject to path explosion: it still involves exploring all control-flow paths that start at the function under analysis. In the limit (i.e., when analyzing main), this can boil down to the same problem as in traditional symex.

In practice, this means that GREASE may report a timeout when analyzing functions with complex control-flow (or functions that call such functions).

k-bounding

GREASE uses a sophisticated, bit-precise memory model with support for advanced features such as reads, writes, and copies of symbolic data with symbolic sizes, to and from symbolic pointers. However, this memory model can't express unbounded heap data-structures. For example, GREASE can't determine the behavior of a function when fed a linked list of arbitrary length, it can only analyze the behavior on linked lists with symbolic content but some fixed length. In practice, GREASE examines program behavior up to some maximum bound, an approach known in static analysis as k-bounding. The program features subject to k-bounding include data structures, loop iterations, and recursion.

Practically speaking, GREASE may report that the bound k has been exceeded when analyzing complex functions. Users may set the bound k at the command-line.

External code

Programs are not pure functions; they interact with the world. They call external libraries, interact with the kernel via syscalls, and query and manipulate with hardware devices. Not only is it infeasible to precisely model the plethora of complex systems with which a program under analysis might interface, given the precision of GREASE's analysis, it is often impractical to even soundly over- or under-approximate the behaviors of such systems.

GREASE provides precise models for a wide variety of commonly used library functions (e.g., from libc) and a limited set of Linux syscalls. However, there will always be many more that cannot be analyzed. GREASE skips such calls by default, but the user may also provide their own models where necessary in the form of overrides.

Scalability of SMT

Symbolic execution fundamentally relies on SMT solvers. Despite decades of incredible research and engineering effort, the performance of such solvers remains unpredictable from problem to problem. At Galois, we've seen performance degrade especially when reasoning about programs with heavy use of floating-point values, non-linear arithmetic, and certain patterns of memory usage.2 To mitigate these difficulties, GREASE allows users to select among many SMT solvers.

If the SMT solver fails to answer a query, GREASE reports this as a timeout and doesn't offer further results for that function.

2

In addition to these practical limitations, there’s also a more fundamental issue: SMT solvers are built to solve an NP-hard problem. Therefore, their performance can’t be uniformly good in all cases.

Analyzing binaries

GREASE operates on compiled code (binaries and LLVM). There may be bugs (e.g., undefined behavior) in the source program that the compiler has optimized away; GREASE has no means of finding such bugs.

Incidental limitations

The following limitations reflect the state of GREASE today, but considerable progress on them is likely possible with further engineering effort.

Aliasing

GREASE assumes that any two pointers reachable from a function's inputs (i.e., the values in registers/arguments) do not alias. It could likely be extended to consider such cases.

Code discovery

Code discovery consists of recovering control-flow graphs (CFGs) from disassembled machine code. This task is undecidable in general, challenging in practice, and amounts to an active area of research in the field of binary analysis. GREASE's approach is thus necessarily heuristic in nature, and could always be improved to support additional common idioms (e.g., different kinds of jump tables emitted by major compilers).

If the code discovery fails to recover a CFG, GREASE reports as much and doesn't offer further results for control-flow paths that reach the site of the failure.

Heuristics

Under-constrained symbolic execution (uc-symex) analyzes functions in isolation. As discussed above, this approach improves scalability as compared to traditional symex (by mitigating path explosion), but it comes with its own trade-offs. Crucially, it makes it difficult to say with certainty whether a behavior observed during analysis is feasible in practice. Any potential error encountered during analysis could either be a true bug, or an artifact of the analysis approach. Tools based on uc-symex have heuristics that attempt to maximize true positives and minimize false positives reported to the user. Such heuristics can generally be improved with additional investment.

Features of binaries

Binary analysis is hard. Executable formats, operating systems, ISAs, relocation types, and memory models proliferate. GREASE currently supports analysis of Linux ELF binaries for 32-bit ARM, PowerPC, and x86_64. Even within those categores, GREASE lacks support for:

Quirks of machine code

It is possible for machine code to exhibit behaviors that are not possible at the level of assembly language; GREASE cannot analyze such code. For example, GREASE doesn't support:

  • self-modifying code
  • run-time code generation (e.g., JIT compilation)
  • jumps into the "middle" of instructions

In brief

  • GREASE can only analyze code in a single thread of execution, without considering side-effects from threads or processes acting in parallel.
  • GREASE has limited support for string operations. For instance, calls to strlen will only work on concrete pointers. These operations are very difficult to handle in a performant way in full generality, as each additional character introduces a symbolic branch.
  • GREASE can't handle calls through non-concrete function pointers.
  • GREASE has a hard time with variable-arity functions.
  • GREASE cannot model heap exhaustion or overflows.
  • It's difficult to detect PLT stubs.
  • GREASE does not currently detect stack buffer overflows.
  • GREASE does not currently support code that runs before main, e.g., C's __attribute__ ((constructor)), ELF's .init/.ctors/.init_array, LLVM's @llvm.global_ctors, or Rust's _init.
  • GREASE currently does not cope well with calls to symbolic function pointers or addresses. By default, GREASE's default behavior is to skip over calls to function pointers or addresses that it cannot resolve as concrete. GREASE also includes a --error-symbolic-fun-calls command-line option that causes GREASE to error if it attempts to invoke a symbolic function call.

Memory model

GREASE builds on the Macaw and Crucible-LLVM memory models.

Background: Crucible-LLVM

In the Crucible-LLVM memory model (permalink),

Each allocation in the memory model is completely isolated from all other allocations and has a unique block identifier. Pointers into the memory model have two components: the identifier of the block they reference and an offset into that block. Note that both the identifier and the offset can be symbolic.

Said another way, the memory model is two-dimensional: One "axis" of a pointer determines which allocation (possibly allocations in the case of a symbolic block identifier) it points to, and the other "axis" is the offset within that allocation.1 For example, the null pointer is represented by the pair (0, 0x0).

Crucible-LLVM memory

Global memory

The Macaw memory model (and so, GREASE) represents a binary's address space as a single Crucible-LLVM allocation of size 0xffffffff. Pointers that appear in the binary become offsets into this allocation. For example, if the global allocation had block identifier 1, the global g was at address 0x903278, then a load from g would become a load from the Crucible-LLVM pointer (1, 0x903278).

Mutable globals

Mutable global variables are tricky:

  • If GREASE initialized mutable global variables to their initial values or to completely symbolic values, it's possible that GREASE would report "bugs" that are infeasible in practice, because the value of the global required to trigger the bug isn't actually feasible at any of the callsites to the function under analysis.
  • On the other hand, if GREASE doesn't initialize global variables at all, any loads from them (that aren't preceeded by writes made by the function under analysis or its callees) will fail. As mutable global variables are pervasive, this would lead to a significant lack of coverage.

GREASE's behavior in this regard is controlled via the --globals flag. The possible values are:

  • Initialized: Each mutable global is initialized using its initializer before analysis of the target function.
  • Symbolic: Each mutable global is initialized to a symbolic value before analysis of the target function.
  • Uninitialized: Mutable globals are left uninitialized. Reads from mutable globals will fail, causing GREASE to be unable to proceed with analysis.

The stack

GREASE represents the stack as a separate Crucible-LLVM allocation. Before symbolically executing the target function, the stack pointer is initialized to point at the end of a fairly large allocation (currently, 1 MiB). This means that GREASE assumes a standard stack discipline, namely that the stack grows downwards from high addresses to low, and functions never access memory above their stack frame (with some exceptions, which are explained below). In theory, false positives may occur if a binary overruns this stack allocation, though in practice, symbolic execution of that much code would take a considerable amount of time.

On some architectures, GREASE will allocate a small amount of space just above the stack frame to store the current function's return address (e.g., on x86-64 and PowerPC) or the back chain (e.g., PowerPC), but otherwise, GREASE will assume that functions never access memory above their stack frame. Note that because GREASE leaves most of the space above the stack frame unallocated by default, this will cause GREASE to reject programs that load function arguments that are spilled to the stack.2 In general, it is challenging to infer how many arguments a function has from analyzing raw assembly code, so GREASE does not make an effort to do so.

Instead, GREASE offers a --stack-argument-slots=<NUM> that can be used to allocate <NUM> additional stack slots above the stack frame before simulating the entrypoint function. <NUM> is 0 by default, so if you know ahead of time how many stack-spilled arguments the entrypoint function requires, you should use --stack-argument-slots to ensure that GREASE can simulate it properly. Note that in general, it is not advisable to run GREASE with a large --stack-argument-slots value. This is because if GREASE reserves more stack space than what is required to model stack-spilled arguments, then reading from the extra stack space will succeed (incorrectly) instead of resulting in an uninitialized stack read error (which is normally what is desired).

The heap

GREASE overrides the behavior of the malloc and free functions such that they interact nicely with the Crucible-LLVM memory model. Each call to malloc will generate a distinct allocation with a non-zero block identifier that is different from all other allocations in the program, including global memory. Similarly, each call to free will deallocate a Crucible-LLVM allocation.

Be mindful of the following limitations of GREASE's model of the heap:

  • There is no limit to the maximum heap size, so GREASE cannot model heap overflows.
  • Because each heap allocation is completely isolated from all other allocations, GREASE cannot model events that would arise after certain types of heap-related exploits (e.g., buffer overflows).
1

Non-pointer bitvectors (e.g. the 5 in int x = 5;) are represented the same way as pointers, but with a block identifier that’s concretely 0.

2

The number of arguments a function must have in order for it to spill some of its arguments to the stack depends on which architecture is being used. In general, the more arguments a function has, the more likely it is to spill arguments to the stack.

Refinement

Before continuing, it would be helpful to review:

This page describes the refinement algorithm in additional detail. However, it does not discuss implementation techniques, which are documented in the Haddocks.

The algorithm is similar to the corresponding functionality in UC-Crux-LLVM.

The goal of the refinement loop is to discover sufficient preconditions for the successful execution of a target function. If a memory error occurs (out-of-bounds read/write, uninitialized read, etc.), the precondition is refined using heuristics, such as expanding allocations or initializing memory.

Preconditions

The preconditions are represented as a map from registers to pointer shapes. A pointer shape consists of a sequence of pointee shapes, where a pointee shape is one of:

  • A number of uninitialized bytes
  • A number of initialized bytes
  • A pointer shape

In the initial precondition, all registers (except the instruction and stack pointers) map to an empty sequence of pointee shapes, meaning that they are not assumed to point to an allocation (i.e., they are treated as raw bitvectors).

Setting up state

Before each execution of the target function, GREASE initializes memory and registers according to the current precondition.

Memory

As described in the document on the memory model, GREASE maps the binary's address space into a single Crucible-LLVM allocation, and sets the stack pointer to the end of a separate allocation.

Registers

All registers are set to symbolic values corresponding to their shape (other than the stack and instruction pointers, which point to the end of an allocation and the beginning of the function, respectively).

For each empty pointer shape, the register is set to a fresh, symbolic value. For each non-empty pointer shape, GREASE creates a separate Crucible-LLVM allocation that is just large enough to hold all of its pointee shapes, and sets the register to a pointer to the base of that allocation. It then initializes the allocation according to the pointee shapes (which may create and initialize additional allocations, recursively).

The refinement loop

The refinement loop proceeds by initializing memory and registers according to the current precondition, then symbolically simulating the target function. If no error occurs, a sufficient precondition has been found and the refinement loop ends. If instead there is a memory error, the error is passed along to a series of heuristics. The heuristics generally:

  • Increase the size of pointee shapes (by adding uninitialized bytes at the end)
  • Turn uninitialized pointee shapes into initialized ones
  • Replace (un)initialized pointee shapes with pointer shapes

These heuristics can be disabled with the --no-heuristics flag.

Requirements

GREASE features a memory model that is capable of detecting many types of common software-related issues, such as double-frees or uninitialized stack reads. In addition to the checks that the memory model performs, GREASE users can opt into checking additional requirements that assert properties that are not covered by the memory model. The difference between a memory model check and a requirement is mostly a matter of performance considerations, as most properties require instrumenting GREASE's control flow to insert re-run simulation with extra assertions enabled.

To opt into checking a requirement, pass --req <NAME> one or more times at the command line, where <NAME> is one of the following:

  • in-text: Assert that code is never executed from memory that has write permissions. In practice, this amounts to checking that the program counter only contains addresses from certain parts of the binary, such as the @.text@ section or PLT stub addresses.

  • no-mprotect: The requirement that code is not self-modifying. In practice, this amounts to checking that a PLT stub named mprotect is never called. A limitation of this approach is that it can only detect calls to mprotect from an external library such as libc. If mprotect is statically linked into the binary, for instance, then this requirement would not detect it.

Rust programs

grease has experimental support for analyzing Rust programs, both when compiled to executables and when compiled to LLVM bitcode. From a grease perspective, the average Rust program is significantly more complicated than, say, an average C program for a variety of reasons, including:

  • Rust has a large standard library, and much of the standard library will be included in a typical Rust program. As such, grease has to simulate more code on average.
  • Some library functions (e.g., Rust functions related to string formatting or panicking) have rather complex implementations that are difficult to symbolically execute. As such, it is often necessary to override tricky library functions to replace them with simpler implementations.
  • The code that rustc produces often looks quite different from the code that a typical C compiler would produce. grease's memory model is designed to work well with C compiler idioms, but perhaps not as much with rustc idioms.

As a general rule, it is wise to invoke grease with the --rust flag when simulating Rust programs. Doing so changes some of grease's simulator settings to be more permissive when analyzing code so that it does not mistakenly flag common rustc idioms as undefined behavior. This is especially important for dealing with Rust enums, as grease will often flag enum-related code as reading from uninitialized memory unless --rust is enabled.

Shape DSL

The goal of GREASE's refinement loop is to discover sufficient preconditions for the successful execution of a target function. These preconditions are represented as a mapping from arguments (i.e., registers) to shapes.

Abstract syntax

Conceptually, a shape has the following grammar:

shape ::=
  | bv
  | bv-lit byte+
  | ptr memshape*

memshape ::=
  | uninit N
  | init N
  | exactly byte+
  | memptr memshape*

byte ::= 00 | 01 | ... | ff

Where:

  • bv represents a symbolic bitvector of the appropriate width
  • bv-lit byte+ represents a concrete bitvector literal
  • ptr represents a pointer, the memshape*s are what it points to
  • uninit N represents N uninitialized bytes of memory
  • init N represents N bytes of memory initialized to symbolic bytes
  • exactly byte+ represents a concrete sequence of bytes
  • memptr represents a pointer to a futher allocation

At certain verbosity levels, GREASE may output these preconditions in its logs. It does so using a concrete syntax described below.

Concrete syntax

Bitvectors (bv) are represented with sequences of XX (each representing a symbolic byte), like so:

  • 32-bit: XX XX XX XX
  • 64-bit: XX XX XX XX XX XX XX XX

Bitvector literals (bv-lit) are written in hexadecimal, 0-padded on the left to the appropriate width, and optionally prefixed with 0x. They must have an even number of hexadecimal digits.

  • 32-bit: 0bad1dea, 0x0bad1dea
  • 64-bit: 0bad1deadeadbeef, 0x0bad1deadeadbeef

Similarly, symbolic bytes (init) are written as sequences of XXs, separated by spaces. Uninitialized bytes are written ##. Concrete bytes (exactly) are written like bitvector literals, in hexadecimal, 0-padded on the left to a width of 2. Pointers (ptr, memptr) are represented as an allocation number plus an offset. The targets of pointers are shown out-of-line.

The following example shows a pointer in AArch32 register R1. The pointer points to allocation number 00, at offset 4. Allocation 00 contains four uninitialized bytes, followed by two initialized, symbolic bytes, followed by the concrete bytes fe and 0a, followed by a pointer to allocation 01. Allocation 01 doesn't contain anything at all (thus, any read from or write to it would fail).

R1: 00+00000004
00: ## ## ## ## XX XX fe 0a 01+00000000
01:

For 32-bit architectures, the allocation numbers are 0-padded on the left to a width of 2, whereas for 64-bit architectures, they are padded to a width of 6. The offsets are padded to the maximal number of hex digits required to write numbers of that bit-width, namely 8 for 32-bit and 16 for 64-bit. This scheme ensures that pointers have the same textual width as a pointer-width sequence of bytes.

Long, repeated sequences of symbolic or uninitialized bytes can be written with run-length encoding. For example, a sequence of 64 uninitialized bytes would be ##*00000040. Just as for pointer offsets, the run length is represented as a hexadecimal number of the size of the machine bit-width.

Specifying initial preconditions

GREASE begins its analysis with a "minimal" precondition,1 and uses its heuristics to search for a precondition that avoids errors. In many cases, GREASE's heuristics cannot find such a precondition. In such cases, you can manually specify an initial precondition from which to begin refinement.

Example

For example, consider this (contrived) program:

// test.c
#include <stdlib.h>

void test(int *p, int *q) {
  if (*p == 0) {
    // do some stuff
    free(q);
  }
  // some other stuff
  free(q);
}

int main() { }

GREASE's heuristics are currently insufficient to avoid the double-free, so GREASE will output something like the following:

clang test.c
grease a.out --symbol test

Finished analyzing 'test'. Possible bug: double free at segment1+0x116a

This result may be unsatisfying if you know that test will never be called with *p == 0. By specifying --initial-precondition, you can show GREASE how to avoid the error and continue its analysis. Assuming your compiler targets x86_64 Linux (SysV ABI), write the following in shapes.txt:

rdi: 000000+0000000000000000

000000: 01 XX XX XX

This ensures that loading from p will return a symbolic bitvector with the lowest byte set to 01. In particular, it will never be zero. Re-running GREASE yields:

grease a.out --symbol test --initial-precondition shapes.txt

All goals passed!

Conventions

The general-purpose and floating-point registers are named according to the following schemes:

  • AArch32: R0, R1, V0, ..., V31
  • PPC: r0, ..., r31, f0, ..., f63
  • x86_64: rax, ..., r15, zmm0, ..., zmm15

For LLVM, the arguments are numbered starting from 0 and prefixed with %, so %0, %1, ..., etc.

1

Specifically, all pointer-sized bitvector-typed registers are set to pointers that don't point to anything, and all other bitvector-typed registers are set to symbolic bitvectors.

Shared libraries

grease has rudimentary support for binaries that dynamically link against shared libraries, but with some notable caveats.

Skipping external function calls

Dynamically linked binaries can invoke external functions defined in shared libraries (e.g., libc). Unless grease has an override available, grease treats any invocation of a function defined in a shared library as as no-op. grease will log that the function is skipped, but it will otherwise not simulate it at all. If you want to intercept grease's behavior when it invokes an external function and have it do something, consider supplying an override for the function.

Limitations of PLT stub detection

On the architectures that grease supports, grease identifies which functions are external by determining if the function is being invoked from a PLT stub. Typically, a PLT stub is located in a specially marked .plt or .plt.sec section of the binary.

Unfortunately, reliably identifying PLT stubs is hard. Therefore, grease has (fallible) heuristics for determining which functions have PLT stubs, and it relies on these heuristics to determine which functions are external (and therefore should be skipped or not).

Unfortunately, grease's PLT stub heuristics are not perfect. In particular, grease does not have reliable heuristics for detecting PLT stubs that are located in .plt.got sections, which are common in x86-64 binaries. If you run grease on a binary with a PLT stub that grease cannot detect, then you will likely get an error message stating that grease does not support the relocation type associated with the PLT stub, e.g.,

grease: Attempted to read from an unsupported relocation type (R_X86_64_GLOB_DAT) at address 0x3ff0.
This may be due to a PLT stub that grease did not detect.
If so, try passing --plt-stub <ADDR>:<NAME>, where
<ADDR> and <NAME> can be obtained by diassembling the
relevant PLT section of the binary
(.plt, .plt.got, .plt.sec, etc.).

If this occurs, then you must supply the address and name of the PLT stub to grease yourself. You can do so by passing --plt-stub <ADDR>:<NAME> to grease on the command line, once for each PLT stub. (If you do not know the name of the PLT stub, it is fine to leave <NAME> empty.) Reverse engineering suites such as Ghidra can be effective at determining PLT stub information.

Development

Build

To build and install from source, you'll need to install:

  • GHC 9.4, 9.6, or 9.8
  • cabal-install 3.6 or later

Follow the instructions on the Haskell installation page.

Then, clone GREASE and its submodules:

git clone https://github.com/GaloisInc/grease
cd grease
git submodule update --init

Then, build with cabal:

cabal build

Docker

GREASE also offers a nightly Docker image that gets built after each commit to the main branch. To run GREASE on an input using Docker, run the following

docker run ghcr.io/galoisinc/grease:nightly <input>

GREASE's test suite can also be run through Docker, although it requires changing the entrypoint to use grease-tests instead:

docker run --entrypoint grease-tests ghcr.io/galoisinc/grease:nightly

The Docker image is available for both amd64 and arm64 architectures.

Documentation

Documentation is built with mdBook. Install with cargo (or with a package manager):

cargo install mdbook

Then build the book with:

cd doc
mdbook build

As always, see --help for more options.

Linting

We treat a small number of hlint warnings as errors in CI. To run hlint locally, try:

hlint main src tests

Test suite

To run the tests:

$ cabal test

The tests reside in the tests/ directory. We divide the tests into two general categories: (1) tests involving binaries, and (2) tests involving LLVM bitcode or S-expression files.

Binary test cases

These test grease's machine code frontend by ingesting binaries. These test cases are organized into different subdirectories:

  1. prop/: Tests that exercise particular property assertions (i.e., requirements). This directory has sub-directories for each property supported by grease. Within each property-specific directory, there are up to four additional directories:

    a. pos/: "true positives", tests that should trigger (fail) the assertion, and do

    b. neg/: "true negatives", tests that should not trigger (pass) the assertion, and don't

    c. xfail-pos/: "false positives", i.e., type I error, tests that should not trigger the assertion, but do

    d. xfail-neg/: "false negatives", i.e., type II error, tests that should trigger the assertion, but don't

  2. refine/: Tests that exercise the precondition refinement process but are not particularly relevant to any property assertions. This directory also has four subdirectories:

    a. bug/: tests that encounter an error that grease can't work around that might be a bug

    b. pos/: "true positives", tests that have some sufficient precondition for successful execution, and grease finds it

    c. neg/: "true negatives", tests that have no sufficient precondition for successful execution, and grease can't find one

    d. xfail-pos/: "false positives", i.e., type I error, tests that have no sufficient precondition for successful execution, but grease still "finds" one

    e. xfail-neg/: "false negatives", i.e., type II error, tests that have some sufficient precondition for successful execution, but grease can't find it

  3. sanity/: Tests that exercise earlier or more fundamental parts of grease, such as disassembly or machine code semantics. For these tests, we don't particularly care whether grease finds a refined precondition. This directory has two subdirectories:

    a. pass/, for tests that don't cause any issues

    b. xfail-panic/, for tests that cause unhandled exceptions in grease

    c. xfail-iters/, for tests that cause unbounded iterations of the refinement loop

xfail tests may represent known bugs, or yet-to-be-implemented improvements. In this case, it's helpful to add a comment to the top of the C source file referring to a specific issue that describes the bug or feature, and to additionally provide a short synopsis of that issue. xfail tests may also represent fundamental limitations of the tool's architecture or design that are not expected to be fixed, in which case the comment should instead describe this limitation (or point to documentation that does).

To add a new test, add a new directory under the appropriate directory above. It should contain at least one of the following executables:

  • A 32-bit ARM ELF executable named test.armv7l.elf
  • A 32-bit PowerPC ELF executable named test.ppc32.elf. (At the moment, we don't include 64-bit PowerPC executables, but we could if the need arose.)
  • An x86_64 executable named test.x64.elf.

Each executable should contain an entrypoint symbol named test.

By default, each test will be run as though grease were invoked with the following command-line options:

  • The entrypoint is set to --symbol test.
  • --iters is set to 32 to ensure that the xfail-iters tests complete in a somewhat reasonable amount of time.
  • All other command-line options inherit their default values.

If you wish to override these options, you can do so by adding one of the following files alongside the executables:

  • test.config: This file should contain a list of command-line options, with each one separated by whitespace, e.g.,

    --symbol foo --stack-argument-slots 5

    These command-line options are applied to all test.<arch>.elf executables, regardless of what <arch> is being used.

  • test.<arch>.config: This is like a test.config file, except that the options in this file are only applied to test.<arch>.elf, making these options architecture-specific.

If both types of *.config files are present, then the options from both files will be combined. If a command-line option is not explicitly mentioned in a *.config file, then it will inherit its default value as described above.

LLVM bitcode and S-expression test cases

Test cases that do not involve binaries fall into this category. Unlike binary test cases, the test suite will not automatically discover these test cases, so it is the developer's responsibility to define expectations for them in the Haskell test code. These test cases are organized into different subdirectories:

  1. llvm/: LLVM CFGs (via crucible-llvm-syntax). Each of these test cases has the file extension *.llvm.cbl.

  2. llvm-bc/: LLVM bitcode files (via grease's LLVM frontend). Each of these test cases has the file extension *.bc.

  3. arm: AArch32 machine-code CFGs (via macaw-aarch32-syntax). Each of these test cases has the file exension *.armv7l.cbl.

  4. ppc32: PPC32 machine-code CFGs (via macaw-ppc-syntax). Each of these test cases has the file exension *.ppc32.cbl.

  5. x86: x86-64 machine-code CFGs (via macaw-x86-syntax). Each of these test cases has the file exension *.x64.cbl.

Each test case can optionally supply a <name>.config file (in the same subdirectory as the test case) that overrides the default command-line options. The <name> in <name>.config file must match the name of the test case without its file extensions. For instance, a file named foo.config will apply to a test case named foo.llvm.cbl, but it would not apply to bar.llvm.cbl.

Profiling

GREASE includes functionality for profiling its performance. To generate a profiling report, pass --profile-to <DIR> to GREASE. This will generate a <DIR>/profile.html file that can be viewed in a web browser. The data that this HTML file presents will be periodically regenerated as GREASE runs on the program. A typical example looks like:

Profiler example

The profiling report presents a hierarchical view of the functions that are invoked during the simulation of a program. The x-axis represents the time, and the y-axis shows the call stack depth, counting from zero at the bottom. Each stack frame is given a score based on some simulator heuristics (the time spent simulating it, its number of allocations, its numbers of merges, etc.). Generally speaking, the higher the score, the more likely it is to be a performance bottleneck.