抽象

现代最强：

vs

过去最强：

正文开始

第一次写文章肯定会有不足之处，欢迎评论区指出
当尝试逆向还原 VMProtect 等混淆保护时，会有以下几种结局：

• 上下文爆炸：模型被冗长的汇编指令淹没，流一地口水（最可能的结局）。
• Token 焦虑：舍不得烧 token，给自己累死了。
• 借过一下。
• 我是黑客：直接对着 Trace 出来的执行流，一句一句手工解密。

——很显然，工具就是用来提升效率的！

本文是设计篇：把架构、编码方案和验证机制讲清楚。真实 VMP 样本上的实测数据（压缩率、首轮命中率、Z3 判定分布、收敛轮数）会在下篇集中放出，欢迎提前挑刺。

以下内容大部分因为没有合适的例子我没法去审查如有错误可以指出!有例子之后发的第二篇(后面整个框架会发出来)将会采纳!

本质原因

为什么 AI 处理混淆汇编如此吃力？归结为三点：

1. 汇编不是为 LLM 设计的
   指令集的表达方式（寄存器、跳转、栈操作）对自然语言模型而言是天然的"高熵"输入。一条 mov r8, [rsp+0x40] 占二十几个字符，其中真正承载语义的不过"读栈上偏移 0x40"这几个 bit——信噪比极低。

2. 幻觉比看不懂更致命
   让模型直接逐条解释汇编，它没有真实的寄存器状态，只能"猜"语义。猜错不可怕，可怕的是它猜得理直气壮——ROL 和 ROR 方向反了这种错误，混在一万行输出里根本看不出来。

3. 现有压缩方法太垃圾
   通用压缩（按行截断、丢弃注释）破坏语义完整性；而面向逆向场景的专用压缩方案又极度匮乏。压缩错了方向，等于给模型喂假药。

解决方案构想

问题（2）靠 prompt 是救不了的，得靠机制。于是整体思路定为：

确定性流水线负责"压缩与搬运"，LLM 只负责"提出假设"，形式化验证负责"最终判定"。

三者的信任等级完全不同：流水线是机械的，可信；LLM 是会幻觉的，它的产出永远只是"待验证的假设"；Z3（SMT 求解器）是数学家，它说等价才是真的等价。

更具体地说：构建一个面向 VMP 还原的汇编上下文压缩框架。

整体的架构

设计目标

对保护后的指令流进行无损语义压缩，输出 LLM 能高效处理的精简汇编（这时候叫 IR 其实更好）。

架构分层

注意：整体面向的是语义压缩而不是字节压缩！

这句话再展开半句：框架里其实有两类压缩——

• 编码级压缩：纯换写法，一条指令都不动，可逆展开还原。这类压缩"免费"，不需要任何证明。
• 语义级压缩：真的删指令（比如 VM 算了但从来没人用的 flag 计算）。这类压缩必须证明自己删的东西不可观察——删错了就是改变了程序行为，后面全白搭。

说明：以下实验部分由 Kimi 集群代跑，笔者还没在本地完整复现（绝对不是我懒，确信）。文中压缩率基于手搓的标准样本，真实 VMP 样本到位后数字会在下篇修正/补充，也欢迎各位提供样本！

核心：五层无损编码

直接上效果。原始：

0x1400012A0: mov r8, [rsp+0x40]
0x1400012A5: jmp qword ptr [r8*8+0x140030000]
0x1400012AC: push rax
0x1400012AD: mov rbx, 0x9E3779B9
0x1400012B7: xor rbx, rax

压缩后：

^1; pu a; mv b,K0; ^b,a

158 字符变 23 字符（^1 是指向字典第 1 条的引用——开头那对"取指 + 查表跳转"的 dispatcher 骨架在字典里只存了一份）。五层分别是：

关键设计两条：

