WEBKT

逆向工程进阶：基于 LLVM Pass 与 Z3 SMT Solver 自动化移除不透明谓词

3 0 0 0

1. 什么是不透明谓词？

在代码混淆（Code Obfuscation）领域，不透明谓词（Opaque Predicates） 是一种常用的手段。简单来说，它是一个在程序运行时结果始终固定（永远为真或永远为假）的表达式，但编译器在静态分析时却难以推断出其结果。

例如，表达式 (x * x + x) % 2 == 0 对于任何整数 x 始终为真。混淆器通过引入这种谓词，可以将原本简单的直线型代码分支化，诱导反汇编器生成复杂的控制流图（CFG），从而大幅提升逆向工程的难度。

2. 识别思路：静态分析的挑战

传统的编译器优化（如 LLVM 的 Constant Propagation）只能处理简单的常量表达式。对于涉及复杂代数恒等式或数论特性的不透明谓词，编译器往往无能为力。

为了识别这些“伪分支”，我们需要引入更强大的工具——SMT（Satisfiability Modulo Theories）解算器。通过将 LLVM IR 中的分支条件提取并转化为逻辑公式，我们可以请求 SMT 解算器（如 Microsoft 的 Z3）验证该公式是否为重言式（Tautology）。

3. 实现架构：LLVM Pass + Z3

我们的目标是编写一个 FunctionPass，遍历函数中的所有基本块，识别 BranchInst 并在可能的情况下将其简化。

3.1 环境准备

  • LLVM 12.0+ 源码环境
  • Z3 库（libz3-dev）
  • CMake 构建系统

3.2 将 LLVM IR 条件转换为 Z3 公式

这是最核心的一步。我们需要实现一个简单的转换器，将 LLVM 的 Value 映射到 Z3 的表达式。

z3::expr llvmToZ3(Value *v, z3::context &ctx) {
    if (auto *CI = dyn_cast<ConstantInt>(v)) {
        return ctx.bv_val(CI->getSExtValue(), 64);
    }
    if (auto *BI = dyn_cast<BinaryOperator>(v)) {
        z3::expr lhs = llvmToZ3(BI->getOperand(0), ctx);
        z3::expr rhs = llvmToZ3(BI->getOperand(1), ctx);
        switch (BI->getOpcode()) {
            case Instruction::Add: return lhs + rhs;
            case Instruction::Mul: return lhs * rhs;
            case Instruction::And: return lhs & rhs;
            // ... 处理更多操作符
        }
    }
    // 对于未知变量，映射为 Z3 符号变量
    return ctx.bv_const(v->getName().str().c_str(), 64);
}

3.3 谓词判定逻辑

利用 Z3 的推断能力。如果我们怀疑条件 P 是恒真谓词，我们尝试证明 Not(P) 是不可满足的（Unsatisfiable）。

bool isAlwaysTrue(z3::expr &e, z3::context &ctx) {
    z3::solver s(ctx);
    s.add(!e);
    return s.check() == z3::unsat;
}

4. 编写 LLVM Pass 进行重构

在 Pass 的 runOnFunction 中执行以下逻辑：

  1. 遍历基本块：定位所有以条件分支（BranchInst）结束的块。
  2. 符号化提取：获取分支条件的 Value 指针，递归构建 Z3 表达式。
  3. 约束求解：
    • 如果 isAlwaysTrue(cond)，则将该分支替换为指向 True 目标的无条件跳转。
    • 如果 isAlwaysFalse(cond)，则替换为指向 False 目标的无条件跳转。
  4. 死代码清理：移除替换后变得不可达的基本块。
virtual bool runOnFunction(Function &F) override {
    bool changed = false;
    for (auto &BB : F) {
        auto *TI = BB.getTerminator();
        if (auto *BI = dyn_cast<BranchInst>(TI)) {
            if (BI->isConditional()) {
                z3::context ctx;
                z3::expr condExpr = llvmToZ3(BI->getCondition(), ctx);
                
                if (isAlwaysTrue(condExpr, ctx)) {
                    // 替换为无条件跳转到第一个目标块
                    BranchInst::Create(BI->getSuccessor(0), BI);
                    BI->eraseFromParent();
                    changed = true;
                } else if (isAlwaysFalse(condExpr, ctx)) {
                    // 替换为无条件跳转到第二个目标块
                    BranchInst::Create(BI->getSuccessor(1), BI);
                    BI->eraseFromParent();
                    changed = true;
                }
            }
        }
    }
    return changed;
}

5. 后置处理与局限性

5.1 CFG 简化

移除谓词后，代码中会留下大量无用的分支和孤立的基本块。建议在自定义 Pass 运行后，挂载 LLVM 自带的 SimplifyCFGPass 和 ADCEPass（侵略性死代码消除），以恢复原始的代码逻辑结构。

5.2 局限性分析

  1. 全局状态依赖：如果谓词依赖于内存状态（如全局变量、指针解引用），上述纯代数识别将失效。需要引入 MemorySSA 或更复杂的别名分析。
  2. 循环诱导变量：某些不透明谓词在循环内部通过多轮迭代建立。这需要结合 LoopInfo 进行归纳变量分析。
  3. 性能开销：对于超大型函数，频繁调用 SMT Solver 会导致编译耗时剧增。实际工程中通常会对表达式深度进行限制。

6. 总结

通过将 LLVM 强大的 IR 操作能力与 Z3 的逻辑推理能力相结合，我们可以构建出一个自动化的反混淆利器。这不仅能有效应对诸如 Tigress 或 Hikari 等混淆工具产生的控制流干扰，也为更深入的代码安全审计打下了基础。对于安全研究员而言，掌握 LLVM Pass 的编写是迈向高端自动化分析的必经之路。

CompilerOps LLVM代码混淆SMT Solver

评论点评