symbolic-execution-tools

来源: yaklang/hack-skills · 安装量: 1.6K · 优先级: P1

利用符号执行引擎进行自动化反混淆和约束求解。

支持的工具

工具	用途
angr	二进制符号执行平台，支持多架构
Z3	SMT 求解器，处理 Opaque Predicates 等约束问题
Triton	动态符号执行框架，支持 taint 分析

利用 Z3 对混淆中插入的永真/永假条件进行自动求解，识别并移除虚假分支。

使用 angr 的仿真执行（SimExe）在不运行恶意代码的情况下模拟脱壳过程。

通过符号执行追踪数据流，恢复被混淆中断的变量关系。