GaloisInc/macaw

这是 Macaw 二进制分析框架的主仓库，它具有两个关键目标：二进制代码发现和机器码的符号执行。实现该框架是为了提供对架构的可扩展支持（即，库客户端可以添加他们自己的架构并按需选择所需的架构支持）。 # 概述 代码发现算法基于强制执行，能够从一个或多个入口点发现代码。符号是可选的，但可以显著提高结果的质量。剥离符号的二进制文件可能会对 Macaw 构成挑战（尤其是静态且被剥离符号的二进制文件）。Macaw 支持将发现的机器码提升为适合通过 Crucible 库进行符号执行的 IR。 目前，Macaw 支持： * x86-64 * PowerPC（32 位和 64 位） * ARM（32 位） * RISC-V ## 仓库结构 Macaw 库包括： * macaw-base -- 核心的架构无关操作和算法。 * macaw-symbolic -- 通过 Crucible 提供 Macaw 程序符号模拟的库。 * macaw-x86 -- 提供使 Macaw 能够用于 X86_64 程序的定义。 * macaw-x86-symbolic -- 添加支持 x86 所需的 Macaw-symbolic 扩展。 * macaw-semmc -- 包含从 semmc 语义到 Macaw IR 转换中与架构无关的组件。这为我们所有的后端提供了共享的基础设施；这将包括 Template Haskell 函数，用于从 _semmc_ 库提供的已学习语义文件创建状态转换器函数。 * macaw-arm -- 通过读取 _semmc_ 生成的语义文件并使用 Template Haskell 生成一个根据已学习语义转换机器状态的函数，使 Macaw 能够用于 ARM（32 位）二进制文件。 * macaw-arm-symbolic -- 使 Macaw/Crucible 能够对 ARM（32 位）架构进行符号模拟。 * macaw-ppc -- 通过读取 _semmc_ 生成的语义文件并使用 Template Haskell 生成一个根据已学习语义转换机器状态的函数，使 Macaw 能够用于 PPC（32 位和 64 位）二进制文件。 * macaw-ppc-symbolic -- 使 Macaw/Crucible 能够对 PPC 架构进行符号模拟 * macaw-riscv -- 使 Macaw 能够用于 RISC-V（RV32GC 和 RV64GC 变体）二进制文件。 * macaw-loader -- 提供统一的接口来加载二进制文件（例如 ELF 格式），并将其转换为基于 Macaw 的内存和入口点列表。 * macaw-loader-{aarch32,ppc,riscv,x86} -- 分别为 ARM、PPC、RISC-V 和 x86_64 架构提供 macaw-loader 后端。 * macaw-refinement -- 启用额外的架构无关的代码发现细化。这可以发现比 macaw-base 中的分析所揭示的更多的功能。 * crucible-macaw-debug：在使用 [Crucible 的交互式调试器](https://github.com/GaloisInc/crucible/tree/master/crucible-debug) 时，支持内省 Macaw 特定的信息。 构成 Macaw 的各个库均在 BSD 许可证下发布。 这些 Macaw 核心库依赖于许多不同的支持库，包括： * elf-edit -- 加载和解析 ELF 二进制文件 * galois-dwarf -- 从二进制文件中检索 Dwarf 调试信息 * flexdis86 -- 针对 x86 架构的反汇编和语义 * dismantle -- 针对 ARM 和 PPC 架构的反汇编 * semmc -- 针对 ARM 和 PPC 架构的语义定义 * crucible -- 符号执行和分析 * what4 -- Crucible 后端的符号表示 * parameterized-utils -- 用于处理参数化类型的实用工具 ## 文档 可以在 [`doc`](doc) 子目录中找到一系列高层设计文档。关于单个 API 函数和数据类型的文档可以在代码中的 Haddock 注释里找到。 我们还编写了其他一些关于 Macaw 的资源： * [Macaw：面向忙碌二进制分析师的机器码工具箱](http://www.arxiv.org/abs/2407.06375)：一篇关于 Macaw 以及构建在 Macaw 之上的二进制分析工具的未发表论文。 * [构建可扩展的、基于 SMT 的机器码内存模型](https://galois.com/blog/2023/03/making-a-scalable-smt-based-machine-code-memory-model/)：一篇关于 `macaw-symbolic` 延迟内存模型的博客文章（在 [`Data.Macaw.Symbolic.Memory.Lazy`](symbolic/src/Data/Macaw/Symbolic/Memory/Lazy.hs) 中实现） # 构建 ## 准备工作 构建 Macaw 时非来自 Hackage 的依赖项是通过 Git 子模块支持的： ``` $ git submodule update --init ``` ### 为 RISC-V 后端准备 Softfloat RISC-V 后端依赖于 softfloat-hs，而后者又依赖于 softfloat 库。Macaw 的构建系统会自动构建 softfloat，但必须递归克隆 softfloat-hs 仓库才能启用此功能。如果您不构建 `macaw-riscv`，则可以跳过此步骤。要递归克隆 softfloat-hs，请运行： ``` $ cd deps/softfloat-hs $ git submodule update --init --recursive ``` ## 使用 Cabal 构建 可以使用 Cabal 单独或集中构建 Macaw 库： ``` $ ln -s cabal.project.dist cabal.project $ cabal configure $ cabal build all ``` 要构建单个库，可以指定该库名称来代替 `all`，或者在构建前切换到该库的子目录： ``` $ cabal build macaw-refinement ``` 或者 ``` $ cd refinement $ cabal build ``` # 关于 Freeze 文件的说明 我们使用 `cabal.project.freeze.ghc-*` 文件来限制 CI 中的依赖项版本。要使用一组已知可用的 Hackage 依赖项进行构建： ``` ln -s cabal.GHC-.config cabal.project.freeze ``` 这些 freeze 文件是使用 `scripts/regenerate-freeze-files.sh` 脚本生成的。 请注意，目前这些配置文件假定使用的是类 Unix 操作系统，因为我们目前没有在 CI 上测试 Windows。如果您想在 Windows 上使用这些配置文件，则需要手动进行一些更改以移除某些包和标志： ``` regex-posix tasty +unix unix unix-compat ``` 请注意，如果任何 Macaw 包在*没有* freeze 文件的情况下构建失败，这就是 `.cabal` 文件中指定的依赖项版本边界存在的一个 bug，应当予以报告 (https://github.com/GaloisInc/macaw/issues)。 # 许可证 此代码基于 BSD3 许可证提供，不提供任何支持。

标签：Crucible, DAST, Hakrawler, Haskell, IR, JA3, Macaw, PowerPC, RISC-V, Semantics, Wayback Machine, x86-64, 中间表示, 二进制分析, 云安全监控, 云安全运维, 云资产清单, 代码发现, 反汇编, 多架构支持, 开源, 强制执行, 恶意软件分析, 机器码分析, 模糊分析, 符号执行, 逆向工程, 静态分析