工具
GREASE 欠约束符号执行二进制分析工具
Galois 开发的命令行工具、Ghidra 插件和 Haskell 库，借助欠约束符号执行检查二进制程序的性质。它把 AArch32、PowerPC 或 x86_64 的 ELF 可执行文件和共享对象（或 LLVM bitcode）转换为控制流图，从所有寄存器均为符号值的状态模拟每个函数，并在发生越界访问后逐步扩充推断出的内存布局，最终报告除零、非法内存访问等可能的未定义行为，并给出具体化的参数。内置覆盖（override）或用户以 Crucible S 表达式语言编写的覆盖可模拟外部库函数，插件则在 Ghidra 中展示结果。
- 目标
- 二进制
- 类别
- 原生分析工具
- 关联
- 基础工具
- 来源复核于
使用条件与局限
- 审阅时没有带标签的发布版本：安装指南提供由 main 分支构建的每夜 Docker 镜像（ghcr.io/galoisinc/grease:nightly），或从源码构建；同一套文档发布在 galoisinc.github.io/grease。所审阅的 main 分支提交日期为 2026-09-24；Galois 在 2025-03-19 的博客文章中介绍了该工具。
- 从源码构建需要 GHC 9.6、9.8 或 9.10、cabal-install 3.6+ 以及仓库的 git 子模块，其中包括 Galois 的 macaw、crucible、what4 和 elf-edit。独立运行的程序还需要 bitwuzla、cvc4、cvc5、yices 或 z3 中的一种 SMT 求解器；默认使用 yices，CI 测试的版本为 2.6.5，Docker 镜像已包含这些求解器。Ghidra 插件需要 Ghidra 11.0+ 和本地的 grease 程序。
- 需自行提供要分析的 ELF 二进制或 LLVM bitcode。默认分析所有已知函数，也可按符号、地址或核心转储选择入口。局限性页面列出：只分析单线程执行；数据结构、循环和递归受 k 界限制；通过符号函数指针的调用会被跳过；不检测栈缓冲区溢出，也不模拟堆耗尽；字符串操作支持有限；不支持在 main 之前运行的代码。
- 仓库提交了由相邻 C 或汇编源码构建的小型测试样本：grease-exe/tests 下约 200 个 AArch32、PowerPC 和 x86_64 ELF 可执行文件与共享对象，另有 grease-x86/test-data、ghidra-ecfs/src/test/resources/ecfs 以及随附的 screach 可达性分析工具各测试数据目录中的测试 ELF。
- BSD-3-Clause 许可证（LICENSE）。README 注明由 DARPA 资助，并附有“Distribution Statement A”（已批准公开发布）声明。报告结果取决于推断出的前置条件、界限和覆盖；本条目未分析任何二进制。
关于此条目
说明已依据一手来源复核；这不代表已运行验证、经过安全审计或确认兼容。
一手来源
- doc/overview.md GitHub · GaloisInc/grease · 修订 b94e1e0
- README.md GitHub · GaloisInc/grease · 修订 b94e1e0
- doc/install.md GitHub · GaloisInc/grease · 修订 b94e1e0
- doc/usage.md GitHub · GaloisInc/grease · 修订 b94e1e0
- doc/dev/dev.md GitHub · GaloisInc/grease · 修订 b94e1e0
- doc/ghidra-plugin.md GitHub · GaloisInc/grease · 修订 b94e1e0
- doc/limitations.md GitHub · GaloisInc/grease · 修订 b94e1e0
- doc/overrides.md GitHub · GaloisInc/grease · 修订 b94e1e0
- grease-exe/tests GitHub · GaloisInc/grease · 修订 b94e1e0
- LICENSE GitHub · GaloisInc/grease · 修订 b94e1e0
- https://galoisinc.github.io/grease/
- https://www.galois.com/articles/introducing-grease