eversinc33/MicroSMT

# MicroSMT MicroSMT 是一款 IDA Pro 插件，旨在通用化地解决不透明谓词。 它通过从 `jcc`/`setcc` 指令进行反向切片，并将相关的 Hex-Ray 微代码片段提升为 z3 表达式。这些表达式可以通过 SMT 求解，然后相应地修补指令。 MicroSMT 目前处于 *pre-alpha* 状态——使用微代码存在一些陷阱，我并不期望它能处处可用。此外，lifter 尚未实现所有指令的支持。 尽管如此，MicroSMT 已经能够自主解决多个系列的不透明谓词（见下文示例）。 在可解决的不透明谓词方面存在一些限制——值得注意的例外包括： * 依赖内存访问的谓词 * 依赖外部 API 调用及其返回结果的谓词 * 跨越多个基本块的谓词 对于这些类型，我建议使用完整的符号执行或类似方法。 *MicroSMT 已在 IDA Pro 9.2 上进行过测试* ### 安装说明 将 `MicroSMT.py` 复制到您的 IDA 插件文件夹（例如 `~/.idapro/plugins`）。请确保已通过 `pip` 安装 `z3`。 ### 使用方法 将光标指向 `jcc` 或 `setcc` 指令，按下 `Alt+m`，MicroSMT 将判断该条件是否为不透明谓词，如果是，则进行求解。如果您在插件设置菜单中勾选修补选项，MicroSMT 还将进行相应修补（例如将 `jcc` 修补为 `nop` 或 `jmp`，或将 `setcc` 替换为赋值 0 或 1）。 ### 示例 ``` Lumma Stealer 00f1a9c6185b346f8fdf03e7928facfc44fc63e6a847eb21fa0ecd7fb94bb7e3 ```  ``` ANELLOADER (Apt10) 362b0959b639ab720b007110a1032320970dd252aa07fc8825bb48e8fdd14332 ```  ### 设计动机 在为一个 bin2bin 混淆器实现 IR lifter 时，我产生了将微代码提升到 z3 以进行去混淆的想法。由于我以前在逆向工程中从未真正使用过 SMT，而是通常依赖动态分析/追踪，所以我想尝试一下。此外，我喜欢对问题采取通用/自动化的解决方案，而 MicroSMT 正好填补了我所需的工具空白。

标签：CTF工具, DAST, Hex-Rays, IDA Pro插件, SMT求解, Z3, 不透明谓词, 二进制分析, 云安全监控, 云安全运维, 云资产清单, 去混淆, 反混淆, 可配置连接, 微代码分析, 恶意软件分析, 指令切片, 漏洞分析, 漏洞搜索, 程序分析, 符号执行, 自动化分析, 跨站脚本, 路径探测, 逆向工具, 逆向工程, 静态分析