toolCHAINZ/jingle

# `jingle`: `p-code` 的 SMT 建模 `jingle` 为 Ghidra 的 `p-code` 提供 SMT 建模。它将 `p-code` 虚拟机的状态表示为 `QF_ABV` 逻辑上的表达式，并将 `p-code` 操作表示为这些状态之间的关系。此外，它还实现了基于 pcode 的可配置程序分析（Configurable Program Analysis）算法，允许快速实现灵活的自定义分析。 **ALPHA 软件：本软件适合用于研究，但尚未准备好在生产环境中使用。** 本仓库包含一个 [Cargo Workspace](https://doc.rust-lang.org/book/ch14-03-cargo-workspaces.html)，其中包含三个相关的 crate： * [`jingle_sleigh`](./jingle_sleigh)：[Ghidra](https://github.com/NationalSecurityAgency/ghidra) 代码转换器 `SLEIGH` 的 Rust FFI 封装。`SLEIGH` 用 C++ 编写，可在[此处](https://github.com/NationalSecurityAgency/ghidra/tree/master/Ghidra/Features/Decompiler/src/decompile/cpp)找到。此 crate 包含指向 `SLEIGH` 的私有内部低级 API，并向使用者暴露符合惯用语法的高级 API。 * [`jingle`](./jingle)：使用 [z3.rs](https://github.com/prove-rs/z3.rs) 定义 p-code 状态和操作的 SMT 建模，以及一个小型程序分析框架。`jingle` 实现了[可配置程序分析](https://doi.org/10.1007/978-3-319-10575-8_16)，允许进行灵活的自定义程序分析，并提供了用于构建展开后的 p-code 程序 SMT 模型的预构建分析。 * [`jingle_python`](./jingle_python)：`jingle` 的一组 [pyo3](https://pyo3.rs) 绑定。这些绑定向 SLEIGH 和我们在 SMT 中对 `p-code` 的逻辑建模暴露了一个简单的接口。SMT 公式被封装在其“原生” Python z3 类中，以便于与其他工具集成。这些绑定目前还非常原始，可能会发生变化，且尚未暴露任何程序分析 API。 ## 用法 为了在您的项目中使用 `jingle`，您只需执行 `cargo add`： ``` cargo add jingle ``` 虽然 `jingle` 可以配置为使用单个固定的 `sleigh` 架构， 但默认的使用方式是将其指向现有的 `ghidra` 安装路径。 [安装 ghidra](https://ghidra-sre.org) 并在实例化 `SleighBuilder` 时使用安装根目录。 此处使用 ghidra 的唯一目的仅是作为 `sleigh` 架构的标准化文件夹布局。 `jingle` 对 ghidra 没有任何代码依赖（捆绑的 `sleigh` C++ 代码除外）。 ### 命令行界面 (CLI) 您可以通过运行以下命令来安装一个展示 jingle 建模功能的简单 CLI ``` cargo install --features bin jingle ``` 如果您正在使用 [CLI](./jingle)， 则在首次运行时请提供 ghidra 的路径作为参数。 该 CLI 可为小型十六进制编码的指令生成反汇编、pcode 和 SMT 模型。请注意，该 CLI 使用的是 `jingle` 建模的一个较旧版本，不支持任意控制流。 ## 开发 如果您正在直接使用 `jingle` 源代码发行版， 您需要手动下载一份 `ghidra` 源码树， 以便构建 `jingle` 或 `jingle_sleigh`。 如果您正在使用 `git`，可以使用现有的子模块完成此操作。 只需运行 ``` git submodule init && git submodule update ``` 如果您出于某种原因使用的是压缩包源码发行版， 则可以运行以下命令： ``` cd jingle_sleigh git clone https://github.com/NationalSecurityAgency/ghidra.git ``` 如果您将 `jingle` 作为 cargo `git` 或 `crates.io` 依赖项使用， 则无需此步骤。`cargo` 将在 `git` 情况下处理所有这些工作， 并且我们会在所有 `crates.io` 发布版本中包含（vendor）必要的 `ghidra` 源码。 # 研究论文 `jingle` 最初是为了支持我们的研究论文 _Synthesis of Code-Reuse Attacks from `p-code` Programs_ 而开发的， 该论文在 [Usenix Security 2025](https://www.usenix.org/conference/usenixsecurity25/presentation/denhoed) 上发表。 如果您发现该论文或其实现有用，可以使用以下 BibTeX 引用它： ``` @inproceedings{10.5555/3766078.3766099, author = {DenHoed, Mark and Melham, Tom}, title = {Synthesis of code-reuse attacks from p-code programs}, year = {2025}, isbn = {978-1-939133-52-6}, publisher = {USENIX Association}, address = {USA}, booktitle = {Proceedings of the 34th USENIX Conference on Security Symposium}, articleno = {21}, numpages = {17}, location = {Seattle, WA, USA}, series = {SEC '25} } ```

标签：FFI, Ghidra, P-Code, Python, QF_ABV 逻辑, Rust, SLEIGH, SMT 求解器, TLS抓取, Z3, 中间语言, 二进制分析, 云安全监控, 云安全运维, 云资产清单, 代码建模, 可视化界面, 可配置程序分析, 可配置连接, 形式化验证, 无后门, 程序分析, 符号执行, 系统运维工具, 网络流量审计, 软件安全, 逆向工具, 逆向工程, 通知系统, 静态分析