概述

符号执行 （Symbolic Execution）是一种程序分析技术。其可以通过分析程序来得到让特定代码区域执行的输入。使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。

动态符号执行

将符号执行和动态二进制插桩结合起来可以取长补短,提高样本分析的效果。

1. 用动态插桩收集路径约束: 首先，使用动态二进制插桩来执行样本，收集执行路径上的路径约束。插桩工具可以记录每个条件分支的执行情况，生成相应的符号约束。这一步可以快速获取样本在实际执行中的路径信息。

2. 用符号执行生成新的测试输入: 然后，使用符号执行来分析收集到的路径约束。符号执行器可以对路径约束进行求解，生成能够触发新路径的测试输入。这些输入可以用于后续的动态分析，以扩大代码覆盖率，触发更多的行为。

3. 重复执行和分析: 使用新生成的测试输入再次执行样本，同时进行动态插桩和符号执行。插桩工具可以在新的路径上收集约束，而符号执行器则可以探索新路径。通过重复这一过程，可以不断扩展分析范围，直到达到所需的覆盖率或者触发感兴趣的行为。

4. 联合分析数据流: 在符号执行的过程中,可以利用动态插桩获取的具体执行信息来优化符号分析。例如,可以使用插桩得到的内存访问信息来优化符号内存模型,或者用实际执行的函数参数值来简化符号约束。

5. 定向分析感兴趣的代码: 动态插桩可以帮助定位样本中的关键代码区域,如解密函数、网络通信函数等。然后,可以使用符号执行重点分析这些区域,生成能够到达这些函数的输入,并详细分析其行为。

6. 环境建模: 样本的行为通常依赖于系统环境。动态插桩可以捕获样本与环境的交互,如系统调用、库函数调用等。这些信息可以用于构建环境模型,供符号执行使用。符号执行可以在这个模型上进行推理,模拟样本在不同环境下的行为。

7. 行为规避: 如果样本使用反调试、反虚拟化等技术来阻碍动态分析,可以首先使用符号执行来分析样本,确定规避行为的触发条件。然后,在动态插桩时避免或绕过这些条件,以获取样本的真实行为。