AwesomeREA.org

Tool

GREASE

Galois's command-line tool, Ghidra plug-in and Haskell library for checking properties of binaries with under-constrained symbolic execution. It lifts AArch32, PowerPC or x86_64 ELF executables and shared objects, or LLVM bitcode, into a control-flow graph, simulates each function from fully symbolic registers and grows the inferred memory layout after out-of-bounds accesses, then reports likely undefined behavior such as division by zero or invalid memory access together with concretized arguments. Built-in overrides, or user overrides written in Crucible's S-expression language, model external library functions, and the plug-in presents results in Ghidra.

Targets
Binary
Category
Native analysis tools
Relationship
Foundation tool
Sources reviewed

Requirements & limits

  • No tagged releases at review: the installation guide offers a nightly Docker image built from main (ghcr.io/galoisinc/grease:nightly) or a source build, and the same documentation is published at galoisinc.github.io/grease. The reviewed main commit is dated 2026-09-24; Galois introduced the tool in a blog post dated 2025-03-19.
  • Source builds need GHC 9.6, 9.8 or 9.10, cabal-install 3.6+ and the repository's git submodules, including Galois's macaw, crucible, what4 and elf-edit. A standalone binary also needs one of the SMT solvers bitwuzla, cvc4, cvc5, yices or z3; it defaults to yices, which CI tests at 2.6.5, and the Docker image includes the solvers. The Ghidra plug-in needs Ghidra 11.0+ and a local grease binary.
  • Supply the ELF binary or LLVM bitcode yourself. By default every known function is analyzed; entry points can instead be chosen by symbol, address or core dump. The limitations page lists single-threaded analysis only, k-bounded data structures, loops and recursion, skipped calls through symbolic function pointers, no stack-buffer-overflow detection or heap-exhaustion modeling, limited string operations and no support for code that runs before main.
  • The repository commits small test fixtures built from adjacent C or assembly sources: about 200 AArch32, PowerPC and x86_64 ELF executables and shared objects under grease-exe/tests, plus test ELFs under grease-x86/test-data, ghidra-ecfs/src/test/resources/ecfs and the bundled screach reachability tool's test-data directories.
  • BSD-3-Clause (LICENSE). The README credits DARPA funding and carries Distribution Statement A, approved for public release. Reports depend on the inferred preconditions, bounds and overrides; no binaries were analyzed for this entry.

About this entry

The description was reviewed against primary sources. This does not establish runtime testing, security auditing or verified compatibility.

Report an outdated entry Suggest a translation fix

Primary sources

  1. doc/overview.md GitHub · GaloisInc/grease · Revision b94e1e0
  2. README.md GitHub · GaloisInc/grease · Revision b94e1e0
  3. doc/install.md GitHub · GaloisInc/grease · Revision b94e1e0
  4. doc/usage.md GitHub · GaloisInc/grease · Revision b94e1e0
  5. doc/dev/dev.md GitHub · GaloisInc/grease · Revision b94e1e0
  6. doc/ghidra-plugin.md GitHub · GaloisInc/grease · Revision b94e1e0
  7. doc/limitations.md GitHub · GaloisInc/grease · Revision b94e1e0
  8. doc/overrides.md GitHub · GaloisInc/grease · Revision b94e1e0
  9. grease-exe/tests GitHub · GaloisInc/grease · Revision b94e1e0
  10. LICENSE GitHub · GaloisInc/grease · Revision b94e1e0
  11. https://galoisinc.github.io/grease/
  12. https://www.galois.com/articles/introducing-grease

More in Native binaries

All 158 entries in Native binaries