MicroSMT

MicroSMT 是一个 IDA Pro 插件，用于自动识别并求解混淆代码中的不透明谓词。其核心功能是通过反向切片定位跳转/设置类指令，将相关 Hex-Rays 微码片段提升为 Z3 表达式，借助 SMT 求解器判定谓词恒真或恒假，并支持自动打补丁（如 NOP 化跳转或替换 setcc）。技术上依赖微码分析与符号执行结合，当前仅支持无内存访问、无外部调用、单基本块内的谓词。适用于恶意软件分析、逆向工程中对抗控制流扁平化等静态混淆场景。