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.

Demo

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

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)

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

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 language. For information about this language, see Writing S-expression programs.

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:¹

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 AArch32 overrides
• *.llvm.cbl for LLVM overrides
• *.ppc32.cbl for PPC32 overrides
• *.ppc64.cbl for PPC64 overrides
• *.x64.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.

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. Many of the built-in overrides correspond to functions from libc. 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. User-defined overrides may call built-in overrides.

A complete list can be found on the page on built-in overrides.

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.

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. We require Ghidra version or 11.0 or later, as this is when Ghidra introduced initial support for Rust binaries.

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:

Writing S-expression programs

In addition to binaries and LLVM bitcode files, GREASE supports analysis of programs written in several variants of the Crucible S-expression language. Each language supported by GREASE extends the base S-expression language with additional types and operations, see:

• macaw-symbolic-syntax for binaries
  • macaw-aarch32-syntax for AArch32
  • macaw-ppc-syntax for PowerPC
  • macaw-x86-syntax for x86_64
• crucible-llvm-syntax for LLVM

File naming conventions

S-expression programs must be named as follows:

• *.armv7l.cbl for AArch32 syntax
• *.llvm.cbl for LLVM syntax
• *.ppc32.cbl for PPC32 syntax
• *.ppc64.cbl for PPC64 syntax
• *.x64.cbl for x86_64 syntax

Conventions for entrypoints

Entrypoints of non-LLVM S-expression programs must take a single argument and return a single value, both of a designated architecture-specific struct type, representing the values of all registers. These struct types are called AArch32Regs, PPC32Regs, PPC64Regs, and X86Regs.

For example, here is a minimal AArch32 S-expression program that swaps the values in R0 and R1:

(defun @test ((regs0 AArch32Regs)) AArch32Regs
  (start start:
    (let init-r0 (get-reg r0 regs0))
    (let init-r1 (get-reg r1 regs0))
    (let regs1 (set-reg r0 init-r1 regs0))
    (let regs2 (set-reg r1 init-r0 regs1))
    (return regs2)))

For more information about this struct, see the Macaw documentation.

Built-in overrides

In addition to user-defined overrides, GREASE also provides a number of built-in overrides that are built directly into the tool. Many of the built-in overrides correspond to functions from libc. 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. User-defined overrides may call built-in overrides.

The list of built-in overrides

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* )
• i32 @open( i8*, i32 )
• i32 @close( i32 )
• ssize_t @read( i32, i8*, size_t )
• ssize_t @write( i32, i8*, size_t )

LLVM-specific overrides

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

• 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> )

Binary-specific overrides

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

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

S-expression-specific overrides

For LLVM S-expression files (programs or overrides), the following overrides are also available:

(declare @read-bytes ((x (Ptr 64))) (Vector (Bitvector 8)))
(declare @read-c-string ((x (Ptr 64))) (String Unicode))
(declare @write-bytes ((dest (Ptr 64)) (src (Vector (Bitvector 8)))) Unit)
(declare @write-c-string ((dst (Ptr 64)) (src (String Unicode))) Unit)

See the upstream documentation.

Discussion

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.

• open, close, read, and write

  These overrides leverage Crucible's experimental symbolic I/O capabilities. In particular, these overrides require the use of a symbolic filesystem, which must be specified with --fs-root <path-to-filesystem-root> when invoking grease. See symbolic I/O for a more detailed description of what the contents of the symbolic filesystem should look like.

Crucible types for overrides

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>)
• ssize_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

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.

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 program¹

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

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. See Undefined behavior for a more detailed discussion of which undefined behaviors GREASE can check for.

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:

• some types of relocations
• executing code from shared libraries
• semantics for some instructions on some architectures (e.g., hlt on x86_64)

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.¹ For example, the null pointer is represented by the pair (0, 0x0).

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 preceded 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.² 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).

Refinement

Before continuing, it would be helpful to review:

• the overview
• the memory model

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 (see Undefined behavior for details). 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 further 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,¹ 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.

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

Undefined behavior

GREASE aims to find or verify the absence of bugs in the program under analysis. It supports checking both for specific requirements and for generally suspicious behaviors. This page describes the latter.

What constitutes a bug? When analyzing C, C++, or Rust code, a conservative answer is that any form of reachable undefined behavior in a complete program constitutes a bug. For machine code, things aren't so clear.

