#Selective Symbolic Execution
符号注入
对于某些二进制文件，只能以符号方式执行程序的子集。例如，我们可能希望在内核中而不是整个操作系统中象征性地执行设备驱动程序。为了支持这一点，符号执行中的常用方法是具体执行直到某个点，然后为任意数量的所需位置插入符号值。请注意，虽然标准输入自动符号化，但通常必须手动注入符号。
在CTF的第二个模块中，给出了要求学生以编程方式将符号注入程序模拟。为了促进这一点，学生将了解程序状态的概念以及如何使用angr来具体执行二进制文件，直到达到程序中的某个点。然后向学生介绍用于实例化符号的数据结构，并将其注入程序的执行状态。具体而言，介绍了通过Claripy实现的bitvectors的概念，并显示了使用该工具的示例脚本。通过这种方式，学生可以获得必须将符号注入执行状态才能解决。在一个层面上，他们用符号替换特定的注册表。在其他级别中，它们替换存储在静态分配的全局内存中，存储在堆中的动态分配的内存中或存储在堆栈中的特定位置的变量。最后，它们被赋予一个级别，其中文件的内容被视为符号。
图6显示了在使一组寄存器符号化后，要求学生在程序中间开始符号执行的级别的反汇编。调用函数获取用户输入，将值读入三个不同的寄存器。学生将符号注入每个寄存器并在从函数返回后立即开始符号执行（0x80488d1）。图7显示了实现解决方案的angr脚本的一部分。如脚本所示，在指定符号执行的起始地址后，Claripy位向量被声明并注入执行状态。然后在调用执行引擎来解决级别之前，为成功和失败定义条件。
约束和函数钩子
第三个模块引入了约束和函数钩子，用于减少被搜索的状态空间，以减少众所周知的函数的复杂性。在符号上添加约束类似于避免如前所述的某些执行状态。当人们可以在执行期间部分约束某些符号时，有效地将某些符号输入具体化，它允许符号执行引擎专注于更有趣的输入。为了练习应用约束，第三个模块包括一个级别，在该级别中，可以在执行的特定部分期间应用约束，当满足时，将允许执行返回解决方案而无需进一步执行。
解决这个问题的另一种方法是用简化的等价物替换复杂但众所周知的函数。例如，不是象征性地执行昂贵且可能不必要的复杂标准C库例程，而是自动挂钩其中的许多例程，而是用一个简单执行的简化汇总例程替换它们。为了教会学生如何利用钩子，需要它们在符号执行引擎中实现钩子的级别，以便用更简单的摘要替换正在分析的程序的部分。图8显示了一个级别的片段，其中学生将标准C库中的复杂调用替换为angr提供的更简单的等价物，这些等价物在Python中编写并具体执行。这样，可以在极短的时间内解决水平。请注意，虽然这个级别可以通过蛮力来解决，但学生们通常坚持以预期的方式解决水平，以了解水平试图教他们的水平。