Key information:

• GREASE can be used as a Ghidra plugin, standalone tool, or Haskell library, and supports analysis of various Linux ELF binaries and LLVM bitcode.
• It can find hard-to-spot bugs in binaries, like in the libpng code example where it detected a divide-by-zero bug.
• GREASE works similarly to UC-Crux by running functions on symbolic registers and using heuristics to refine preconditions.
• It has limitations such as relying on heuristics that can cause false positives or negatives, being subject to path explosion, and having limitations with certain machine code behaviors.
• Compared to other tools, it covers more input space than fuzzers, is different from angr in default symbolic execution and memory model, supports binaries in addition to LLVM like KLEE but with under-constrained symbolic execution, is built on top of Macaw, and can be integrated into binary analysis platforms.

Important details:

• The libpng bug example shows how GREASE can automatically identify a hard-to-spot issue that is difficult to detect at the source level.
• The output of GREASE shows details about the bug found, such as the register values and the specific location where the divide-by-zero occurs.
• Regarding limitations, it is noted that GREASE cannot handle unbounded heap data structures and can get stuck on symbolic loop conditions.
• The comparison to other tools highlights their differences in functionality and usage scenarios.
• The conclusion encourages sharing GREASE and welcomes contributions and questions.
• The material is supported by the Defense Advanced Research Projects Agency.