[论文] LLMs 能恢复程序语义吗？使用 Symbolic Execution 的系统性评估

Source: arXiv - 2511.19130v1

概览

本文研究了大型语言模型（LLM）是否能够“撤销”代码混淆——这是一项开发者在理解、测试或保护软件时常遇到的难题。通过使用 KLEE 引擎进行符号执行生成的数据对 LLM 进行微调，作者展示了 LLM 能够比单纯微调更可靠地恢复原始程序语义。

关键贡献

• 去混淆基准套件 – 对来自 TUM 混淆基准、LLVM 测试套件以及算法仓库的多样化 C 程序，应用 4 种经典混淆技术（控制流平坦化、不透明谓词、算术编码、分支编码）。
• 混合训练流水线 – 基线微调使用混淆/原始代码对，增强模式则注入 KLEE 生成的制品（SMT 约束、路径统计、具体测试用例）。
• 全面评估指标 – 编译成功率（语法正确性）、符号执行下的行为等价性（语义保真度）以及代码质量分数（可读性/结构）。
• 实证发现 – GPT‑4.1‑mini 始终优于其他最先进的 LLM，且加入 KLEE 的训练在整体上提升了语义保持能力。
• 实践洞见 – 表明将 LLM 与符号执行相结合，即使在代码被有意或无意混淆的情况下，也能提升自动化测试、静态分析和程序理解的效果。

方法论

1. 混淆生成 – 作者对每个源文件程序化地应用四种成熟的转换，生成每个原始程序的多个混淆变体。
2. 符号执行数据收集 – 对每对原始/混淆代码，运行 KLEE 产生：
   • 描述每条执行路径的 SMT（可满足模理论）约束，
   • 路径级统计信息（如分支数、循环上限），以及
   • 实现高路径覆盖率的具体测试用例。
3. 模型微调 – 对三种主流 LLM（包括 GPT‑4.1‑mini）在两种模式下进行微调：
   • 基线： 简单的“混淆 → 原始”代码翻译对。
   • 增强： 在相同对的基础上拼接 KLEE 制品作为辅助上下文。
4. 评估流水线 – 生成后，每个去混淆的输出会：
   • 编译以验证语法正确性，
   • 再次通过 KLEE 检查符号行为是否与原程序匹配，
   • 使用可读性指标（如环形复杂度、命名约定）打分。

整个工作流全自动化，支持可复现的大规模测试。

结果与发现

• 编译成功率 在加入 KLEE 制品后提升 15‑25 个百分点，说明额外的语义提示帮助模型避免了非法的语法改写。
• 语义保真度（符号执行下的行为等价）在所有模型上提升约 20 个百分点，证实去混淆代码实际执行的功能与原始代码相同。
• 可读性 分数略有上升；经过 KLEE 增强训练后，生成的代码通常具有更清晰的控制流和更常规的命名。
• GPT‑4.1‑mini 始终产生最可靠的去混淆结果，可能得益于其更大的上下文窗口和更强的推理能力。

实践意义

• 自动化逆向工程 – 安全团队可以将混淆的二进制先通过反编译得到 C 表示，再使用 KLEE‑增强的 LLM 恢复可读版本，加速漏洞排查。
• 稳健的静态分析 – 依赖源代码信息的工具（如 linter、类型检查器、形式化验证器）可在第三方库上预处理此方法，缓解编译器优化或有意混淆带来的“黑箱”效应。
• 持续集成与测试 – 当构建流水线使用激进的优化导致代码意外变得难以阅读时，去混淆步骤可以重新生成干净的代码供下游测试框架使用，保持测试覆盖率指标。
• 开发者生产力 – 在大型代码库中，若遗留模块被压缩或大量宏展开，开发者可以向 LLM 请求一次“语义清理”，得到既能编译又行为相同但更易阅读和修改的代码。

对从业者的关键启示是 符号执行数据充当了强大的“语义锚点”，使 LLM 从纯模式匹配转变为尊重程序行为的工具。

局限性与未来工作

• 语言范围 – 本研究仅聚焦 C 程序；扩展到 C++、Rust 或托管语言可能会出现新挑战（如模板、垃圾回收）。
• KLEE 的可扩展性 – 对大型代码库进行符号执行成本高昂，作者指出路径爆炸限制了可处理程序的规模。
• 混淆多样性 – 只评估了四种经典转换；现代打包器、基于虚拟化的混淆器或 AI 生成的混淆仍未覆盖。
• 模型规模与成本 – 虽然 GPT‑4.1‑mini 表现最佳，但在 CI 流水线中运行大型 LLM 可能成本过高；未来工作可探索在保持语义优势的前提下进行蒸馏或量化的模型。

作者建议进一步研究 增量式符号反馈…