课程导论与前置知识：符号执行是什么？为什么能破解密码学校验？
大家好，欢迎来到这门课。
先说说我自己的经历。几年前我接手过一个固件逆向任务，对方用了白盒AES做校验。我盯着反汇编代码看了三天，手动模拟了十几条路径，结果发现还有上百条分支没覆盖到。那时候我就想，一定有更聪明的办法。后来我接触了符号执行，嗯，这玩意儿确实改变了我的工作方式。
符号执行是什么？
说白了，符号执行就是一种程序分析技术。它不关心具体的数值，而是用符号代替变量。你想想看，传统调试是给程序喂具体输入，然后看它怎么走。符号执行不一样，它把所有可能的输入都当成未知数，然后推导出程序会走哪些路径。
举个例子：
if (input > 10) {
// 路径A
} else {
// 路径B
}传统执行需要你给input一个具体值，比如5或者20。符号执行呢？它把input当成符号变量x，然后自动生成两个约束条件：x > 10 和 x ≤ 10。每条路径对应一组约束，求解器就能算出满足条件的输入值。
核心思想：用符号代替具体值，用约束求解代替手动调试。
为什么能破解密码学校验？
密码学校验，尤其是嵌入式设备里的校验，通常长这样：
- 读入用户输入（密码、序列号、许可证）
- 经过一系列加密、哈希、比较操作
- 输出成功或失败
传统逆向怎么做？你得找到比较指令，然后暴力枚举或者手动分析。但密码算法往往有大量分支和循环，手动分析非常痛苦。
符号执行的优势就在这里：
- 自动探索路径——它能把所有可能的校验路径都走一遍
- 约束求解——走到成功路径后，求解器直接给出满足条件的输入值
- 绕过混淆——很多混淆技术对符号执行无效，因为它不关心代码长得什么样，只关心语义
我在项目中遇到过一种情况：目标固件用了花指令和虚假控制流，IDA里看代码逻辑一团乱麻。但符号执行直接跳过了这些干扰，因为它只跟踪符号变量相关的指令。那些没用的垃圾代码，根本不会影响约束条件。
个人经验：遇到反调试、反逆向的代码，别慌。符号执行很多时候能直接绕过去，因为它是在模拟器里跑的，不是真的在CPU上执行。
环境搭建
工欲善其事，必先利其器。我们需要的三件套：Angr、Z3、IDA Pro。
1. Angr
Angr是一个基于Python的符号执行框架。它把二进制文件加载到模拟器中，然后自动分析。我个人习惯用Python 3.8以上版本，兼容性最好。
安装命令：
pip install angr如果遇到依赖问题，建议用虚拟环境：
python -m venv angr_env
source angr_env/bin/activate # Linux/Mac
angr_env\Scripts\activate # Windows
pip install angr注意：Angr的依赖比较多，尤其是z3-solver。我曾经在Windows上折腾了半天，最后发现用WSL2最省心。如果你用Windows，强烈建议装个WSL2的Ubuntu。
2. Z3
Z3是微软出品的约束求解器。Angr内部集成了Z3，但有时候你需要单独用它做符号计算。
安装：
pip install z3-solver简单测试：
from z3 import *
x = Int('x')
solve(x > 5, x < 10)
# 输出：[x = 6]你看，Z3直接给出了一个可行解。这就是符号执行的核心引擎。
3. IDA Pro
IDA Pro用来做静态分析。我们先用IDA看明白程序的大致结构，找到关键函数地址，然后把这些地址喂给Angr做符号执行。
我个人推荐IDA 7.5以上版本，配合Python 3插件。如果你没有正版，可以用Ghidra替代，但Angr对IDA导出的地址格式支持更好。
知识体系总览
下面这张图概括了本章的核心逻辑：
环境验证
装好之后，跑个简单脚本验证一下：
import angr
import claripy
# 创建一个简单的二进制分析项目
proj = angr.Project('/bin/true')
print("加载成功，架构:", proj.arch.name)
# 创建一个符号变量
flag = claripy.BVS('flag', 8 * 32)
print("符号变量创建成功")如果没报错，恭喜你，环境搭好了。
避坑指南：我曾经在Mac上装Angr，结果因为LLVM版本冲突折腾了两天。后来发现用Docker最省事：docker pull angr/angr。如果你不想折腾环境，直接用Docker镜像，开箱即用。
小结
这一章我们讲了符号执行的基本概念，为什么它能破解密码学校验，以及怎么搭建环境。说白了，符号执行就是把逆向分析从「手动猜谜」变成了「自动求解」。你只需要告诉工具「我要走到成功路径」，剩下的交给约束求解器。
下一章我们会真正动手，用Angr分析一个简单的密码校验程序。到时候你会发现，原来破解密码可以这么简单。
公众号:蓝海资料掘金营，微信deep3321