• 映射表随包发 + 固定文法：LLM 不需要在预训练里"学过"这套编码——映射表和文法随压缩包一起注入 prompt，相当于现场发教材、开卷考试，而不是闭卷猜谜。顺带这份表直接就是中间 DSL 的文法定义，一份表三处用（编码器、文法文档、LLM 教材），全部代码生成，杜绝手工维护漂移。

  文法约定（核心几条，完整表随包发）：

  • 立即数一律十六进制、省略 0x 前缀；负数同样按十六进制解读（#-4 = -0x4）；
  • < 是 lsl 的短码（ld 9,[9,8,<#3] = ldr x9, [x9, x8, lsl #3]）；
  • EF 是副作用封装标记（effectful）：被它包裹的指令（如 svc）原样保留，任何压缩层不得改动其内容；
  • 映射表是唯一权威：表里没有的符号不许出现在输出里。

• 可逆性有测试兜底：编码 → 展开 → 和原文逐条比对，差一条整条流水线停摆。这个测试叫 roundtrip，是整个框架的出生证明。

压缩率实测

先拿 ARM64 hello world 试刀（10 条指令）：压掉 47%（体积剩余 53%）。别急着笑——hello world 没有重复序列，字典层根本没吃上力。

光拿 hello world 说服力不够，于是我ai手搓了一个微型 VM 当靶子——3 个 handler + 线程化 dispatch，dispatch 骨架按 VMP 风格在每个 handler 末尾内联一份，完整源码如下：

// vip = x19（虚拟PC），vsp = x20（虚拟栈指针）
// 字节码: 00 05 00 02 01 02 = VPUSH 5; VPUSH 2; VADD; VOUT → 打印 '7'
_start:
    adrp x19, bytecode
    add  x19, x19, :lo12:bytecode
    adrp x20, vstack
    add  x20, x20, :lo12:vstack
    add  x20, x20, #256
    br   dispatch

dispatch:                        // 取指-译码-跳转（独立副本）
    ldrb w8, [x19], #1           // opcode = *vip++
    adrp x9, handler_table
    add  x9, x9, :lo12:handler_table
    ldr  x9, [x9, x8, lsl #3]    // 查 handler 表
    br   x9

h_vpush:                         // handler 0: VPUSH imm8
    ldrb w10, [x19], #1
    str  w10, [x20, #-4]!
    ldrb w8, [x19], #1           // ── dispatch 骨架内联副本 #1 ──
    adrp x9, handler_table
    add  x9, x9, :lo12:handler_table
    ldr  x9, [x9, x8, lsl #3]
    br   x9

h_vadd:                          // handler 1: VADD（弹二压一）
    ldr  w10, [x20], #4
    ldr  w11, [x20], #4
    add  w10, w10, w11
    str  w10, [x20, #-4]!
    ldrb w8, [x19], #1           // ── dispatch 骨架内联副本 #2 ──
    adrp x9, handler_table
    add  x9, x9, :lo12:handler_table
    ldr  x9, [x9, x8, lsl #3]
    br   x9

h_vout:                          // handler 2: VOUT（弹栈顶打印）
    ldr  w10, [x20], #4
    add  w10, w10, #0x30         // 数字 → ASCII
    adrp x11, outbuf
    add  x11, x11, :lo12:outbuf
    strb w10, [x11]
    mov  x0, #1
    mov  x1, x11
    mov  x2, #1
    mov  x8, #64                 // write(1, outbuf, 1)
    svc  #0
    mov  x0, #0
    mov  x8, #93                 // exit(0)
    svc  #0

结构就是 VMP 的等比缩小：x19 当 vip、x20 当 vsp、handler 表跳转、字节码驱动。这个 VM 跑 VPUSH 5; VPUSH 2; VADD; VOUT，5+2=7 转字符打印——已用 unicorn 模拟器实际执行验证，输出确实是 7。样本语义已知、结构典型、可执行，这就是后面所有测试的"标准答案"。

编码器过一遍，输出：

DCT 1: ldb 8w,[J],#1; la 9,L1; ld 9,[9,8,<#3]; br 9

BLK _start:  la J,L3; la K,L4; +K,K,#100; ^1
BLK h_vpush: ldb Aw,[J],#1; st Aw,[K,#-4]!; ^1
BLK h_vadd:  ld Aw,[K],#4; ld Bw,[K],#4; +Aw,Aw,Bw; st Aw,[K,#-4]!; ^1
BLK h_vout:  ld Aw,[K],#4; +Aw,Aw,#30; la B,L2; stb Aw,[B]
             mv 0,#1; mv 1,B; mv 2,#1; mv 8,#40; EF svc #0
             mv 0,#0; mv 8,#5D; EF svc #0

注意看三个 handler 末尾那坨五条的 dispatch 骨架，在编码结果里全部变成了 2 个字符的 ^1——字典里只存了一份。副作用指令 svc 被 EF 原样封装，任何压缩层都不许碰它。

实测数字：样本原文约 1385 字符（含注释）→ 编码输出 381 字符，体积剩余约 28%，压掉约 72%。对比 hello world 的 47%，字典层在重复骨架上的贡献一目了然。当然这只是等比缩小的玩具 VM——真实 VMP 样本混淆密度更高、重复模式更多，数字会更好看还是更难看，下篇见分晓。

防幻觉：LLM 提议，Z3 判定

这是整个框架的命门，单独一节。

先说理论位置：这个设计本质上是把 CEGIS（反例引导归纳合成） 搬到了 LLM 时代——LLM 扮演"提议器"（和 Syntia [15]、QSynth [16] 里的程序合成引擎同一个生态位），SMT 求解器扮演"验证器"，反例驱动迭代。区别在于：程序合成引擎的搜索空间是语法树，慢但严谨；LLM 的"搜索空间"是它预训练见过的所有混淆模式，快但会幻觉。两者刚好互补，Z3 是那个不让 LLM 乱来的裁判 [12]。而"用求解器验证两段代码语义等价"这件事本身，是超优化（superoptimization）领域验证了十几年的成熟路径（STOKE [19]、Souper [20]：找等价但更短的指令序列，等价性由求解器背书）。

LLM 读完压缩 IR 后的产出，不允许是自然语言结论，必须写成可执行的断言（claim），比如：

{
  "block": "0x4012A0",
  "claim": "v3 == ROL(XOR(LOAD8[v0+0x18], 0x9E3779B9), 13)",
  "intent": "rolling key 更新（这段自然语言只给人看，永不参与判定）"
}

然后走双通道对照：

• 通道 B（真值）：符号执行引擎把原始 block 逐条算出精确的位向量公式；
• 对照器：把 claim 和符号执行结果编译到同一个 SMT 平面，问 Z3："存在让两者不同的输入吗？"
  • UNSAT（不存在） → 数学证明等价，放行，标记 PROVEN；
  • SAT（存在） → Z3 直接吐出反例输入，连反例一起打回给 LLM："这个输入下你错了，修正。"按 CEGIS 类系统的经验，预期 2~3 轮内收敛——注意这是设计预期，实测收敛数据同样留给下篇；
  • 超时 → 降级到模拟器差分测试（随机+边界值输入，两边具体执行比对输出），标记 FUZZED，可信度低一档。

最终报告里每个 block 都带三档可信度之一：PROVEN / REFUTED / FUZZED。没有"我觉得等价"这个档位。

能力边界（诚实声明）

这套机制的软肋不在 LLM，而在真值通道本身：Banescu [21]、Loki [22] 这类抗符号执行混淆（SMT-hard 谓词、路径爆炸炸弹）攻击的正是符号执行引擎。框架的应对是把符号执行限制在 block 级、控制爆炸半径，但对刻意构造的对抗样本，真值通道仍可能直接超时——这时候框架不会假装等价，而是整块降级为 FUZZED，甚至标记 UNVERIFIED 拒收，并在报告里如实暴露。验证不了就承认验证不了，这是和"LLM 觉得等价"之间的最后一条底线。 符号执行引擎输出的 bit-vector 公式与 LLM 的 claim 之间，需要一层变量名映射表——符号执行用 R_AX、MEM_0x18_OFFSET 这类内部名，LLM 用 v0、v3，两者必须归一化到同一个 SMT 命名空间才能比对。映射构造机制在下篇结合具体 VMP 样本展开。

教练模块：让通用大模型变专家

框架默认用 GPT / Claude 这类通用模型，它们没专门训过混淆代码，直接上岗命中率堪忧。所以加了个 instructor（教练层）：

• 教材小册：VMP 心智模型、rolling key 常见形式、MBA 混淆恒等式速查，每册 500~1500 token，按需注入而不是一次性灌满；
• 模式卡片库：x^y = (x|y)-(x&y) 这类教科书形态做成可检索卡片，看到对应特征自动塞进 prompt；
• 失败手册：每次 Z3 打回的反例沉淀成一条"错题本"，下次遇到相似结构自动附上——模型犯过的错不允许犯第二次；
• 已验证样例库：只有通过 Z3 判定的案例才配进 few-shot 库，未验证的一个不收。

注意定位：instructor 提升的是假设命中率（第一轮就猜对的比例），兜底正确性的永远是 Z3。它是效率组件，不是信任组件——所以可以放心把它做厚。

目前的进度

已经 vibe 出框架的雏形了，接下来进入实战验证阶段。容易复现的真实 VMP 样本还在征集中（其实是我懒），样本到位、实测跑完之后会发下篇实测帖。

相关工作与理论位置

混淆变换的分类学基础见 Collberg 的经典工作 [1][2]，此处不再赘述。各模块的理论位置与代表工作：

和已有轮子的差别：

• Yadegari / VMHunt / Salwan 这条路 [5][7][8]：全自动符号执行去虚拟化，严谨但重——路径爆炸、对强混淆样本收敛慢，且输出是"代码"而不是"给 LLM 的上下文"。本框架的符号执行只做到 block 级，重活交给契约拼接，目的就是给 LLM 喂得起。
• Syntia / MBA-Blast 这条路 [15][17]：表达式级化简极强，但不管 VM 结构、不管上下文工程。本框架把它们的技术收编为"压缩层的提议通道"，产出统一过 Z3。
• 纯 LLM 反混淆这条路 [25]：DIMVA'25 的实测表明微调后的小模型在源码级混淆（Tigress）上确实能取得不错的化简效果——但它做的是 C 源码级，不管二进制、不管 VM 结构，且产出没有求解器背书，对了错了没人判。本框架补的正是"机器生成的真值 IR"和"求解器判定"这两根柱子，同时把免微调的通用大模型当作提议器来用。
• VTIL [26]：开源界的 VMP 去虚拟化实现，本框架的 IR 设计大量参考它，值得 star。

参考文献

[1] Collberg C, Thomborson C, Low D. A Taxonomy of Obfuscating Transformations. 1997.
[2] Collberg C, Nagra J. Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection. Addison-Wesley, 2009.
[3] Coogan K, Lu G, Debray S. Deobfuscation of Virtualization-Obfuscated Software: A Semantics-Based Approach. ACM CCS, 2011.
[4] Kinder J. Towards Static Analysis of Virtualization-Obfuscated Binaries. WCRE, 2012.
[5] Yadegari B, Johannesmeyer B, Whitely B, Debray S. A Generic Approach to Automatic Deobfuscation of Executable Code. IEEE S&P, 2015.
[6] Yadegari B, Debray S. Symbolic Execution of Obfuscated Code. ACM CCS, 2015.
[7] Xu D, Ming J, Fu Y, Wu D. VMHunt: A Verifiable Approach to Partially-Virtualized Binary Code Simplification. ACM CCS, 2018.
[8] Salwan J, Bardin S, Potet M-L. Symbolic Deobfuscation: From Virtualized Code Back to the Original. DIMVA, 2018.（配套工具 Triton，SSTIC 2015）
[9] Kochberger P, Schrittwieser S, Schweighofer S, Kieseberg P, Weippl E. SoK: Automatic Deobfuscation of Virtualization-Protected Applications. ARES, 2021.
[10] Cadar C, Dunbar D, Engler D. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. OSDI, 2008.
[11] Baldoni R, Coppa E, D'Elia D C, Demetrescu C, Finocchi I. A Survey of Symbolic Execution Techniques. ACM Computing Surveys, 2018.
[12] de Moura L, Bjørner N. Z3: An Efficient SMT Solver. TACAS, 2008.
[13] Eyrolles N, Goubin L, Videau M. Defeating MBA-Based Obfuscation. ACM SPRO, 2016.
[14] Eyrolles N. Obfuscation with Mixed Boolean-Arithmetic Expressions: Reconstruction, Analysis and Simplification Tools. PhD Thesis, Université Paris-Saclay, 2017.
[15] Blazytko T, Contag M, Aschermann C, Holz T. Syntia: Synthesizing the Semantics of Obfuscated Code. USENIX Security, 2017.
[16] David R, Coniglio L, Ceccato M. QSynth: A Program Synthesis Based Approach for Binary Code Deobfuscation. BAR Workshop (NDSS), 2020.
[17] Liu B, Shen J, Ming J, Zheng Q, Li J, Xu D. MBA-Blast: Unveiling and Simplifying Mixed Boolean-Arithmetic Obfuscation. USENIX Security, 2021.
[18] Xu D, Liu B, Feng W, Ming J, Zheng Q, Li J, Yu Q. Boosting SMT Solver Performance on Mixed-Bitwise-Arithmetic Expressions. PLDI, 2021.
[19] Schkufza E, Sharma R, Aiken A. Stochastic Superoptimization. ASPLOS, 2013.
[20] Sasnauskas R, Chen Y, Collingbourne P, et al. Souper: A Synthesizing Superoptimizer. 2017.
[21] Banescu S, Collberg C, Ganesh V, Newsham Z, Pretschner A. Code Obfuscation Against Symbolic Execution Attacks. ACSAC, 2016.
[22] Schloegel M, Blazytko T, Contag M, et al. Loki: Hardening Code Obfuscation Against Automated Attacks. USENIX Security, 2022.
[23] Feng W, Liu B, Xu D, Zheng Q, Xu Y. NeuReduce: Reducing Mixed Boolean-Arithmetic Expressions by Recurrent Neural Network. EMNLP (Findings), 2020.
[24] Lachaux M-A, Rozière B, Szafraniec M, Lample G. DOBF: A Deobfuscation Pre-Training Objective for Programming Languages. NeurIPS, 2021.
[25] Beste D, Menguy G, Hajipour H, et al. Exploring the Potential of LLMs for Code Deobfuscation. DIMVA, 2025.
[26] can1357. VTIL: Virtual-machine Translation Intermediate Language. GitHub 开源项目.

欢迎评论区指正。本文约一半由 K3 完成，我就提了个思路——ai 太好用了你知道吗。实测篇数据到位之前，这篇先当readme放着！Z3部分因为没有经过实战验证所以整体暂时不放出来

冰与火的战歌：Windows内核攻防实战高级班！从零到实战，融合AI与Windows内核攻防全技术栈，打造具备自动化能力的内核开发高手。