1. 问题起源为什么单独把“malloc地址单元符号化”拎出来讲写这一篇纯属被坑出来的。前面几篇笔记里我一直在处理“标准输入符号化”“argv符号化”这类常规操作当时觉得 angr 已经很顺手了直到遇到一个程序逻辑看起来非常简单就是读入一段数据经过一个校验函数对了就打印 flag。结果 angr 跑下来路径倒是探索了一堆但求解器死活给不出一个合法的输入。最后排查了半天问题就出在 malloc 分配的地址内容没有被符号化上。这里先解释一下背景。符号执行的本质是把输入变成符号变量让程序带着符号跑碰到分支就把条件收集起来最后交给约束求解器去解。但这里的“输入”是有范围的你符号化的是 stdin、argv 还是某个全局缓冲区angr 只会把明确标成 BVSBitVectorSymbolic的那部分内存当成“可变”的其余内存内容 angr 会按具体值处理。malloc 出来的堆区怎么处理就很微妙了。它不像栈上声明的数组有明确的地址和大小malloc 返回的地址在符号执行里是动态生成的angr 默认不知道你这个地址指向的内存区域代表什么含义更不会主动给这块内存灌入符号变量。结果就是程序从堆区读数据、做比较angr 真以为堆里那些字节是“固定值”于是产生了大量不可能满足的条件分支。这也就引出了本篇笔记要讲的方案如何让 malloc 分配出来的那块地址空间其内容也成为符号变量从而让符号执行真正覆盖到程序的核心校验逻辑。这篇笔记适合两类人看。一类是刚接触 angr、只跑通过几道入门题准备挑战真实程序的人malloc 符号化是绕不过去的一关。另一类是已经会用 angr 但经常遇到“求解无解”“分支全走死”这类问题、排查无头绪的人。本篇会从原理讲到实操最后给出排查技巧核心是一个可复现的 Demo万金油思路。2. 能力铺垫angr 符号执行里“内存状态”的本质2.1 从符号变量到约束求解angr 到底在做什么angr 跑一个程序时维护的是一个“符号状态”。这个状态可以理解成一张大表记录了当前执行到的指令地址、寄存器的值、内存中每个地址的内容。这些“值”有两种形态一种是确定的具体数值比如0x401000另一种是符号变量比如一个 32 位的BVS(input_0, 32)它不是一个固定值而是一个“待定值”。angr 在模拟执行过程中遇到分支指令比如cmp; jz时会同时探索两个方向每条路径上都会记录一个路径条件。比如某条路径可能记录了input_0 0x41另一条路径可能记录了input_0 0x41。到最后你想让某一条路径走到 “success” 分支就把这条路径上所有的路径条件收集出来连同你自己手动添加的其他约束一起交给底层求解器z3去解。z3 会返回一个具体的数值使得这些条件全部成立。这个数值就是让程序走进目标分支的输入。这个模型看似简单但注意一个关键点约束求解器只能基于符号变量去求解。如果一个值不是符号变量而是一个具体常量那 angr 是不可能“反过来算”出一个输入去改变它的。说得夸张一点如果你压根没把一个内存位置标记成符号那 angr 眼里它就永远是某个固定值哪怕程序逻辑上它初始依赖 stdin。所以 malloc 地址单元符号化本质上就是在回答一个问题堆上这块内存的“值”能不能随输入变化如果能angr 才有机会通过路径条件反推出输入如果不能那 angr 就只能看见一个死板的具体值路径探索也戛然而止。2.2 malloc 在符号执行里是“黑盒”问题就出在这真实程序里 malloc 可不是拿来看的。常见模式是程序从标准输入读固定字节数存到 malloc 得到的缓冲区里然后对这个缓冲区做字节变换、查表、比较。比如下面这类简化逻辑char *buf malloc(10); read(0, buf, 10); if (buf[0] f buf[1] l buf[2] a buf[3] g) { puts(correct); }如果是在真实系统上跑read会从 stdin 往 buf 指向的地址填充数据。但在 angr 里问题出现了angr 默认的read系统调用如果遇到未知的文件描述符通常是提前处理后返回确定值或触发异常具体行为取决于 angr 对read的模拟方式。即使你通过SimFile或者 hook 方式把 stdin 提供了也存在一个更深层的坑angr 的read模拟是写在系统调用层面的它的“目标地址”是 malloc 返回的那个地址。而 malloc 在 angr 的 SimHeap 里大多被 hook 成返回某个地址但这个地址指向的内存并没有被初始化为符号。于是你在状态里做了state.solver.BVS(stdin, 10*8)以为万事大吉实际上 angr 执行read时确实把符号变量“拷贝”到了 malloc 地址上但前提是你正确配置了 stdin 的文件描述符并且 angr 把这次 read 识别为读符号数据。如果程序不是走read而是先从 stdin 读到一个临时栈缓冲再手动memcpy到堆区那 angr 在 memcpy 时是逐字节复制符号变量的这种情况反而没事。真正出问题的场景是程序校验逻辑直接作用在 malloc 内容上但 malloc 的内容来源不是 angr 认识的符号通道而是来自程序内部的某种初始化逻辑。举个典型例子程序从 stdin 读入一串十六进制字符串strtol转换成整数再当作种子去初始化一个伪随机序列最后用这个序列去校验堆区的某个数据。strtol、srand、rand这些函数在 angr 里的模拟如果不做额外处理会产生具体数值所以堆区数据就不可能被符号化。这种情况下你必须跳过“生成链条”直接在 malloc 地址单元上做符号化——人为声明“这块内存的内容是符号变量”。2.3 为什么“符号化地址”不等于“符号化内容”这里有必要区分两个概念。一个是把 malloc 返回的指针值符号化一个是把 malloc 指向的内存内容符号化。很多入门教程讲“malloc 符号化”时说的是前者让 malloc 的返回值成为一个符号变量这样能让程序走不同的堆分配分支比如检查 malloc 是否失败。字符串比较常见的一个坑是在分析带堆喷的程序时需要让 malloc 返回不同的地址来探索堆布局分支。但本文讨论的“malloc 地址单元符号化”指的是后者malloc 返回的地址是确定的或可计算的但该地址上的内存单元内容是符号化的。打个比方你和朋友约好在一家餐厅见面地址是固定的但你不知道朋友在那家餐厅坐哪一桌内容你想通过一定规则反推出来。符号化内容就是给“坐哪一桌”这个变量建立数学模型让求解器去算。两者在 angr 里的具体操作位置也不同符号化返回值需要 hook malloc 本身符号化地址内容需要在 malloc 之后拿到地址再用 store 操作往这个地址写入 BVS。理解了这一点后面看别人代码就不容易晕。3. 方案选型四种“让 malloc 区域符号化”的方式对比3.1 方式一hook malloc拿到返回值后再 store BVS最直接的做法通过project.hook_symbol(malloc, hook_func)劫持 malloc 符号在 hook 函数里先返回一块地址通常用state.heap相关接口或直接返回一个固定地址然后立刻在这个地址上 store 一个 BVS。这样程序后续对这块地址的读取就读到了符号变量。import angr import claripy def malloc_hook(state): # 手动指定一块地址避开已有内存区域 addr 0x5000000 # 只是一个示例地址实际要选堆区 size 0x40 # 让 malloc 返回这个地址 state.regs.rax addr # 在这块区域写入 64 字节的符号值 sym claripy.BVS(heap_data, 8 * size) state.memory.store(addr, sym)这种方式的好处是直观你能控制全流程。坏处也很明显一个程序里不止一处调用 malloc如果你全都 hook 到一个统一处理所有 malloc 区域内容都一样同一个 BVS逻辑就乱了。所以这种方式更适合目标明确、malloc 调用点不多的情况一般实验里也就一两个关键 malloc。3.2 方式二在输入符号化阶段同步填充堆区域不少初学者看到“malloc 地址单元符号化”第一反应是我先不碰 malloc直接把符号变量写到那个地址不就行了比如你知道 malloc 返回地址的规律像 glibc 的 fastbin 在固定偏移就硬编码一个地址在initial_state里storeBVS。这种方式在很多 CTF 题目里很有效因为题目程序简单甚至不校验 malloc 的返回值。不过这种方式有个前提你必须知道 malloc 返回地址到底是多少。angr 里 malloc 的默认 implementation 通常返回一块固定的模拟堆地址每次运行基本一致。但不同版本的 angrSimHeap 的地址策略不一样你硬编码的地址可能会踩到 angr 给栈或全局区域预留的空间。稳妥起见可以在 setup 阶段 hook 住 malloc打印返回地址再决定往哪填充。3.3 方式三利用 angr 的 SimHeap 自定义分配器这是“正统”做法。angr 内部有SimHeap类体系比如SimHeapBrk、SimHeapLibc。通过自定义一个继承SimHeap的分配器重写_allocate方法在分配时自动记录所有 malloc 返回的地址并在返回前将地址写入符号变量。这样程序里所有 malloc 出来的区域内容都是“全新符号”每个 malloc 对应一个独立 BVS互不干扰。class SymHeap(angr.state_plugins.heap.SimHeapLibc): def _allocate(self, size, **kwargs): addr super()._allocate(size, **kwargs) sym claripy.BVS(fheap_{addr:x}, 8 * size) self.state.memory.store(addr, sym) return addr # 使用时 state.heap SymHeap()这种方式约束力最强但复杂度也高。还有坑过度的自动符号化会让路径条件爆炸。每个 malloc 区域都有一整块 BVS一旦程序对这块区域做逐字节比较angr 会为每个字节引入分叉状态数呈指数级增长。所以这种方式适合研究目的不适合直接对真实大型程序用。3.4 方式四高阶玩法——用 concretization 和约束定向符号化前面几种叫“宽泛符号化”还有更精细的定向符号化不让整个 malloc 区域一开始就是 BVS而是让它先保持具体值等 angr 执行到某个比较指令时发现该分支不可满足再“回头”把相关内存地址符号化。angr 确实存在某种程度上“从失败中学习”的机制——如果你在探索时设置了save_unconstrained常见的是保存未约束状态而不是自动回填符号。这里说的“回头符号化”通常要你手动根据失败路径的特征在特定地址上补充约束。这种方式我已经一年没在实战中用了因为多数情况下方式一和方式二够用。但了解这个概念有助于理解 angr 的局限符号执行不是魔法它要在“尽可能多地探索”和“避免状态爆炸”之间取舍。手动符号化 malloc 区域本质上就是一种人工引导这种取舍的行为。3.5 选型建议按判定条件选不按喜好选说实话我在自己的实践里没用过一种包打天下的方案。我建议按下面这个标准来选场景特征推荐方式理由程序 malloc 调用点少关键区域只有一处方式一代码短好控制调试直观CTF 题目、程序结构简单且 malloc 地址稳定方式二写起来最快能跑就行想系统分析某类程序需要让所有堆区域都可变方式三自动化程度最高但要防状态爆炸求解出现 unsat 或路径走死需要精确定位方式四实际是排查局部符号化灵活但依赖经验判断本篇下面的实操用方式一做演示因为最能体现“malloc 地址单元符号化”的思路先拿到地址再填充符号。把这一步走通其他方式就是在它的基础上做变通。4. 实操演示从零跑通“malloc 内容符号化”完整流程4.1 准备实验环境与模拟程序首先准备好 angr 环境。我用的版本是 angr 9.2往下的 9.0 和往上的 10.x 在 API 上有细微差别但核心思路一致。安装就是常规的pip install angr需要注意的是 angr 依赖的 z3-solver 版本可能跟系统其他包冲突建议建虚拟环境避免污染系统 Python。然后是模拟程序。本文要分析的 Demo 用 C 语言写成为了简化后面解释原理我刻意写得很“人工”#include stdio.h #include stdlib.h #include string.h int check(char *buf, int len) { if (buf[0] * buf[1] 0x861) { if (buf[2] buf[3] 0xcb) { if (buf[4] ^ buf[5] 0x5c) { return 1; } } } return 0; } int main(int argc, char **argv) { char *heap_buf (char *)malloc(0x20); // 模拟从某处填充数据关键是在符号执行中这块内容没有被正常符号化 memcpy(heap_buf, ABCDEF, 6); if (check(heap_buf, 6)) { puts(ok); } else { puts(bad); } return 0; }编译gcc -o demo demo.c -no-pie -fno-stack-protector。这里关掉 PIE 不是为了别的只是后面分析时地址固定方便说明问题。真实复现时你可以保留 PIEangr 也支持。这个 Demo 里check函数对 heap_buf 的内容做了几组算术校验。如果按常规思路直接跑会看到 angr 走到check之后两个分支都不可满足因为内存里是固定的ABCDEF算不出满足条件的解法。这正是我们要解决的。4.2 常规分析脚本与失败现象记录先写一个最常规的 angr 脚本看看失败长什么样import angr def main(): proj angr.Project(./demo, auto_load_libsFalse) state proj.factory.entry_state() sm proj.factory.simulation_manager(state) sm.explore(find0x4006a4, avoid0x4006ad) # 目标是 ok 分支 if sm.found: print(Found!) print(sm.found[0].posix.dumps(0)) else: print(No found) # 看看活跃状态情况 print(active:, len(sm.active)) for st in sm.active[:3]: print(st.solver.constraints[-3:]) if __name__ __main__: main()跑一下结果大概率是No found。这就说明内存内容确确实实没有被符号化程序执行到比较时就没有合法路径了。只用看路径活跃数会发现所有状态都是 unsatisfiable在sm.active里检查state.solver.satisfiable()会返回 False。这里要专门提醒一下在 angr 里一个状态“活着”不代表它能继续往后执行。很多人在sm.explore没找到结果时就打印sm.active里的状态数发现数量不少就觉得是不是其他 bug。实际上这些 active 状态很可能全是 unsat后续指令执行全是死胡同。所以排查时第一件事就是检查状态的可满足性。4.3 方案落地hook malloc 并符号化返回地址指向的内容现在按方式一改造。先 hookmalloc符号让 malloc 返回一个我们指定的地址并在这个地址上写入 BVS。angr 的hook_symbol接受一个符号名和 hook 函数。hook 函数的输入是state你可以在里面修改寄存器、内存、求解器约束。import angr import claripy def setup_malloc_sym(state): # 选一个地址作为“堆区”注意避开已知区域 fake_heap 0x600000 size 0x20 sym_data claripy.BVS(malloc_0, 8 * size) state.memory.store(fake_heap, sym_data) # malloc 的返回结果放在 rax state.regs.rax fake_heap然后把 hook 挂到符号上。angr 里hook_symbol的第一个参数是字符串对应程序里malloc在动态符号表中的名字。def main(): proj angr.Project(./demo, auto_load_libsFalse) proj.hook_symbol(malloc, setup_malloc_sym, length0) # length 为 0 表示完全替换写完这个 hook 之后重新用同样的 explore 跑就能在found里看到状态了。这时候可以 dump 一下标准输入如果你程序里有读入或者直接查看malloc_0这个符号变量的值found_state sm.found[0] solver found_state.solver solution solver.eval(claripy.BVS(malloc_0, 8 * 6), cast_tobytes) print(solution)如果不出意外你得到的 bytes 就是满足check条件的“目标值”比如bKI\xe5TZ之类。验证方式很简单用这个字节串替换 Demo 里 memcpy 的数据重新编译跑一下发现打印ok。这一步的关键点在于顺序必须先 store BVS 到地址再让 malloc 返回地址。如果反过来先设置 rax 再 storestore 的地址还是我们自己指定的理论上没区别但如果你 store 的地址依赖 rax 的内容那顺序就很重要。另外store 的 size 要跟后面读取的长度匹配只 store 6 字节也行但为了稳妥我会按整个分配大小 store 一整块 BVS后面读取哪一段都能命中。4.4 完整脚本与边界参数说明下面给一个完整的脚本可以直接替换地址、符号名跑别的程序用import angr import claripy fake_heap_base 0x200000 malloc_size 0x100 def malloc_hook(state): # 可以在这里打印调用栈或者分配大小便于调试 # state.inspect 相关用法可以拿到调用参数这里略过 addr fake_heap_base sym claripy.BVS(heap_0, 8 * malloc_size) state.memory.store(addr, sym) state.regs.rax addr def main(): proj angr.Project(./demo, auto_load_libsFalse) proj.hook_symbol(malloc, malloc_hook, length0) state proj.factory.entry_state() sm proj.factory.simulation_manager(state) sm.explore(find0x4006a4, avoid0x4006ad) if sm.found: st sm.found[0] # 解析整个堆区域的具体解 heap_bytes st.solver.eval(claripy.BVS(heap_0, 8 * 6), cast_tobytes) print(Found, heap bytes:, heap_bytes) else: print(No found) for i, st in enumerate(sm.active[:5]): print(factive[{i}] satisfiable:, st.solver.satisfiable()) if __name__ __main__: main()说几个容易踩的坑。第一fake_heap_base一定要选一个 angr 不会主动使用的地址。前面我用 0x600000对大多数小型二进制没问题但如果你程序本身加载地址就在这个范围就要避开。可以用state.memory._get_region或者干脆打印state.regs.rsp、加载基地址后估算。第二malloc_size建议取你实际需要大小的两倍以上留余量。第三hook_symbol的length参数如果不传angr 默认会以符号对应的函数长度做替换容易出问题hook 我们自己的纯 Python 函数时length0更安全。第四如果你的二进制是静态链接的可能没有malloc动态符号hookmalloc会失败。处理方式是 hook 地址先通过proj.loader.main_object.get_symbol(malloc)拿到地址或者直接对proj.loader的 memory 地图找到 malloc 所在的 PLT 入口用proj.hook(addr, hook_func)。4.5 设计点详解为什么这里要“同时符号化整个 size 块”很多人在成功跑出一次结果后会有个疑问为什么我要符号化整个 0x100 字节而不是只在 hook 到的 malloc size这里是 0x20对应的空间上做符号化这有两个层面的原因。一方面符号化整个保留区域的成本并不高。angr 的 BVS 在约束求解时只对实际参与比较的字节产生约束那些没有被读取的字节不会影响求解复杂度。你把整个区域标成符号相当于为后续可能发生的越界读取或者各种偏移访问留了后路。另一方面真实程序里malloc 后面往往还跟着realloc、memcpy、strlen等各种操作你无法预测程序会读取哪一段偏移。动态规划一步到位后续就不用反复回头看。如果担心状态爆炸可以只符号化实际参与校验的那几个字节。这需要你先摸清程序逻辑指向性更强。操作方式是一样的把 BVS 长度设成目标字节数store 到对应偏移即可。自由度在你自己手上。5. 实操过程与核心环节实现从一个更真实的例子看符号化代码设计5.1 新案例程序接收字符串后存堆、校验且带循环上面 Demo 非常简单主要是验证思路。现在换一个稍微真实一点的例子。假设程序从 argv[1] 接收字符串长度限制 0x20把它拷贝到 malloc 分配的缓冲区里随后在一个循环中逐字节累加异或校验最后比较结果。直接对 argv 符号化很简单但问题来了程序把 argv 字符串拷贝到 malloc 区域后如果 angr 正确识别了 memcpy该区域的值仍是符号变量。关键难点在于循环结构的处理。循环在符号执行里容易造成路径爆炸但如果校验逻辑是“无分支”的循环比如只是累加、异或而不根据内存内容跳转angr 的执行路径不会分叉只是状态会包含大量循环变量。不要被“循环”两个字吓到angr 并不是盲人骑瞎马它会管理路径的。对无分支循环执行次数就算成百上千次也完全没问题。真正麻烦的是循环内依赖内容的条件跳转。这种情况下malloc 地址单元符号化能帮你把循环条件变成符号约束而不是把条件里出现的每个具体值都固定死。比如程序里有if (buf[i] a)这样的判断angr 在 i 未知时会尝试所有可能。如果你提前把整个 malloc 区域符号化了angr 就能正确处理这种分支探索所有可能字符值。实战里对这类循环条件一个非常有效的技巧是“约束内生符号化”你在 hook 的 malloc 里不光 store BVS还可以主动 store 几个额外的约束。比如你知道校验一定要求某个字节是字母就可以直接加state.solver.add(buf[i] A)减少无用分支。这类约束越早加状态精简越明显。5.2 结合“查找目标地址”与“避免地址”的工程化脚本实战中你一旦开始符号化 malloc就不能只关注找目标那一支。很多程序校验失败的分支会调用 exit 或者 abort这些地址如果不写进avoidangr 会为了探索它们消耗大量资源。我给一个稍微工程化的脚本框架def run_analysis(proj, start_addrNone, find_addrs[], avoid_addrs[]): if start_addr is None: state proj.factory.entry_state() else: state proj.factory.blank_state(addrstart_addr) # 初始化符号化堆 fake_heap_base 0x200000 sym_size 0x200 state.memory.store(fake_heap_base, claripy.BVS(heap_symbolic, 8 * sym_size)) # 探索 sm proj.factory.simulation_manager(state) sm.use_technique(angr.exploration_techniques.DFS()) # 深度优先找路径失败后快速回溯 sm.explore(findfind_addrs, avoidavoid_addrs) if sm.found: for st in sm.found: # 按需提取 return st return None这个框架把 malloc 符号化的动作和执行解耦了你可以在任意起点状态调用。注意我用的是DFS而不是默认的BFS。找 target 时深度优先往往更快但如果你希望覆盖更全面的路径BFS 更稳。实际场景中我会根据程序复杂度切换小而精的程序用 DFS大而杂的程序用 BFS。另外blank_state配合start_addr是处理复杂反调试、自修改代码的好姿势。你可以先手动分析程序逻辑直接跳到某个关键函数入口把上下文寄存器、栈设置好后再符号化堆区开始探索。5.3 参数计算符号化范围与约束条件怎么写更经济这个点我觉得很有必要详细展开因为很多脚本卡死不是符号化太少而是符号化太多、约束太宽造成的。假设程序有 10 个 malloc 调用点每个分配 0x100 字节。如果你统一 hook对每个 malloc 区域都写入一整块全新的 BVS那 angr 需要同时跟踪的可能符号变量就是 10 × 0x100 × 8 字节 12800 个 bit。约束求解器面对这些符号光维护可达性关系就可能内存爆炸。所以我给自己定了三条规矩只符号化必要地址。如果程序只校验 malloc 区域的前 16 字节那 BVS 长度就设成 16 字节甚至更小别贪多。同一时间只让少数几个 malloc 区域“活着”。一个技巧是判断 malloc 的调用点只有当它是关键位置比如某个函数里的 malloc才写入符号其他 malloc 返回具体地址内容不管。尽早加约束。如果你从逆向分析或动态调试已经知道输入字节属于可打印字符那就提前 add 约束不要等求解器自己去探索 256 种可能。用生活例子来说你让一个快递员送包裹给某个神秘收件人只给了他“地址在某某小区”这个信息他要跑遍整个小区你得让他跑多久但如果你提前说“收件人姓王”他直接去查门牌系统效率完全不一样。符号执行里的约束约等于这个“提前信息”。判断调用点的姿势在 hook 函数里用state.inspect的 call 事件拿到调用返回地址。注意 hook 时length0会完全替换函数你可能拿不到原始调用参数更好的办法是用state.inspect在函数入口处监听寄存器参数def malloc_hook(state): size_arg state.regs.rdi # System V 下第一个参数在 rdi # 你要分析的那个关键 malloc 很可能 size 是一个特定常量或范围 if state.solver.eval(size_arg) 0x100: # 粗略筛一下 addr fake_heap_base sym claripy.BVS(key_heap, 8 * state.solver.eval(size_arg)) state.memory.store(addr, sym) state.regs.rax addr else: state.regs.rax fake_heap_base 0x1000 # 其他 malloc 返回另一个地址不过要注意state.solver.eval(size_arg)如果你不去约束它它可能返回任意值。这个例子只是演示思路真正使用时建议先约束size_arg或者直接用state.solver.min、max判断范围。更稳妥的做法是不依赖 size直接在调用点返回地址上做判断这需要你从反汇编结果里查到 malloc 的调用方地址。5.4 现场问题一符号化之后求解结果不对如何定位按上面的脚本执行你可能成功 found 了但拿到的字节串塞回程序却不对。这种问题一般有三个来源。第一个来源是约束没加全。有些校验逻辑不只有一层比较可能是算术运算后再比较或者有可能通过查表实现。如果你的约束只覆盖了表层判断求解器给出的解可能只满足表层条件内层条件被绕过了。这时候需要结合反汇编确认整个校验链有多少步。第二个来源是符号化地址选错了。你符号化的是 malloc 返回的地址但程序后面可能把数据拷贝到了另一块地址或者 malloc 返回的地址被某个指针变量改动过。用 angr 的state.memory.load检查那个地址的内容就能发现是不是符号变量。很多次我发现符号变量在但程序读取的来源却是一个别的地方因为程序里有个中间变量保存了 malloc 结果后来又改了这个变量。第三个来源是内存模型默认的字节序问题。x86 用的是小端序当你把整个 8 字节的 BVS store 到地址上后续如果程序按字节读取没问题但如果程序把这块区域当成一个 uint64 来比较小端序会把 BVS 的低字节放在低地址与常规直觉相反。解决方式是统一用endnessstate.arch.memory_endness或者显式使用state.memory.store(addr, sym, endnessIend_BE)具体按你程序里的读取方式调整。5.5 现场问题二符号化后路径爆炸卡在循环出不来另一个高频问题是符号化成功后 angr 确实“活”了但它非常兴奋把每条路径都探索了个遍尤其是程序中存在循环结构时几秒钟就爆出几百万状态。这种情况下不要慌第一步先看是不是循环条件依赖了符号内容。比如for (i 0; buf[i] ! 0; i)一旦 buf 被符号化这个循环条件就变成了一个探索点buf[i] 是否等于 0angr 会同时探索“等于 0”和“不等于 0”的分支然后继续执行更深层的逻辑。对策有三个方向。第一手动约束 buf[i] 的取值范围比如可打印字符减少穷举空间。第二限制路径深度或使用veritesting技术它能把部分循环条件合并。angr 的Veritestingexploration technique 是对付这类情况的常用工具虽然原理复杂但调用很简单sm proj.factory.simulation_manager(state) sm.use_technique(angr.exploration_techniques.Veritesting()) sm.explore(find..., avoid...)第三直接对循环结构下手用angr的SimProcedure替换循环函数。如果你的循环可以抽象成一个简单的数学函数直接 hook 循环入口计算完结果后放在指定内存里能大幅加快分析。不过这需要你对目标代码结构有足够理解属于高级玩法。我自己实战中70% 的情况用约束DFS 能解决20% 情况用 veritesting 解决剩下 10% 只能换思路放弃完全符号化改用“混合符号执行”把部分已知的具体值喷到堆区只符号化真正未知的部分。6. 常见问题排查与避坑指南6.1 现象对照看到这些情况优先怀疑 malloc 符号化问题现象可能原因排查动作sm.active全是 unsat没有 found符号化范围没覆盖关键内存或约束过强打印活跃状态约束检查是否包含 address 对应的内存内容explore 卡死内存暴涨符号化范围过大循环条件生成海量状态收缩符号化大小添加取值范围约束found 了但塞回程序不对约束缺失或符号化地址/字节序问题反汇编比较链逐步验证malloc 返回值不对hook 方式错误或 Return address 被覆盖用state.inspect监听返回值同步检查寄存器符号化后无法执行到malloc后续可能 malloc 内部还有分支或间接跳转检查 hook 是否完全替换了原实现length0确认这个表既是我自己排查的索引也是写给后面看笔记的自己的速查卡。不少问题看起来五花八门根源指向同一个方向符号变量的位置、范围、约束与真实程序逻辑不对齐。6.2 遇到 unsat 时如何拆解不少同学看到unsat就以为 angr 坏了。这里有个很重要的调试方法把活跃状态的约束打印出来逐个检查。for i, st in enumerate(sm.active[:5]): print(State, i, satisfiable:, st.solver.satisfiable()) if not st.solver.satisfiable(): for idx, c in enumerate(st.solver.constraints): print( Constraint, idx, :, c)逐个看约束列表你会发现很多 unsat 是因为你手动 add 了范围约束比如buf[0] A和buf[0] Z但程序本身的比较条件要求buf[0] -这就产生矛盾。如果是这种情况说明你的全局约束跟程序固有逻辑冲突要放宽手动约束。另一个常见原因是符号区域里有多个不同 BVS程序把它们做了乘法或除法操作导致某些非线性的算术关系不可满足。z3 对非线性算术乘法、除法的支持并不好遇到就可能直接抛出 unsat 或返回 unknown。这种情况的解法是尽量在源头把符号变量拆分避免一次符号化一整块后让程序做整体乘法校验。6.3 hook malloc 时被递归调用或被静态链接坑hook 符号碰到“递归”问题的时候不多但碰到一次就很折磨。如果你的 hook 函数内部又调用了state.memory.store而某个后续指令再次调用 malloc你没有在 hook 里做区分处理就会导致内存被反复覆盖。比如程序在一个循环里 malloc 三次每次 malloc 都返回同一个 fake_heap_base那第二次 malloc 会把第一次符号化区域冲掉。解决方法是维护一个分配计数每次 store 一个不同地址。静态链接的情况下hook_symbol(malloc)往往静默失效。我排查这类问题时就用proj.loader.main_object.symbols看有没有 malloc 符号。没有就改用 hook 地址方式从 IDA 或 Ghidra 里找到 malloc 函数的起始地址通常在 .text 段里直接proj.hook(addr, my_malloc_hook)。要注意地址在 PIE 开启时是相对偏移angr 内部处理加载基址时会换算你只要确认地址与 IDA 里显示的静态地址一致就行。6.4 关于 angr 版本差异的提醒我一直强调这一点因为不同版本的 angr API 变化太大。老版本 7.x 和现在 9.x/10.x在sim_manager、hook_symbol、BVS的位置上都有改动。我笔记里的代码基于 9.2如果你用的是其他版本跑不通时先看 API 变化其次才怀疑分析思路。尤其是 10.x 中SimState的插件体系和state.memory.store的默认参数有调整BVS 包导入也从claripy.BVS迁移到state.solver.BVS这类方式。版本变了但“malloc 地址单元符号化”的思想不变确定地址、写入符号、约束求解。7. 一点个人经验收尾我在这篇笔记里写的方法说白了就是一套“给 angr 补内存上下文”的思路。malloc 地址单元符号化只是这套思路里最常见的一种落地形式。实际分析中很多东西都能人为符号化栈上的未初始化变量、文件读入的缓冲区、甚至全局对象内部的某个字段。你只要记住一个原则凡是你希望求解器能“推算”出来的值就必须让它成为一个符号变量并且最好提前加上已知约束。这样想后面遇到各种奇奇怪怪的程序思路就不会乱。最后给一个新手的实用建议如果你刚开始学 angr不要一上来就研究各种高深技巧。先把我这篇笔记里的 Demo 完整跑通然后试着改几个参数比如改 malloc 返回地址、改符号化大小、加一个取值范围约束看求解结果怎么变。等你亲手撞过一次 unsat、亲手把约束从矛盾里解放出来你对符号执行的直觉会上一个台阶。这个领域没有捷径但每一次“哇原来是这里”的瞬间都会让你离真正的约定求解玩家更近一步。 malloc地址单元符号化：angr符号执行的关键技巧
1. 问题起源为什么单独把“malloc地址单元符号化”拎出来讲写这一篇纯属被坑出来的。前面几篇笔记里我一直在处理“标准输入符号化”“argv符号化”这类常规操作当时觉得 angr 已经很顺手了直到遇到一个程序逻辑看起来非常简单就是读入一段数据经过一个校验函数对了就打印 flag。结果 angr 跑下来路径倒是探索了一堆但求解器死活给不出一个合法的输入。最后排查了半天问题就出在 malloc 分配的地址内容没有被符号化上。这里先解释一下背景。符号执行的本质是把输入变成符号变量让程序带着符号跑碰到分支就把条件收集起来最后交给约束求解器去解。但这里的“输入”是有范围的你符号化的是 stdin、argv 还是某个全局缓冲区angr 只会把明确标成 BVSBitVectorSymbolic的那部分内存当成“可变”的其余内存内容 angr 会按具体值处理。malloc 出来的堆区怎么处理就很微妙了。它不像栈上声明的数组有明确的地址和大小malloc 返回的地址在符号执行里是动态生成的angr 默认不知道你这个地址指向的内存区域代表什么含义更不会主动给这块内存灌入符号变量。结果就是程序从堆区读数据、做比较angr 真以为堆里那些字节是“固定值”于是产生了大量不可能满足的条件分支。这也就引出了本篇笔记要讲的方案如何让 malloc 分配出来的那块地址空间其内容也成为符号变量从而让符号执行真正覆盖到程序的核心校验逻辑。这篇笔记适合两类人看。一类是刚接触 angr、只跑通过几道入门题准备挑战真实程序的人malloc 符号化是绕不过去的一关。另一类是已经会用 angr 但经常遇到“求解无解”“分支全走死”这类问题、排查无头绪的人。本篇会从原理讲到实操最后给出排查技巧核心是一个可复现的 Demo万金油思路。2. 能力铺垫angr 符号执行里“内存状态”的本质2.1 从符号变量到约束求解angr 到底在做什么angr 跑一个程序时维护的是一个“符号状态”。这个状态可以理解成一张大表记录了当前执行到的指令地址、寄存器的值、内存中每个地址的内容。这些“值”有两种形态一种是确定的具体数值比如0x401000另一种是符号变量比如一个 32 位的BVS(input_0, 32)它不是一个固定值而是一个“待定值”。angr 在模拟执行过程中遇到分支指令比如cmp; jz时会同时探索两个方向每条路径上都会记录一个路径条件。比如某条路径可能记录了input_0 0x41另一条路径可能记录了input_0 0x41。到最后你想让某一条路径走到 “success” 分支就把这条路径上所有的路径条件收集出来连同你自己手动添加的其他约束一起交给底层求解器z3去解。z3 会返回一个具体的数值使得这些条件全部成立。这个数值就是让程序走进目标分支的输入。这个模型看似简单但注意一个关键点约束求解器只能基于符号变量去求解。如果一个值不是符号变量而是一个具体常量那 angr 是不可能“反过来算”出一个输入去改变它的。说得夸张一点如果你压根没把一个内存位置标记成符号那 angr 眼里它就永远是某个固定值哪怕程序逻辑上它初始依赖 stdin。所以 malloc 地址单元符号化本质上就是在回答一个问题堆上这块内存的“值”能不能随输入变化如果能angr 才有机会通过路径条件反推出输入如果不能那 angr 就只能看见一个死板的具体值路径探索也戛然而止。2.2 malloc 在符号执行里是“黑盒”问题就出在这真实程序里 malloc 可不是拿来看的。常见模式是程序从标准输入读固定字节数存到 malloc 得到的缓冲区里然后对这个缓冲区做字节变换、查表、比较。比如下面这类简化逻辑char *buf malloc(10); read(0, buf, 10); if (buf[0] f buf[1] l buf[2] a buf[3] g) { puts(correct); }如果是在真实系统上跑read会从 stdin 往 buf 指向的地址填充数据。但在 angr 里问题出现了angr 默认的read系统调用如果遇到未知的文件描述符通常是提前处理后返回确定值或触发异常具体行为取决于 angr 对read的模拟方式。即使你通过SimFile或者 hook 方式把 stdin 提供了也存在一个更深层的坑angr 的read模拟是写在系统调用层面的它的“目标地址”是 malloc 返回的那个地址。而 malloc 在 angr 的 SimHeap 里大多被 hook 成返回某个地址但这个地址指向的内存并没有被初始化为符号。于是你在状态里做了state.solver.BVS(stdin, 10*8)以为万事大吉实际上 angr 执行read时确实把符号变量“拷贝”到了 malloc 地址上但前提是你正确配置了 stdin 的文件描述符并且 angr 把这次 read 识别为读符号数据。如果程序不是走read而是先从 stdin 读到一个临时栈缓冲再手动memcpy到堆区那 angr 在 memcpy 时是逐字节复制符号变量的这种情况反而没事。真正出问题的场景是程序校验逻辑直接作用在 malloc 内容上但 malloc 的内容来源不是 angr 认识的符号通道而是来自程序内部的某种初始化逻辑。举个典型例子程序从 stdin 读入一串十六进制字符串strtol转换成整数再当作种子去初始化一个伪随机序列最后用这个序列去校验堆区的某个数据。strtol、srand、rand这些函数在 angr 里的模拟如果不做额外处理会产生具体数值所以堆区数据就不可能被符号化。这种情况下你必须跳过“生成链条”直接在 malloc 地址单元上做符号化——人为声明“这块内存的内容是符号变量”。2.3 为什么“符号化地址”不等于“符号化内容”这里有必要区分两个概念。一个是把 malloc 返回的指针值符号化一个是把 malloc 指向的内存内容符号化。很多入门教程讲“malloc 符号化”时说的是前者让 malloc 的返回值成为一个符号变量这样能让程序走不同的堆分配分支比如检查 malloc 是否失败。字符串比较常见的一个坑是在分析带堆喷的程序时需要让 malloc 返回不同的地址来探索堆布局分支。但本文讨论的“malloc 地址单元符号化”指的是后者malloc 返回的地址是确定的或可计算的但该地址上的内存单元内容是符号化的。打个比方你和朋友约好在一家餐厅见面地址是固定的但你不知道朋友在那家餐厅坐哪一桌内容你想通过一定规则反推出来。符号化内容就是给“坐哪一桌”这个变量建立数学模型让求解器去算。两者在 angr 里的具体操作位置也不同符号化返回值需要 hook malloc 本身符号化地址内容需要在 malloc 之后拿到地址再用 store 操作往这个地址写入 BVS。理解了这一点后面看别人代码就不容易晕。3. 方案选型四种“让 malloc 区域符号化”的方式对比3.1 方式一hook malloc拿到返回值后再 store BVS最直接的做法通过project.hook_symbol(malloc, hook_func)劫持 malloc 符号在 hook 函数里先返回一块地址通常用state.heap相关接口或直接返回一个固定地址然后立刻在这个地址上 store 一个 BVS。这样程序后续对这块地址的读取就读到了符号变量。import angr import claripy def malloc_hook(state): # 手动指定一块地址避开已有内存区域 addr 0x5000000 # 只是一个示例地址实际要选堆区 size 0x40 # 让 malloc 返回这个地址 state.regs.rax addr # 在这块区域写入 64 字节的符号值 sym claripy.BVS(heap_data, 8 * size) state.memory.store(addr, sym)这种方式的好处是直观你能控制全流程。坏处也很明显一个程序里不止一处调用 malloc如果你全都 hook 到一个统一处理所有 malloc 区域内容都一样同一个 BVS逻辑就乱了。所以这种方式更适合目标明确、malloc 调用点不多的情况一般实验里也就一两个关键 malloc。3.2 方式二在输入符号化阶段同步填充堆区域不少初学者看到“malloc 地址单元符号化”第一反应是我先不碰 malloc直接把符号变量写到那个地址不就行了比如你知道 malloc 返回地址的规律像 glibc 的 fastbin 在固定偏移就硬编码一个地址在initial_state里storeBVS。这种方式在很多 CTF 题目里很有效因为题目程序简单甚至不校验 malloc 的返回值。不过这种方式有个前提你必须知道 malloc 返回地址到底是多少。angr 里 malloc 的默认 implementation 通常返回一块固定的模拟堆地址每次运行基本一致。但不同版本的 angrSimHeap 的地址策略不一样你硬编码的地址可能会踩到 angr 给栈或全局区域预留的空间。稳妥起见可以在 setup 阶段 hook 住 malloc打印返回地址再决定往哪填充。3.3 方式三利用 angr 的 SimHeap 自定义分配器这是“正统”做法。angr 内部有SimHeap类体系比如SimHeapBrk、SimHeapLibc。通过自定义一个继承SimHeap的分配器重写_allocate方法在分配时自动记录所有 malloc 返回的地址并在返回前将地址写入符号变量。这样程序里所有 malloc 出来的区域内容都是“全新符号”每个 malloc 对应一个独立 BVS互不干扰。class SymHeap(angr.state_plugins.heap.SimHeapLibc): def _allocate(self, size, **kwargs): addr super()._allocate(size, **kwargs) sym claripy.BVS(fheap_{addr:x}, 8 * size) self.state.memory.store(addr, sym) return addr # 使用时 state.heap SymHeap()这种方式约束力最强但复杂度也高。还有坑过度的自动符号化会让路径条件爆炸。每个 malloc 区域都有一整块 BVS一旦程序对这块区域做逐字节比较angr 会为每个字节引入分叉状态数呈指数级增长。所以这种方式适合研究目的不适合直接对真实大型程序用。3.4 方式四高阶玩法——用 concretization 和约束定向符号化前面几种叫“宽泛符号化”还有更精细的定向符号化不让整个 malloc 区域一开始就是 BVS而是让它先保持具体值等 angr 执行到某个比较指令时发现该分支不可满足再“回头”把相关内存地址符号化。angr 确实存在某种程度上“从失败中学习”的机制——如果你在探索时设置了save_unconstrained常见的是保存未约束状态而不是自动回填符号。这里说的“回头符号化”通常要你手动根据失败路径的特征在特定地址上补充约束。这种方式我已经一年没在实战中用了因为多数情况下方式一和方式二够用。但了解这个概念有助于理解 angr 的局限符号执行不是魔法它要在“尽可能多地探索”和“避免状态爆炸”之间取舍。手动符号化 malloc 区域本质上就是一种人工引导这种取舍的行为。3.5 选型建议按判定条件选不按喜好选说实话我在自己的实践里没用过一种包打天下的方案。我建议按下面这个标准来选场景特征推荐方式理由程序 malloc 调用点少关键区域只有一处方式一代码短好控制调试直观CTF 题目、程序结构简单且 malloc 地址稳定方式二写起来最快能跑就行想系统分析某类程序需要让所有堆区域都可变方式三自动化程度最高但要防状态爆炸求解出现 unsat 或路径走死需要精确定位方式四实际是排查局部符号化灵活但依赖经验判断本篇下面的实操用方式一做演示因为最能体现“malloc 地址单元符号化”的思路先拿到地址再填充符号。把这一步走通其他方式就是在它的基础上做变通。4. 实操演示从零跑通“malloc 内容符号化”完整流程4.1 准备实验环境与模拟程序首先准备好 angr 环境。我用的版本是 angr 9.2往下的 9.0 和往上的 10.x 在 API 上有细微差别但核心思路一致。安装就是常规的pip install angr需要注意的是 angr 依赖的 z3-solver 版本可能跟系统其他包冲突建议建虚拟环境避免污染系统 Python。然后是模拟程序。本文要分析的 Demo 用 C 语言写成为了简化后面解释原理我刻意写得很“人工”#include stdio.h #include stdlib.h #include string.h int check(char *buf, int len) { if (buf[0] * buf[1] 0x861) { if (buf[2] buf[3] 0xcb) { if (buf[4] ^ buf[5] 0x5c) { return 1; } } } return 0; } int main(int argc, char **argv) { char *heap_buf (char *)malloc(0x20); // 模拟从某处填充数据关键是在符号执行中这块内容没有被正常符号化 memcpy(heap_buf, ABCDEF, 6); if (check(heap_buf, 6)) { puts(ok); } else { puts(bad); } return 0; }编译gcc -o demo demo.c -no-pie -fno-stack-protector。这里关掉 PIE 不是为了别的只是后面分析时地址固定方便说明问题。真实复现时你可以保留 PIEangr 也支持。这个 Demo 里check函数对 heap_buf 的内容做了几组算术校验。如果按常规思路直接跑会看到 angr 走到check之后两个分支都不可满足因为内存里是固定的ABCDEF算不出满足条件的解法。这正是我们要解决的。4.2 常规分析脚本与失败现象记录先写一个最常规的 angr 脚本看看失败长什么样import angr def main(): proj angr.Project(./demo, auto_load_libsFalse) state proj.factory.entry_state() sm proj.factory.simulation_manager(state) sm.explore(find0x4006a4, avoid0x4006ad) # 目标是 ok 分支 if sm.found: print(Found!) print(sm.found[0].posix.dumps(0)) else: print(No found) # 看看活跃状态情况 print(active:, len(sm.active)) for st in sm.active[:3]: print(st.solver.constraints[-3:]) if __name__ __main__: main()跑一下结果大概率是No found。这就说明内存内容确确实实没有被符号化程序执行到比较时就没有合法路径了。只用看路径活跃数会发现所有状态都是 unsatisfiable在sm.active里检查state.solver.satisfiable()会返回 False。这里要专门提醒一下在 angr 里一个状态“活着”不代表它能继续往后执行。很多人在sm.explore没找到结果时就打印sm.active里的状态数发现数量不少就觉得是不是其他 bug。实际上这些 active 状态很可能全是 unsat后续指令执行全是死胡同。所以排查时第一件事就是检查状态的可满足性。4.3 方案落地hook malloc 并符号化返回地址指向的内容现在按方式一改造。先 hookmalloc符号让 malloc 返回一个我们指定的地址并在这个地址上写入 BVS。angr 的hook_symbol接受一个符号名和 hook 函数。hook 函数的输入是state你可以在里面修改寄存器、内存、求解器约束。import angr import claripy def setup_malloc_sym(state): # 选一个地址作为“堆区”注意避开已知区域 fake_heap 0x600000 size 0x20 sym_data claripy.BVS(malloc_0, 8 * size) state.memory.store(fake_heap, sym_data) # malloc 的返回结果放在 rax state.regs.rax fake_heap然后把 hook 挂到符号上。angr 里hook_symbol的第一个参数是字符串对应程序里malloc在动态符号表中的名字。def main(): proj angr.Project(./demo, auto_load_libsFalse) proj.hook_symbol(malloc, setup_malloc_sym, length0) # length 为 0 表示完全替换写完这个 hook 之后重新用同样的 explore 跑就能在found里看到状态了。这时候可以 dump 一下标准输入如果你程序里有读入或者直接查看malloc_0这个符号变量的值found_state sm.found[0] solver found_state.solver solution solver.eval(claripy.BVS(malloc_0, 8 * 6), cast_tobytes) print(solution)如果不出意外你得到的 bytes 就是满足check条件的“目标值”比如bKI\xe5TZ之类。验证方式很简单用这个字节串替换 Demo 里 memcpy 的数据重新编译跑一下发现打印ok。这一步的关键点在于顺序必须先 store BVS 到地址再让 malloc 返回地址。如果反过来先设置 rax 再 storestore 的地址还是我们自己指定的理论上没区别但如果你 store 的地址依赖 rax 的内容那顺序就很重要。另外store 的 size 要跟后面读取的长度匹配只 store 6 字节也行但为了稳妥我会按整个分配大小 store 一整块 BVS后面读取哪一段都能命中。4.4 完整脚本与边界参数说明下面给一个完整的脚本可以直接替换地址、符号名跑别的程序用import angr import claripy fake_heap_base 0x200000 malloc_size 0x100 def malloc_hook(state): # 可以在这里打印调用栈或者分配大小便于调试 # state.inspect 相关用法可以拿到调用参数这里略过 addr fake_heap_base sym claripy.BVS(heap_0, 8 * malloc_size) state.memory.store(addr, sym) state.regs.rax addr def main(): proj angr.Project(./demo, auto_load_libsFalse) proj.hook_symbol(malloc, malloc_hook, length0) state proj.factory.entry_state() sm proj.factory.simulation_manager(state) sm.explore(find0x4006a4, avoid0x4006ad) if sm.found: st sm.found[0] # 解析整个堆区域的具体解 heap_bytes st.solver.eval(claripy.BVS(heap_0, 8 * 6), cast_tobytes) print(Found, heap bytes:, heap_bytes) else: print(No found) for i, st in enumerate(sm.active[:5]): print(factive[{i}] satisfiable:, st.solver.satisfiable()) if __name__ __main__: main()说几个容易踩的坑。第一fake_heap_base一定要选一个 angr 不会主动使用的地址。前面我用 0x600000对大多数小型二进制没问题但如果你程序本身加载地址就在这个范围就要避开。可以用state.memory._get_region或者干脆打印state.regs.rsp、加载基地址后估算。第二malloc_size建议取你实际需要大小的两倍以上留余量。第三hook_symbol的length参数如果不传angr 默认会以符号对应的函数长度做替换容易出问题hook 我们自己的纯 Python 函数时length0更安全。第四如果你的二进制是静态链接的可能没有malloc动态符号hookmalloc会失败。处理方式是 hook 地址先通过proj.loader.main_object.get_symbol(malloc)拿到地址或者直接对proj.loader的 memory 地图找到 malloc 所在的 PLT 入口用proj.hook(addr, hook_func)。4.5 设计点详解为什么这里要“同时符号化整个 size 块”很多人在成功跑出一次结果后会有个疑问为什么我要符号化整个 0x100 字节而不是只在 hook 到的 malloc size这里是 0x20对应的空间上做符号化这有两个层面的原因。一方面符号化整个保留区域的成本并不高。angr 的 BVS 在约束求解时只对实际参与比较的字节产生约束那些没有被读取的字节不会影响求解复杂度。你把整个区域标成符号相当于为后续可能发生的越界读取或者各种偏移访问留了后路。另一方面真实程序里malloc 后面往往还跟着realloc、memcpy、strlen等各种操作你无法预测程序会读取哪一段偏移。动态规划一步到位后续就不用反复回头看。如果担心状态爆炸可以只符号化实际参与校验的那几个字节。这需要你先摸清程序逻辑指向性更强。操作方式是一样的把 BVS 长度设成目标字节数store 到对应偏移即可。自由度在你自己手上。5. 实操过程与核心环节实现从一个更真实的例子看符号化代码设计5.1 新案例程序接收字符串后存堆、校验且带循环上面 Demo 非常简单主要是验证思路。现在换一个稍微真实一点的例子。假设程序从 argv[1] 接收字符串长度限制 0x20把它拷贝到 malloc 分配的缓冲区里随后在一个循环中逐字节累加异或校验最后比较结果。直接对 argv 符号化很简单但问题来了程序把 argv 字符串拷贝到 malloc 区域后如果 angr 正确识别了 memcpy该区域的值仍是符号变量。关键难点在于循环结构的处理。循环在符号执行里容易造成路径爆炸但如果校验逻辑是“无分支”的循环比如只是累加、异或而不根据内存内容跳转angr 的执行路径不会分叉只是状态会包含大量循环变量。不要被“循环”两个字吓到angr 并不是盲人骑瞎马它会管理路径的。对无分支循环执行次数就算成百上千次也完全没问题。真正麻烦的是循环内依赖内容的条件跳转。这种情况下malloc 地址单元符号化能帮你把循环条件变成符号约束而不是把条件里出现的每个具体值都固定死。比如程序里有if (buf[i] a)这样的判断angr 在 i 未知时会尝试所有可能。如果你提前把整个 malloc 区域符号化了angr 就能正确处理这种分支探索所有可能字符值。实战里对这类循环条件一个非常有效的技巧是“约束内生符号化”你在 hook 的 malloc 里不光 store BVS还可以主动 store 几个额外的约束。比如你知道校验一定要求某个字节是字母就可以直接加state.solver.add(buf[i] A)减少无用分支。这类约束越早加状态精简越明显。5.2 结合“查找目标地址”与“避免地址”的工程化脚本实战中你一旦开始符号化 malloc就不能只关注找目标那一支。很多程序校验失败的分支会调用 exit 或者 abort这些地址如果不写进avoidangr 会为了探索它们消耗大量资源。我给一个稍微工程化的脚本框架def run_analysis(proj, start_addrNone, find_addrs[], avoid_addrs[]): if start_addr is None: state proj.factory.entry_state() else: state proj.factory.blank_state(addrstart_addr) # 初始化符号化堆 fake_heap_base 0x200000 sym_size 0x200 state.memory.store(fake_heap_base, claripy.BVS(heap_symbolic, 8 * sym_size)) # 探索 sm proj.factory.simulation_manager(state) sm.use_technique(angr.exploration_techniques.DFS()) # 深度优先找路径失败后快速回溯 sm.explore(findfind_addrs, avoidavoid_addrs) if sm.found: for st in sm.found: # 按需提取 return st return None这个框架把 malloc 符号化的动作和执行解耦了你可以在任意起点状态调用。注意我用的是DFS而不是默认的BFS。找 target 时深度优先往往更快但如果你希望覆盖更全面的路径BFS 更稳。实际场景中我会根据程序复杂度切换小而精的程序用 DFS大而杂的程序用 BFS。另外blank_state配合start_addr是处理复杂反调试、自修改代码的好姿势。你可以先手动分析程序逻辑直接跳到某个关键函数入口把上下文寄存器、栈设置好后再符号化堆区开始探索。5.3 参数计算符号化范围与约束条件怎么写更经济这个点我觉得很有必要详细展开因为很多脚本卡死不是符号化太少而是符号化太多、约束太宽造成的。假设程序有 10 个 malloc 调用点每个分配 0x100 字节。如果你统一 hook对每个 malloc 区域都写入一整块全新的 BVS那 angr 需要同时跟踪的可能符号变量就是 10 × 0x100 × 8 字节 12800 个 bit。约束求解器面对这些符号光维护可达性关系就可能内存爆炸。所以我给自己定了三条规矩只符号化必要地址。如果程序只校验 malloc 区域的前 16 字节那 BVS 长度就设成 16 字节甚至更小别贪多。同一时间只让少数几个 malloc 区域“活着”。一个技巧是判断 malloc 的调用点只有当它是关键位置比如某个函数里的 malloc才写入符号其他 malloc 返回具体地址内容不管。尽早加约束。如果你从逆向分析或动态调试已经知道输入字节属于可打印字符那就提前 add 约束不要等求解器自己去探索 256 种可能。用生活例子来说你让一个快递员送包裹给某个神秘收件人只给了他“地址在某某小区”这个信息他要跑遍整个小区你得让他跑多久但如果你提前说“收件人姓王”他直接去查门牌系统效率完全不一样。符号执行里的约束约等于这个“提前信息”。判断调用点的姿势在 hook 函数里用state.inspect的 call 事件拿到调用返回地址。注意 hook 时length0会完全替换函数你可能拿不到原始调用参数更好的办法是用state.inspect在函数入口处监听寄存器参数def malloc_hook(state): size_arg state.regs.rdi # System V 下第一个参数在 rdi # 你要分析的那个关键 malloc 很可能 size 是一个特定常量或范围 if state.solver.eval(size_arg) 0x100: # 粗略筛一下 addr fake_heap_base sym claripy.BVS(key_heap, 8 * state.solver.eval(size_arg)) state.memory.store(addr, sym) state.regs.rax addr else: state.regs.rax fake_heap_base 0x1000 # 其他 malloc 返回另一个地址不过要注意state.solver.eval(size_arg)如果你不去约束它它可能返回任意值。这个例子只是演示思路真正使用时建议先约束size_arg或者直接用state.solver.min、max判断范围。更稳妥的做法是不依赖 size直接在调用点返回地址上做判断这需要你从反汇编结果里查到 malloc 的调用方地址。5.4 现场问题一符号化之后求解结果不对如何定位按上面的脚本执行你可能成功 found 了但拿到的字节串塞回程序却不对。这种问题一般有三个来源。第一个来源是约束没加全。有些校验逻辑不只有一层比较可能是算术运算后再比较或者有可能通过查表实现。如果你的约束只覆盖了表层判断求解器给出的解可能只满足表层条件内层条件被绕过了。这时候需要结合反汇编确认整个校验链有多少步。第二个来源是符号化地址选错了。你符号化的是 malloc 返回的地址但程序后面可能把数据拷贝到了另一块地址或者 malloc 返回的地址被某个指针变量改动过。用 angr 的state.memory.load检查那个地址的内容就能发现是不是符号变量。很多次我发现符号变量在但程序读取的来源却是一个别的地方因为程序里有个中间变量保存了 malloc 结果后来又改了这个变量。第三个来源是内存模型默认的字节序问题。x86 用的是小端序当你把整个 8 字节的 BVS store 到地址上后续如果程序按字节读取没问题但如果程序把这块区域当成一个 uint64 来比较小端序会把 BVS 的低字节放在低地址与常规直觉相反。解决方式是统一用endnessstate.arch.memory_endness或者显式使用state.memory.store(addr, sym, endnessIend_BE)具体按你程序里的读取方式调整。5.5 现场问题二符号化后路径爆炸卡在循环出不来另一个高频问题是符号化成功后 angr 确实“活”了但它非常兴奋把每条路径都探索了个遍尤其是程序中存在循环结构时几秒钟就爆出几百万状态。这种情况下不要慌第一步先看是不是循环条件依赖了符号内容。比如for (i 0; buf[i] ! 0; i)一旦 buf 被符号化这个循环条件就变成了一个探索点buf[i] 是否等于 0angr 会同时探索“等于 0”和“不等于 0”的分支然后继续执行更深层的逻辑。对策有三个方向。第一手动约束 buf[i] 的取值范围比如可打印字符减少穷举空间。第二限制路径深度或使用veritesting技术它能把部分循环条件合并。angr 的Veritestingexploration technique 是对付这类情况的常用工具虽然原理复杂但调用很简单sm proj.factory.simulation_manager(state) sm.use_technique(angr.exploration_techniques.Veritesting()) sm.explore(find..., avoid...)第三直接对循环结构下手用angr的SimProcedure替换循环函数。如果你的循环可以抽象成一个简单的数学函数直接 hook 循环入口计算完结果后放在指定内存里能大幅加快分析。不过这需要你对目标代码结构有足够理解属于高级玩法。我自己实战中70% 的情况用约束DFS 能解决20% 情况用 veritesting 解决剩下 10% 只能换思路放弃完全符号化改用“混合符号执行”把部分已知的具体值喷到堆区只符号化真正未知的部分。6. 常见问题排查与避坑指南6.1 现象对照看到这些情况优先怀疑 malloc 符号化问题现象可能原因排查动作sm.active全是 unsat没有 found符号化范围没覆盖关键内存或约束过强打印活跃状态约束检查是否包含 address 对应的内存内容explore 卡死内存暴涨符号化范围过大循环条件生成海量状态收缩符号化大小添加取值范围约束found 了但塞回程序不对约束缺失或符号化地址/字节序问题反汇编比较链逐步验证malloc 返回值不对hook 方式错误或 Return address 被覆盖用state.inspect监听返回值同步检查寄存器符号化后无法执行到malloc后续可能 malloc 内部还有分支或间接跳转检查 hook 是否完全替换了原实现length0确认这个表既是我自己排查的索引也是写给后面看笔记的自己的速查卡。不少问题看起来五花八门根源指向同一个方向符号变量的位置、范围、约束与真实程序逻辑不对齐。6.2 遇到 unsat 时如何拆解不少同学看到unsat就以为 angr 坏了。这里有个很重要的调试方法把活跃状态的约束打印出来逐个检查。for i, st in enumerate(sm.active[:5]): print(State, i, satisfiable:, st.solver.satisfiable()) if not st.solver.satisfiable(): for idx, c in enumerate(st.solver.constraints): print( Constraint, idx, :, c)逐个看约束列表你会发现很多 unsat 是因为你手动 add 了范围约束比如buf[0] A和buf[0] Z但程序本身的比较条件要求buf[0] -这就产生矛盾。如果是这种情况说明你的全局约束跟程序固有逻辑冲突要放宽手动约束。另一个常见原因是符号区域里有多个不同 BVS程序把它们做了乘法或除法操作导致某些非线性的算术关系不可满足。z3 对非线性算术乘法、除法的支持并不好遇到就可能直接抛出 unsat 或返回 unknown。这种情况的解法是尽量在源头把符号变量拆分避免一次符号化一整块后让程序做整体乘法校验。6.3 hook malloc 时被递归调用或被静态链接坑hook 符号碰到“递归”问题的时候不多但碰到一次就很折磨。如果你的 hook 函数内部又调用了state.memory.store而某个后续指令再次调用 malloc你没有在 hook 里做区分处理就会导致内存被反复覆盖。比如程序在一个循环里 malloc 三次每次 malloc 都返回同一个 fake_heap_base那第二次 malloc 会把第一次符号化区域冲掉。解决方法是维护一个分配计数每次 store 一个不同地址。静态链接的情况下hook_symbol(malloc)往往静默失效。我排查这类问题时就用proj.loader.main_object.symbols看有没有 malloc 符号。没有就改用 hook 地址方式从 IDA 或 Ghidra 里找到 malloc 函数的起始地址通常在 .text 段里直接proj.hook(addr, my_malloc_hook)。要注意地址在 PIE 开启时是相对偏移angr 内部处理加载基址时会换算你只要确认地址与 IDA 里显示的静态地址一致就行。6.4 关于 angr 版本差异的提醒我一直强调这一点因为不同版本的 angr API 变化太大。老版本 7.x 和现在 9.x/10.x在sim_manager、hook_symbol、BVS的位置上都有改动。我笔记里的代码基于 9.2如果你用的是其他版本跑不通时先看 API 变化其次才怀疑分析思路。尤其是 10.x 中SimState的插件体系和state.memory.store的默认参数有调整BVS 包导入也从claripy.BVS迁移到state.solver.BVS这类方式。版本变了但“malloc 地址单元符号化”的思想不变确定地址、写入符号、约束求解。7. 一点个人经验收尾我在这篇笔记里写的方法说白了就是一套“给 angr 补内存上下文”的思路。malloc 地址单元符号化只是这套思路里最常见的一种落地形式。实际分析中很多东西都能人为符号化栈上的未初始化变量、文件读入的缓冲区、甚至全局对象内部的某个字段。你只要记住一个原则凡是你希望求解器能“推算”出来的值就必须让它成为一个符号变量并且最好提前加上已知约束。这样想后面遇到各种奇奇怪怪的程序思路就不会乱。最后给一个新手的实用建议如果你刚开始学 angr不要一上来就研究各种高深技巧。先把我这篇笔记里的 Demo 完整跑通然后试着改几个参数比如改 malloc 返回地址、改符号化大小、加一个取值范围约束看求解结果怎么变。等你亲手撞过一次 unsat、亲手把约束从矛盾里解放出来你对符号执行的直觉会上一个台阶。这个领域没有捷径但每一次“哇原来是这里”的瞬间都会让你离真正的约定求解玩家更近一步。