# GREASE 欠约束符号执行二进制分析工具 > Galois 开发的命令行工具、Ghidra 插件和 Haskell 库，借助欠约束符号执行检查二进制程序的性质。它把 AArch32、PowerPC 或 x86_64 的 ELF 可执行文件和共享对象（或 LLVM bitcode）转换为控制流图，从所有寄存器均为符号值的状态模拟每个函数，并在发生越界访问后逐步扩充推断出的内存布局，最终报告除零、非法内存访问等可能的未定义行为，并给出具体化的参数。内置覆盖（override）或用户以 Crucible S 表达式语言编写的覆盖可模拟外部库函数，插件则在 Ghidra 中展示结果。 - 类型：工具 - 目标：二进制 - 类别：原生分析工具 - 关联：基础工具 - 来源复核于：2026-10-27 - 收录于：2026-11-03 - 原始资源： - 一手来源： - 目录页面： - 记录 JSON： - 英文版：[English](https://awesomerea.org/resources/grease/index.md) ## 使用条件与局限 - 审阅时没有带标签的发布版本：安装指南提供由 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”（已批准公开发布）声明。报告结果取决于推断出的前置条件、界限和覆盖。 ## 一手来源 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11. 12. ## 同分区更多条目：原生二进制 - [PLASMA 交互式反汇编器](https://awesomerea.org/zh/resources/plasma-disassembler/index.md) · 工具 - [mobdevim iOS 设备命令行工具](https://awesomerea.org/zh/resources/mobdevim/index.md) · 工具 - [XPEViewer PE 文件查看与编辑工具](https://awesomerea.org/zh/resources/xpeviewer/index.md) · 工具 - [Fermion Frida 脚本图形化开发环境](https://awesomerea.org/zh/resources/fermion/index.md) · 工具 - [Ghidrathon Ghidra Python 3 脚本扩展](https://awesomerea.org/zh/resources/ghidrathon/index.md) · 工具 - [diStorm3 x86/AMD64 反汇编库](https://awesomerea.org/zh/resources/distorm/index.md) · 工具 ## 关于此条目 说明已依据一手来源复核。 原创说明采用 MIT 许可；外部项目、论文与素材保留各自的权利和许可。