Many behaviors that might be considered undesirable or undefined at the source level have well-defined semantics at the machine code level. For example, consider a C program with a stack buffer overflow into an adjacent variable. In the C abstract machine, such behavior is clearly undefined. However, if the program is compiled in a straightforward way into machine code, the distinction between different stack variables is lost. The resulting code simply performs several innocuous-looking writes to the stack. Similarly, adding two signed integers in C might result in an undefined signed overflow. At the machine code level, there is no distinction between signed and unsigned integers, and arithmetic operations generally have a well-defined semantics for all inputs (e.g., based on a two's complement representation).

GREASE aims to be pragmatic in what it calls a bug. It uses a C-like memory model, and reports behaviors of binaries that would likely constitute undefined behavior in C. However, as described above, many sources of undefined behavior are impossible or infeasible to detect at the level of machine code. The following sections detail what behaviors GREASE can and cannot check.

C11 undefined behaviors

This section describes which forms of undefined behaviors listed in the C11 standard GREASE checks for. Because the C standard does not offer a comprehensive numbering scheme, we adopt that of the back matter of the SEI CERT C Coding Standard.

The following determinations are quite nuanced. Please reach out to grease@galois.com if you have further questions about the properties checked by GREASE.

Many undefined behaviors refer to the lexical and syntactic structure of the source C program. Such behaviors are clearly out of scope for GREASE. This includes at least behaviors 2, 3, 4, 6, 7, 8, 14, 15, 26-31, 33, 34, 58, 59, and 90-96.

Additional behaviors refer to syntactic categories such as lvalues that do not have corollaries at the binary level. This includes at least behaviors 12, 13, 18-21, 36, 46, 61, 62.

Further behaviors refer to types that are not available or semantically meaningful at the binary level, such as void. This includes at least behavior 22.

The following table lists the remaining behaviors. It is far from complete, and we hope to expand it over time.

Exceptions

Certain operations generate traps or exceptions at the processor level. GREASE attempts to treat these as errors. These include:

• Division by zero

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 exe:grease

See Test suite for how to run the tests.

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

Generic scripts

We have a few Python scripts in scripts/lint/ that perform one-off checks. They generally take some number of paths as arguments, check .github/workflows/lint.yml to see how they are invoked in CI.

hlint

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

hlint grease{,-aarch32,-ppc,-x86}/src grease-cli/{main,src,tests}

ruff

We lint and format the Python linting scripts and Ghidra plug-in with ruff.

ruff format scripts/lint ghidra_scripts
ruff check scripts/lint ghidra_scripts

typos

We run typos on doc/ to spell-check the documentation. To run it locally, try:

typos doc/

Source code

The grease source code is split up into a number of smaller libraries, each residing in its own top-level directory:

• grease: This comprises the core of grease as a library.
• grease-aarch32: This extends the grease library with the ability to reason about AArch32 binaries.
• grease-ppc: This extends the grease library with the ability to reason about 32-bit and 64-bit PowerPC binaries.
• grease-x86: This extends the grease library with the ability to reason about x86-64 binaries.
• grease-cli: This defines a command-line application on top of the library code in grease.

Periodic tasks

The following is a list of things that should be done occasionally by GREASE developers.

• Check for out-of-date documentation
• Fix warnings from cabal haddock
• Review and triage old issues
• Update versions of dependencies and tools
  • Bump bounds on Hackage dependencies (cabal outdated can help)
  • Bump submodules
  • Update versions of tools used in CI:
    • Cabal
    • GHC (see below)
    • Linters
    • OS images
    • what4-solvers
  • Update versions of tools used in the Dockerfile:
    • ghcup

GHC versions

We support the three most recent versions of GHC. We try to support new versions as soon as they are supported by the libraries that we depend on.

Adding a new version

GREASE has several Galois-developed dependencies that are pinned as Git submodules, in deps/. These dependencies need to support new GHC versions before GREASE itself can. First, create GitHub issues on each of these dependencies requesting support for the new GHC version. Then, create an issue on the GREASE repo that includes:

1. A link to the GHC release notes for the new version
2. Links to the issues on the dependencies
3. A link to this section of this document

Then, wait for the issues on the dependencies to be resolved. When adding support for the new GHC version to GREASE itself, complete the following steps:

• For each package:
  • Allow the new version of base in the Cabal build-depends
  • Run cabal {build,test,haddock}, bumping dependency bounds and submodules as needed
  • Fix any new warnings from -Wdefault
• Add the new GHC version to the matrix in the GitHub Actions workflows
• Bump the GHC version in the Dockerfile to the latest supported version
• Follow the below steps to remove the oldest GHC version

Removing an old version

• Remove the old version from the matrix in the GitHub Actions configuration
• Remove outdated CPP ifdefs that refer to the dropped version
• Remove outdated if stanzas in the Cabal files

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:

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.

Test suite

To run the tests:

$ cabal test pkg:grease-cli

The tests reside in the grease-cli/tests/ directory. They are automatically discovered by the test harness based on their file name. They are written using Oughta.

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 can be several 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. 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 a few 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.

LLVM bitcode and S-expression test cases

Test cases that do not involve binaries fall into this category. They 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 extension *.armv7l.cbl.

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

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

UX tests

Tests located in the ux/ directory may be binaries, bitcode, or S-expression programs. They are intended to test the User eXperience (mostly, the log output) of GREASE.

Lua API

The test harness provides the following Lua API, which enriches that of Oughta with GREASE-specific functionality. The API is presented with Haskell-style type signatures:

• prog: The name of the program under test, e.g., "test.llvm.cbl".
• go(prog_name): Run GREASE with the given string as the name of the program. Frequently, prog is passed as the argument, e.g., go(prog). go may be called multiple times per test, see func-ptr.llvm.cbl for an example.
• flags(fs): Append the given flags to the arguments passed to GREASE when go is invoked. The flags are cleared after go is run.

It is common (though not necessary) to define a function named test and to specify it as the only entrypoint:

// all: flags {"--symbol", "test"}
// all: go(prog)

void test(/* ... */) { /* ... */ }

Writing good tests

The Rust Compiler Development Guide has some helpful guidance on writing high-quality tests. The GREASE test suite is generally quite similar in structure to that of rustc, so almost all of the advice there applies mutatis mutandis.