MicroSMT

MicroSMT 是一个IDA Pro插件，用于通过将微代码提升到z3进行SMT推理来自动去混淆不透明谓词。其核心功能包括从`jcc`/`setcc`指令反向切片并将其相关的Hex-Ray微代码片段提升为z3表达式，进而求解这些表达式并对指令进行相应修补。该项目适合于需要对二进制文件中的控制流保护进行分析和去混淆的场景，特别是针对恶意软件分析领域。需要注意的是，当前版本处于预alpha阶段，存在一些限制，例如无法处理依赖内存访问或跨多个基本块的谓词等复杂情况。尽管如此，MicroSMT已经能够在某些恶意软件家族中自主解决不透明谓词问题。