0x03.Lab 3: Symbolic execution

本 lab 将教大家使用 符号执行 （symbolic execution）这一强大的技术来寻找软件中的漏洞，在 lab 的最后我们将建立一个可以在 zoobar web 应用中寻找触发多种漏洞的符号执行系统（准确的说是一个混合执行（concolic execution）系统）

关于什么是 concolic execution，可以看这张图

在 EXE paper 中描述了一个用于 C 程序的符号执行系统，为了简单化，该 lab 将通过修改 Python 对象与重载特定方法来为 Python 程序建立一个符号/混合执行系统，类似于 EXE，我们将使用一个 SMT （ Satisfiability Modulo Theories，可满足性模理论）求解器来检查可满足的约束，这意味着我们的求解器可以检查同时包含传统布尔可满足性表达式与涉及其他“理论”的约束如整型、位向量、字符串等

本 lab 初始我们首先要通过计算 32 位有/无符号数的平均值来熟悉 Z3——一个流行的 SMT 求解器，接下来我们将为 Python 整型操作创建 wrappers（类似 EXE 提供了符号变量上的操作置换），并应用调用 Z3 的核心逻辑来探索可能的不同执行路径；最终我们将探索如何将其应用在 web 应用程序上，以对字符串进行求解，我们将为 Python 的字符串操作套一层 wrapper，在 SQLalchemy 数据库接口上应用对符号化友好的（symbolic-friendly）wrapper，并使用这个系统寻找 Zoobar 中的漏洞

上面两段都是抄实验手册的

接下来首先还是惯例地切换到 lab 3 的分支：

$ git commit -am 'lab2 completed'
$ git pull
$ git checkout -b lab3 origin/lab3

这里注意不要将 lab 2 的代码合并到 lab 3 里边，因为我们的符号执行系统无法通过 RPC 追踪多进程间的符号约束，所以我们在一个没有进行权限分离的 Zoobar 上进行符号执行

接下来是检查代码可用性：

$ make check

结果如下就🆗，需要注意的是符号执行系统是 CPU 密集型的，因此对于不开启 KVM 支持的 QEMU 而言会非常慢：

、

Using an SMT solver

符号执行的核心是 可满足性模理论求解器（Satisfiability Modulo Theory solver，即 SMT solver），在本 lab 中我们将使用微软开发的 Z3 solver 的 Python-based API（参见 z3py tutorial & documentation for Z3’s Python API），并使用 Z3’s support for strings；本 Lab 带有一个构建自 Z3 github repo 的 Z3

实验提供了 int-avg.py 作为使用 Z3 的例子： 计算两个 32 位整型的平均值 ，一个最简单的算法是 (x + y) / 2 ，但这可能会发生整型上溢，从而得到 模 2³² 上的值（想了解更多，参见 KINT paper ）——Z3 可以帮我们检查这个错误：予其一个布尔表达式，Z3 可以告诉我们其是否为真（即可以被满足）；若表达式可以为真且包含一些变量，Z3 可以给我们一些使表达式为真的🌰变量

现在我们来看这份代码（这里不会仔细讲 Z3 的用法，不懂的自行查文档），其首先会使用 Z3 创建两个 32 位的位向量 a 与 b：

#!/usr/bin/env python3

import z3

## Construct two 32-bit integer values.  Do not change this code.
a = z3.BitVec('a', 32)
b = z3.BitVec('b', 32)

接下来分别计算有/无符号除法下两数的平均值，注意这里并没有实际进行计算，而仅是保存了符号变量表达式：

## Compute the average of a and b.  The initial computation we provided
## naively adds them and divides by two, but that is not correct.  Modify
## these lines to implement your solution for both unsigned (u_avg) and
## signed (s_avg) division.
##
## Watch out for the difference between signed and unsigned integer
## operations.  For example, the Z3 expression (x/2) performs signed
## division, meaning it treats the 32-bit value as a signed integer.
## Similarly, (x>>16) shifts x by 16 bits to the right, treating it
## as a signed integer.
##
## Use z3.UDiv(x, y) for unsigned division of x by y.
## Use z3.LShR(x, y) for unsigned (logical) right shift of x by y bits.
u_avg = z3.UDiv(a + b, 2)
s_avg = (a + b) / 2

由于 32 位整数加法可能存在溢出，故这里为了求得其正确的平均值，我们将其扩展为两个 33 位的位向量，完成计算后再截断回 32 位（不会导致结果错误，因为 32 位的平均值总会在 32 位内）：

## Do not change the code below.

## To compute the reference answers, we extend both a and b by one
## more bit (to 33 bits), add them, divide by two, and shrink back
## down to 32 bits.  You are not allowed to "cheat" in this way in
## your answer.
az33 = z3.ZeroExt(1, a)
bz33 = z3.ZeroExt(1, b)
real_u_avg = z3.Extract(31, 0, z3.UDiv(az33 + bz33, 2))

as33 = z3.SignExt(1, a)
bs33 = z3.SignExt(1, b)
real_s_avg = z3.Extract(31, 0, (as33 + bs33) / 2)

最后就是求解是否存在能够发生整型溢出的约束，即：是否存在这样的两个 32 位整型变量值使得其 32 位下运算结果不与真实计算结果相等：

def printable_val(v, signed):
    if type(v) == z3.BitVecNumRef:
        if signed:
            v = v.as_signed_long()
        else:
            v = v.as_long()
    return v

def printable_model(m, signed):
    vals = {}
    for k in m:
        vals[k] = printable_val(m[k], signed)
    return vals

def do_check(msg, signed, avg, real_avg):
    e = (avg != real_avg)
    print("Checking", msg, "using Z3 expression:")
    print("    " + str(e).replace("\n", "\n    "))
    solver = z3.Solver()
    solver.add(e)
    ok = solver.check()
    print("  Answer for %s: %s" % (msg, ok))

    if ok == z3.sat:
        m = solver.model()
        print("  Example:", printable_model(m, signed))
        print("  Your average:", printable_val(m.eval(avg), signed))
        print("  Real average:", printable_val(m.eval(real_avg), signed))

结果如下，Z3 求解器帮助我们找到了这样的值：

接下来是 Exercise 1：通过修改 int-avg.py 中的 u_avg = ... 一行，实现一个正确的函数，以在 32 位运算下正确计算出 a 与 b 的无符号平均值，不能改变操作数的位宽

Exercise 1. Implement a correct function to compute the unsigned average of a and b using only 32-bit arithmetic, by modifying the u_avg = ... line in int-avg.py.

For the purposes of this exercise, you are not allowed to change the bit-widths of your operands. This is meant to represent the real world, where you cannot just add one more bit to your CPU’s register width.

You may find it helpful to search online for correct ways to perform fixed-width integer arithmetic. The book Hacker’s Delight by Henry S. Warren is a particularly good source of such tricks.

Check your averaging function by re-running ./int-avg.py or make check. If your implementation is correct, int-avg.py should produce the message Answer for unsigned avg: unsat.

这里笔者给出一个比较笨的解法（毕竟笔者的脑子: (也想不出啥聪明解法）：

(a / 2) + (b / 2) + ((a % 2) + (b % 2)) / 2

这个算法的思路比较简单，最初的出发点就是两数之和的平均值不会超出 2³²，那么我们只要先将两数分别除以2再相加就不会发生溢出了，但是奇数除以2会丢失 0.5，所以如果两个数都是奇数的话最后的结果会丢掉1，那么这里我们再将其加上即可

这里需要注意的是 Z3 默认为带符号运算，故这里我们应当使用 z3.UDiv() 来进行无符号除法运算：

u_avg = z3.UDiv(a, 2) + z3.UDiv(b, 2) + ((a % 2) + (b % 2)) / 2

运行 make check，成功通过 Exercise 1：

除了这个算法之外，笔者还了解到有一种算法是利用位运算来进行计算：

(a & b) + ((a ^ b) >> 1)

这个算法的基本原理是先提取出公有部分，再计算私有部分的平均值，最后相加即可得到结果；这个算法也能通过 Exercise 1 ，这里就不重复贴图了

接下来是 Challenge 1：通过修改 int-avg.py 中的 s_avg = ... 一行，实现一个正确的函数，以在 32 位运算下正确计算出 a 与 b 的有符号平均值

Challenge! (optional) For extra credit, figure out how to compute the average of two 32-bit signed values. Modify the s_avg = ... line in int-avg.py, and run ./int-avg.py or make check to check your answer. Keep in mind the direction of rounding: 3/2=1 and -3/2=-1, so so the average of 1 and 2 should be 1, and the average of -2 and -1 should be -1.

As you explore signed arithmetic, you may find it useful to know that Z3 has two different modulo-like operators. The first is signed modulo, which you get by using a % b in the Python Z3 API. Here, the sign of the result follows the sign of the divisor (i.e., b). For example, -5 % 2 = 1. The second is signed remainder, which you get by using z3.SRem(a, b). Here, the sign of the result follows the sign of the dividend (i.e., a). With the same example inputs, z3.SRem(-5, 2) = -1.

对于带符号值的运算而言，限制在 32 位内的正确计算便没有那么简单了，若我们直接用上面的式子进行计算则很容易被 Z3 找到能导致运算结果错误的例子：

为什么在有符号除法下计算出来的结果不一致呢？这是因为在题目中~~MIT 非常SB地~~对于正数除法其选择向下取整，对于负数除法的截断，其选择的是向上取整，但我们的算法是正数与负数皆向下取整，因此计算结果就出现了偏差

由于正数部分没有问题，因此这里我们需要对计算结果为负数的情况进行特殊化处理，在结果为负数时将向下取整变为向上取整，因此最后的计算公式如下：

tmp = (a & b) + ((a ^ b) >> 1)
res = tmp + ((tmp >> 31) & (a ^ b))

首先按照我们原来的公式计算出向下取整的结果，接下来对其符号位进行判断，若为 1 则再判断其私有部分平均值的计算是否发生截断（即私有部分和是否为奇数），若是则说明结果发生了向下取整，此时变为向上取整即可

由于要对符号位进行判断，所以这里我们使用 z3.LShR() 将初始运算结果作为无符号整型进行右移操作：

tmp = (a & b) + ((a ^ b) >> 1)
s_avg = tmp + (z3.LShR(tmp, 31) & (a ^ b))

运行结果如下，成功通过 Challenge 1：

Interlude: what are symbolic and concolic execution?

正如我们前面在 EXE 的论文中所见，符号执行是一种通过观测程序在不同输入下如何表现来进行程序测试的方法，通常而言其目的是为了获得更高的 代码覆盖率 （code coverage）或是 路径覆盖率 （path coverage），在安全中其比传统代码执行更能触发罕见的可能包含漏洞的代码路径

从更高层次而言，若我们要构建一个符号执行系统，我们需要解决以下几点：

由于程序包含基于输入的中间值（例如输入两个整型并计算平均值，并存放在一些变量中），我们需要记住输入与这些中间值间的关系，通常这通过允许变量或内存位置有 具体的 （concrete，例如 114514 这样的实际值）或 符号的 （symbolic，例如我们在上一小节构建的符号变量）值
我们需要根据输入来确定要执行的控制流分支，这归结于在程序每次发生分支时构建符号约束，在程序选择一些特定分支时描述布尔条件（以程序原有输入的形式）；由于我们持续保存中间值与程序原有输入的间隙，我们并不需要通过原有输入来计算约束，这些约束就像我们在前文中用来寻找整型中漏洞的约束；确定控制流约束非常重要，因为若程序初始时进入了特定分支路径，我们想要知道如何让他走到另一条路径来寻找是否存在漏洞，在 EXE 的论文中使用了一个 C-to-C 的翻译器来在所有的分支上插入他们的代码
对于每一条上述分支，我们需要决定是否有一个输入能够让程序在一条分支上执行另一条路径（更准确地说，我们考虑整个控制流路径而非单个路径），这帮助我们在程序中寻找可以让我们通过调整输入来影响的控制流条件，所有的符号执行系统都基于 SMT 求解器来完成这些工作
我们需要确定我们在测试中寻找的是什么，这是我们从程序中确保 不变量 （invariant）来考虑的最佳方法，而符号执行寻找改变这些常量的输入（~~👴也没咋读明白，可以看实验手册原句~~）；我们可以寻找的事物之一是程序崩溃（crashes，即不变量是 我们的程序不应当崩溃 ），在 C 程序中这非常有意义，因为 crashes 通常指示了代表漏洞的内存损坏，在 Python 这样更高级的语言中在设计上并不存在内存损坏，但我们仍然可以寻找如 Python 代码级的代码注入攻击（例如 eval() ）或是特定于某种应用的影响安全的不变量
最终，对于给出程序中所有可能执行的控制流路径，我们需要决定该尝试哪条路径，因为路径数量会随着程序规模的增大而快速增长，我们不可能尝试所有的路径，因此符号执行系统通常包含确定哪一条路径更有希望发现破坏不变量的某种 调度器 （scheduler）或 搜索策略 （search strategy），一个简单的搜索策略例子便是尝试未执行过的路径，这代表着更高的代码覆盖率与未被发现的漏洞的存在的可能性

与符号执行相对的一个选择是 fuzzing （又称 fuzz-testing，模糊测试），其选择了一个随机化方案：不同于关注触发应用中不同代码路径的原因，fuzzing 会创建随机的具体值交给程序执行并检查其行为；虽然这比符号执行更简单，但通常很难构造能满足程序代码中一些特定情况的输入

构建符号执行系统的一个挑战是我们的系统需要知道如何在符号值上执行所有可能的操作（上面的 Step 1 & 2），在本 Lab 中我们将在 Python 对象（更准确地说，整型与字符串）上实践，对于符号执行而言这很有挑战性，因为 Python 对象可以实现的操作有很多

幸运的是我们还有一个更简单的选择—— 混合执行 （concolic execution），介于完全随机的模糊测试与完全的符号执行之间，相较于跟踪纯净的符号值（如 EXE 中所做），其思想是：对于从输入中得到的变量，我们可以同时保存一个具体值与一个符号值，由此：

若我们的 concolic system 知道应用的行为，我们可以像符号执行那样运行（除了我们还会同时传播每个值的 concrete 部分）；例如，假设我们有两个 concolic 整型变量 aa 与 bb，其有着具体值 5 与 6 ，并对应符号表达式 a 与 b，此时若应用创建了一个变量 cc = aa + bb，其会同时有着具体值 11 及符号表达式 a + b；类似地，若应用在 cc == 12 的分支上执行，程序可以像分支为假一样执行，并记录对应的符号分支条件 a + b != 12
若我们的 concolic system 不知道应用的当前行为，应用将只会得到具体的值；例如若应用将 cc 写入文件中，或者是传递到外部库中，代码仍可以使用具体值 11 如同应用正常运行那样继续执行

对于本 lab 而言，混合执行的好处是我们并不需要完全完成对符号值的操作支持，我们只需要支持足够发现漏洞的操作即可（实际上大部分挖洞系统也是如此），不过若应用执行了我们所不支持的操作，我们将失去对符号部分的跟踪，并无法对这些路径进行符号执行式的（symbolic-execution-style）探索，若想了解更多可以参见 DART paper

Concolic execution for integers

首先我们将为整型值构建一个混合执行系统，本 Lab 为我们的混合执行提供的框架代码位于 symex/fuzzy.py 中，其实现了几个重要的抽象层：

抽象语法树（The AST）：与此前我们在 int-avg.py 中使用 Z3 表达式来表示符号值所不同的是，本 Lab 构建了其自己的抽象语法树（abstract syntax tree）来表达符号表达式，一个 AST 节点可以是一个简单的变量（ sym_str 或 sym_int 对象）、一个常量（const_int、const_str 或 const_bool 对象）、或是一些将其他 AST 节点作为参数的函数或操作符（例如 sym_eq(a, b) 表示布尔表达式 a==b，其中 a 与 b 都是 AST 节点，或是 sym_plus(a, b) 表示整型表达式 a + b）

每个 AST 节点 n 都可以使用 z3expr(n) 转化为 Z3 表达式，这由调用 n._z3expr 完成，即每个 AST 节点都实现了返回对应 Z3 表达式的 _z3expr 方法

我们使用自己的 AST 层而非使用 Z3 的符号表示的原因是因为我们需要实现一些 Z3 表示难以完成的操作，此外我们需要分出一个独立的进程来调用 Z3 的求解器，以在 Z3 求解器耗时过长时杀死进程——将约束归为不可解（这种情况下我们可能失去这些路径，但至少我们会让程序探索其他路径）；使用我们自己的 AST 能让我们将 Z3 状态完全独立在 fork 出的进程里
混合封装（The concolic wrappers）：为了拦截 python-level 的操作并进行混合执行，我们将常规的 int 与 str 对象替换成了混合的子类：concolic_int 继承自 int 而 concolic_str 继承自 str，每一个混合封装都同时存储一个具体值（self.__v ）与一个符号表达式（与 AST 节点，在 self.__sym），当应用在计算混合值表达式（例如 a+1 中的 a 为 concolic_int），我们需要拦截该操作并返回一个同时包含具体值与符号表达式的的混合值

为了实现这样的拦截操作，我们重载了 concolic_int 与 concolic_str 类中的一些方法，例如 concolic_int.__add__ 在上面的例子 a + 1 中会被调用并返回一个新的混合值表示结果

原则上我们应该也要有一个 concolic_bool 作为 bool 的子类，不幸的是在 Python 中 bool 不能被继承（参见这里与这里），于是我们创建了函数 concolic_bool 作为代替，当我们创建一个混合布尔值时，程序会按其值进行分支，故 concolic_bool 也会为当前路径条件添加一个约束（布尔值的符号表达式与具体值相等的约束），并返回一个具体的布尔值
具体输入（The concrete inputs）：在混合执行下被测试的程序输入都存储在 concrete_values 字典中，在该字典中存储了程序输入的字符串名字，并将每个名字映射到对应的输入值（整型变量的值为python整型，字符串变量为python字符串）

concrete_value 被设为全局变量的原因是应用通过调用 fuzzy.mk_str(name) 或 fuzzy.mk_int(name) 来创建一个混合字符串或混合整型，其返回一个混合值，其中的符号部分为一个新的 AST 节点对应到一个名为 name 的变量，但具体值被在 concrete_values 中查找，若字典中没有与之关联的变量，系统将其设为默认的初始值（整型为0，字符串为空串）

混合执行框架在一个 InputQueue 对象中维持一个待尝试的不同输入的队列，框架首先会添加一个初始输入（空字典 {}），之后执行代码，若应用进入了分支，混合执行系统将唤醒 Z3 来带来新的输入以测试代码中的其他分支，将这些输入放到输入队列中，并保持迭代直到没有输入可以尝试
可满足性模理论求解器（The SMT solver）： fork_and_check(c) 函数会检查约束 c （一个 AST 节点）是否为可满足的表达式，并返回一对值：可满足性状态 ok 及示例模型（分配给变量的值），若约束可以被满足则 ok 为 z3.sat ，若约束不可被满足则 ok 为 z3.unsat 或 z3.unknown；该函数内部会 fork 一个独立的进程来运行 Z3 求解器，若耗时超过 z3_timeout 则杀死进程并返回 z3.unknown
当前路径条件（The current path condition）：当应用执行并基于混合值决定控制流时（参见上面关于 concolic_bool 的讨论），表示该分支的约束会被添加到 cur_path_constr 列表中，为了生成能够沿着一条分支从一个点进行不同选择的输入，所需的约束为路径上该点之前的约束集合，加上该点的反向约束；为了帮助调试与启发式搜索，触发了分支的代码行的信息会被存放在 cur_path_constr_callers 列表中

接下来我们的工作是完成对 concolic_int 的实现，并将代码应用于混合执行循环的核心，本 Lab 提供了两个测试程序： check-concolic-int.py 与 check-symex-int.py

混合执行框架代码浅析 - Part 1

在做 Exercise 之前，我们先看一下这个混合执行框架的代码结构，其核心代码主要位于 symex/fuzzy.py 中

I. AST 节点

首先是 AST 节点，作为所有符号类的父类而存在，定义比较简单：

class sym_ast(object):
  def __str__(self):
    return str(self._z3expr())

II. 符号运算

然后是 sym_func_apply 类，作为所有符号操作的父节点，这里主要重载了 __eq__() 和 __hash__() 方法，用于比较与计算哈希值，比较的方法就是判断是否所有参数相等，哈希值的计算则是所有参数的哈希值进行异或：

class sym_func_apply(sym_ast):
  def __init__(self, *args):
    for a in args:
      if not isinstance(a, sym_ast):
        raise Exception("Passing a non-AST node %s %s as argument to %s" % \
                        (a, type(a), type(self)))
    self.args = args

  def __eq__(self, o):
    if type(self) != type(o):
      return False
    if len(self.args) != len(o.args):
      return False
    return all(sa == oa for (sa, oa) in zip(self.args, o.args))

  def __hash__(self):
    return functools.reduce(operator.xor, [hash(a) for a in self.args])

然后是三个类 sym_unop 、sym_binop 、sym_triop，表示带有1、2、3个操作数的封装，可以使用 a 、b 、c 获得第 1、2、3个操作数：

class sym_unop(sym_func_apply):
  def __init__(self, a):
    super(sym_unop, self).__init__(a)

  @property
  def a(self):
    return self.args[0]

class sym_binop(sym_func_apply):
  def __init__(self, a, b):
    super(sym_binop, self).__init__(a, b)

  @property
  def a(self):
    return self.args[0]

  @property
  def b(self):
    return self.args[1]

class sym_triop(sym_func_apply):
  def __init__(self, a, b, c):
    super(sym_triop, self).__init__(a, b, c)

  @property
  def a(self):
    return self.args[0]

  @property
  def b(self):
    return self.args[1]

  @property
  def c(self):
    return self.args[2]

基于 sym_func_apply 与 op 类，封装了相等比较、与、或、非四个操作，其实现原理主要还是转成 Z3 表达式后利用 Z3 的与或非进行运算：：

## Logic expressions

class sym_eq(sym_binop):
  def _z3expr(self):
    return z3expr(self.a) == z3expr(self.b)

class sym_and(sym_func_apply):
  def _z3expr(self):
    return z3.And(*[z3expr(a) for a in self.args])

class sym_or(sym_func_apply):
  def _z3expr(self):
    return z3.Or(*[z3expr(a) for a in self.args])

class sym_not(sym_unop):
  def _z3expr(self):
    return z3.Not(z3expr(self.a))

符号数的加减乘除比较等操作都是基于上面封装的 op 类完成的：

乘除等运算需要我们在后续的 Exercise 中自行实现

class sym_lt(sym_binop):
  def _z3expr(self):
    return z3expr(self.a) < z3expr(self.b)

class sym_gt(sym_binop):
  def _z3expr(self):
    return z3expr(self.a) > z3expr(self.b)

class sym_plus(sym_binop):
  def _z3expr(self):
    return z3expr(self.a) + z3expr(self.b)

class sym_minus(sym_binop):
  def _z3expr(self):
    return z3expr(self.a) - z3expr(self.b)

III. 常量

字符串常量 const_str 、整型常量 const_int 、布尔常量 const_bool 的实现比较简单，主要就是继承自 sym_ast 并且储存对应的值，其中字符串常量在转为 Z3 表达式时会调用 z3.StringVal()：

class const_str(sym_ast):
  def __init__(self, v):
    self.v = v

  def __eq__(self, o):
    if not isinstance(o, const_str):
      return False
    return self.v == o.v

  def __hash__(self):
    return hash(self.v)

  def _z3expr(self):
    return z3.StringVal(self.v)

class const_int(sym_ast):
  def __init__(self, i):
    self.i = i

  def __eq__(self, o):
    if not isinstance(o, const_int):
      return False
    return self.i == o.i

  def __hash__(self):
    return hash(self.i)

  def _z3expr(self):
    return self.i

class const_bool(sym_ast):
  def __init__(self, b):
    self.b = b

  def __eq__(self, o):
    if not isinstance(o, const_bool):
      return False
    return self.b == o.b

  def __hash__(self):
    return hash(self.b)

  def _z3expr(self):
    return self.b

IV. 符号变量

在该框架中定义了两种类型的符号变量：sym_int 与 sym_str，都是直接基础自 AST 节点类：

## Arithmetic

class sym_int(sym_ast):
  def __init__(self, id):
    self.id = id

  def __eq__(self, o):
    if not isinstance(o, sym_int):
      return False
    return self.id == o.id

  def __hash__(self):
    return hash(self.id)

  def _z3expr(self):
    return z3.Int(self.id)

###...

## String operations

class sym_str(sym_ast):
  def __init__(self, id):
    self.id = id

  def __eq__(self, o):
    if not isinstance(o, sym_str):
      return False
    return self.id == o.id

  def __hash__(self):
    return hash(self.id)

  def _z3expr(self):
    return z3.Const(self.id, z3.StringSort())

V. 混合变量

正如前文所言，我们实际上在混合执行引擎当中使用的为混合型（concolic）的变量来储存约束值，框架中提供了两种类型的混合变量——concolic_int （整型）与 concolic_str（字符串），其中具体值（conctre value）存放在 __v 成员中，符号值（symbolic value）存放在 __sym 中

主要是大量的运算符重载，这里就不贴完整代码了，可以自己去看（笑）：

class concolic_int(int):
  def __new__(cls, sym, v):
    self = super(concolic_int, cls).__new__(cls, v)
    self.__v = v
    self.__sym = sym
    return self

## ...

class concolic_str(str):
  def __new__(cls, sym, v):
    assert type(v) == str
    self = super(concolic_str, cls).__new__(cls, v)
    self.__v = v
    self.__sym = sym
    return self

##...

接下来是 Exercise 2：通过增加整型乘法与除法支持来完成对 symex/fuzzy.py 中 concolic_int 的实现，我们需要重载额外的方法并为乘除法运算添加 AST 节点，并为这些 AST 节点应用 _z3expr

Exercise 2. Finish the implementation of concolic_int by adding support for integer multiply and divide operations. You will need to overload additional methods in the concolic_int class (see the documentation for operator functions in Python 3), add AST nodes for multiply and divide operations, and implement _z3expr appropriately for those AST nodes.

Look for the comments Exercise 2: your code here in symex/fuzzy.py to find places where we think you might need to write code to solve this exercise.

Run ./check-concolic-int.py or make check to check that your changes to concolic_int work correctly.

我们首先实现符号变量乘除所需的 sym_binop 子类，这里我们参照前面的加减运算直接调用 z3expr() 来返回 Z3 表达式即可

需要注意的是虽然 python 的除法运算有 / 与 //两种，但是 Z3并不支持 ArithRef 与 int 直接进行 // 运算，所以这里我们只实现一个普通的乘法即可：

## Exercise 2: your code here.
## Implement AST nodes for division and multiplication.
class sym_mul(sym_binop):
  def _z3expr(self):
    return z3expr(self.a) * z3expr(self.b)

class sym_div(sym_binop):
  def _z3expr(self):
    return z3expr(self.a) / z3expr(self.b)

接下来我们重写 concolic_int 的乘法与除法，我们先参考一下 concolic_int 中的加法运算方式：、

首先判断运算对象是否为 concolic_int ，若是则将自身具体值加上对象具体值，否则直接加上该对象，结果存放到 res
创建一个新的 concolic_int 实例作为返回值，res 作为其具体值部分，创建两个 ast 实例并利用 sym_plus() 计算结果作为新 concolic_int 的符号值部分

  def __add__(self, o):
    if isinstance(o, concolic_int):
      res = self.__v + o.__v
    else:
      res = self.__v + o
    return concolic_int(sym_plus(ast(self), ast(o)), res)

那么我们的乘除法其实依葫芦画瓢即可，这里需要注意的是我们要同时实现 / 与 // 两种除法运算：

  ## Exercise 2: your code here.
  ## Implement symbolic division and multiplication.
  def __mul__(self, o):
    if isinstance(o, concolic_int):
      res = self.__v * o.__v
    else:
      res = self.__v * o
    return concolic_int(sym_mul(ast(self), ast(o)), res)
  
  def __truediv__(self, o):
    if isinstance(o, concolic_int):
      res = self.__v / o.__v
    else:
      res = self.__v / o
    return concolic_int(sym_div(ast(self), ast(o)), res)

  def __floordiv__(self, o):
    if isinstance(o, concolic_int):
      res = self.__v // o.__v
    else:
      res = self.__v // o
    return concolic_int(sym_div(ast(self), ast(o)), res)

运行，成功通过 Exercise 2：

然后是 Exercise 3，主要是让我们熟悉混合执行系统的使用方式，这里提供的途径是修改 symex_exercises.py 以给予测试系统正确的输入：

Exercise 3. An important component of concolic execution is concolic_exec_input() in symex/fuzzy.py. We have given you the implementation. You will use it to build a complete concolic execution system. To understand how to use concolic_exec_input(), you should create an input such that you pass the first check in symex/check-symex-int.py. Don’t modify symex/check-symex-int.py directly, but instead modify symex_exercises.py. Run ./check-symex-int.py or make check to check your solution.

混合执行框架的核心组件便是 symex/fuzzy.py 中的 concolic_exec_input() ，题目说后续我们将用其实现一个完整的混合执行系统，那我们先来看其相关的具体实现

混合执行框架代码浅析 - Part 2

VI.具体值字典 - ConcreteValues

如前文所言，在混合执行下被测试的程序输入都存储在一个全局字典中，实为一个ConctreteValues 类对象，实际上就是 python 字典的一个 wrapper

# ConcreteValues maintains a dictionary of variables name to values.
# If a variable is created and it doesn't exist, we use a default
# value for the variable (0 for int and '' for string).
class ConcreteValues(object):
  def __init__(self):
    self.concrete_values = {}

在 symex/fuzzy.py 中有一个全局变量 current_concrete_values，实际上就是我们前面所说的全局具体值字典，我们可以使用ConctreteValues.mk_global() 使该对象变为全局引用，即我们每次使用只需要创建一个ConctreteValues 对象即可：

# During concolic execution, new variables will be added to
# current_concrete_values, which is an instance of ConcreteValues.
# This variable is global because application code, the concolic
# Execution engine, and test code, all create new variables.  We make
# it global so that we don't have to modify application code.  At the
# start of a concolic execution we will set this variable to the
# concrete values to be used.

current_concrete_values=None

#...

  def mk_global(self):
    global current_concrete_values
    current_concrete_values = self

在该类中有三个查询字典内 id 对应具体值并返回混合值的函数，若 id 不在字典内则进行添加，同时在 symex/fuzzy.py 中带有三个对这些函数的 wrapper：

  def mk_int(self, id, initval):
    if id not in self.concrete_values:
      self.concrete_values[id] = initval
    return concolic_int(sym_int(id), self.concrete_values[id])

  def mk_str(self, id, initval):
    if id not in self.concrete_values:
      self.concrete_values[id] = initval
    return concolic_str(sym_str(id), self.concrete_values[id])

  def mk_bytes(self, id, initval):
    if id not in self.concrete_values:
      self.concrete_values[id] = initval
    return concolic_bytes(sym_str(id), self.concrete_values[id])

#...

# Wrapper functions to allow application code to create new
# variables. They will be added to the current global current
# concrete values.
def mk_int(id, initval):
  global current_concrete_values
  return current_concrete_values.mk_int(id, initval)

def mk_str(id, initval):
  global current_concrete_values
  return current_concrete_values.mk_str(id, initval)

def mk_bytes(id, initval):
  global current_concrete_values
  return current_concrete_values.mk_bytes(id, initval)

除了上面的函数以外，也可以直接使用 add() 成员函数来向字典内添加映射：

  def add(self, id, v):
    self.concrete_values[id] = v

以及还有一个 canonical_rep() 成员函数用以返回字典中的键值对元组排序列表，以及 var_names() 用以返回 id 列表：

  def canonical_rep(self):
    return sorted(self.concrete_values.items())

#...

  def var_names(self):
    return self.concrete_values.keys()

以及一个 inherit() 成员函数用以从另一个字典中拷贝键值对：

  def inherit(self, o):
    for id in o.concrete_values:
      if id not in self.concrete_values:
        self.concrete_values[id] = o.concrete_values[id]

VII. concolic_exec_input() - 输入执行

该函数内容用以根据给予的字典对传入的函数进行执行，整体逻辑比较简单：

初始化两个全局空列表 cur_path_constr （当前路径的条件约束）与 cur_path_constr_callers（当前路径的信息）
调用 concrete_values.mk_global() 使其成为一个全局字典
调用传入的函数指针来获得一个值 v，若参数 verbose > 1 则打印两个列表的内容
最后的返回值为 (v, cur_path_constr, cur_path_constr_callers)

# Concolically execute testfunc with the given concrete_values. It
# returns the value testfunc computes for the given concrete_values
# and the branches it encountered to compute that result.
def concolic_exec_input(testfunc, concrete_values, verbose = 0):
  global cur_path_constr, cur_path_constr_callers
  cur_path_constr = []
  cur_path_constr_callers = []
    
  if verbose > 0:
    print('Trying concrete value:', concrete_values)

  # make the concrete_value global so that new variables created
  # by testfunc(), directly or indirectly, will be added to
  # concrete_values.
  concrete_values.mk_global()
  v = testfunc()

  if verbose > 1:
    print('Test generated', len(cur_path_constr), 'branches:')
    for (c, caller) in zip(cur_path_constr, cur_path_constr_callers):
      print(indent(z3expr(c)), '@', '%s:%d' % (caller[0], caller[1]))

  return (v, cur_path_constr, cur_path_constr_callers)

可以看到在该函数中并没有更改路径约束与信息的列表，实际上这在 add_constr() 中完成，该函数在 concolic_bool() 中调用，将约束信息进行添加：

def add_constr(e):
  global cur_path_constr, cur_path_constr_callers
  cur_path_constr.append(simplify(e))
  cur_path_constr_callers.append(get_caller())

def concolic_bool(sym, v):
  ## Python claims that 'bool' is not an acceptable base type,
  ## so it seems difficult to subclass bool.  Luckily, bool has
  ## only two possible values, so whenever we get a concolic
  ## bool, add its value to the constraint.
  add_constr(sym_eq(sym, ast(v)))
  return v

而 concolic_bool() 实际上在 concolic_int 与 concolic_str 的运算符重载中进行调用，这也是为什么每次执行 concolic_exec_input() 都要重新将路径约束与信息列表清空的缘故，这里以 concolic_int 中的 __cmp__ 运算符为例：

  def __cmp__(self, o):
    res = int(self.__v).__cmp__(int(o))
    if concolic_bool(sym_lt(ast(self), ast(o)), res < 0):
      return -1
    if concolic_bool(sym_gt(ast(self), ast(o)), res > 0):
      return 1
    return 0

我们接下来来看 symex_exercises.py 里有啥，主要就一个 make_a_test() 函数，我们需要在其中完成全局具体值字典 concrete_values 的构建：

import symex.fuzzy as fuzzy

def make_a_test_case():
  concrete_values = fuzzy.ConcreteValues()
  ## Your solution here: add the right value to concrete_values
  return concrete_values

那么我们该如何修改 symex_exercises.py 中创建的字典呢？我们先看一下 Exercise 3 的评判标准，在 check_lab3.py 中检测的是运行 check-symex-int.py 后要输出 "Found input for 1234" 字符串：

def check_symex_int():
    sh('python3 check-symex-int.py >/tmp/lab3.log')
    if 'Found input for 1234' in file_read('/tmp/lab3.log'):
        log(green("PASS"), "Exercise 3: concrete input for 1234")
    else:
        log(red("FAIL"), "Exercise 3: concrete input for 1234")

我们接下来来看 check-symex-int.py ，其开头的逻辑如下，r 的值为 1234 即可通过 Exercise 3：

## This test case checks that you provided the right input in symex_exercises.
print('Calling f with a specific input..')
v = symex_exercises.make_a_test_case()
(r, constr, callers) = fuzzy.concolic_exec_input(test_f, v, verbose=1)
if r == 1234:
    print("Found input for 1234")
else:
    print("Input produced", r, "instead of 1234")

如前面我们对 concolic_exec_input() 的分析，r 的值由传入的函数指针决定，故我们来看 test_f() 的逻辑，主要就是用 mk_int() 从全局具体值字典中获取 id 为 i 的值传入 f() 中进行运算，若不存在 i 则 i 会被默认赋值 0 ：

def f(x):
    if x == 7:
        return 100
    if x*2 == x+1:
        return 70
    if x > 2000:
        return 80
    if x*2 == 1000:
        return 30000
    if x < 500:
        return 33
    if x // 123 == 7:
        return 1234
    return 40

def test_f():
    i = fuzzy.mk_int('i', 0)
    v = f(i)
    return v

由函数 f() 我们可以知道的是我们只需要向具体值字典中添加一个 i = 123 * 7 的值即可让 test_f() 返回 1234，故修改 symex_exercises.py 如下，这里用 mk_int() 和 add() 都可以：

import symex.fuzzy as fuzzy

def make_a_test_case():
  concrete_values = fuzzy.ConcreteValues()
  ## Your solution here: add the right value to concrete_values
  concrete_values.add('i', 123 * 7)
  return concrete_values

运行，成功通过 Exercise 3：

接下来是 Exercise 4，完成 symex/fuzzy.py 中 concolic_find_input 的实现：

Exercise 4. Another major component in concolic execution is finding a concrete input for a constraint. Complete the implementation of concolic_find_input in symex/fuzzy.py and make sure you pass the second test case of symex/check-symex-int.py. For this exercise, you will have to invoke Z3, along the lines of (ok, model) = fork_and_check(constr) (see the comments in the code). Run ./check-symex-int.py or make check to check your solution.

在该函数当中我们需要完成对约束的求解并返回对应的结果，因此这里需要使用 Z3 求解器来完成约束求解过程，不过这里已经将调用 Z3 的流程在 fork_and_check() 中完成封装，我们只需要调用该函数进行求解即可，那么我们先来看 fork_and_check() 的具体实现：

创建子进程调用 fork_and_check_worker() 进行约束求解，父子进程通过管道通信
父进程等待子进程的 SIGALRM 信号，若 z3_timeout 秒后未收到，杀死子进程
从管道接收结果并返回，若超时（子进程被杀，管道关闭）则返回 (z3.unknown, None)

## Support for forking because z3 uses lots of global variables

## timeout for Z3, in seconds
z3_timeout = 5

##...

def fork_and_check(constr):
  constr = simplify(constr)

  parent_conn, child_conn = multiprocessing.Pipe()
  p = multiprocessing.Process(target=fork_and_check_worker,
                              args=(constr, child_conn))
  p.start()
  child_conn.close()

  ## timeout after a while..
  def sighandler(signo, stack):
    print("Timed out..")
    # print z3expr(constr).sexpr()
    p.terminate()

  signal.signal(signal.SIGALRM, sighandler)
  signal.alarm(z3_timeout)

  try:
    res = parent_conn.recv()
  except EOFError:
    res = (z3.unknown, None)
  finally:
    signal.alarm(0)

  p.join()
  return res

接下来我们来看 fork_and_check_workder() 的具体实现：

新建一个 Z3 求解器将转化为字符串的约束表达式传入，调用 Solver.check() 求解
若求解成功，调用 Solver.model() 获得求解结果
判断结果中变量类型并转换为整型/字符串，对于字符串做额外处理，将结果放到一个 字符串→结果 映射的字典中并返回

Z3 这玩意用起来确实方便，不愧是微软大爹

def fork_and_check_worker(constr, conn):
  s = z3.Solver()
  s.add(z3expr(constr))
  ok = s.check()
  m = {}
  if ok == z3.sat:
    z3m = s.model()
    for k in z3m:
      v = z3m[k]
      if v.sort() == z3.IntSort():
        m[str(k)] = v.as_long()
      elif v.sort() == z3.StringSort():
        ## There doesn't seem to be a way to get the raw string
        ## value out of Z3..  Instead, we get the escaped string
        ## value.  We need to jump through hoops to unescape it.
        x = v.as_string()
        u = x.encode('latin1').decode('unicode-escape')
        m[str(k)] = u
      else:
        raise Exception("Unknown sort for %s=%s: %s" % (k, v, v.sort()))
  conn.send((ok, m))
  conn.close()

那么现在我们可以完成 Exercise 4 了，我们只需要调用 fork_and_check() 进行求解即可，需要注意的是我们返回的字典中的键值对应当只包含 ok_names 参数中所需要的键，若 ok_names == None 则将所有的键值对添加到字典中：

# Given a constraint, ask Z3 to compute concrete values that make that
# constraint true. It returns a new ConcreteValues instance with those
# values.  Z3 produces variables that don't show up in our
# applications and in our constraints; we filter those by accepting
# only variables names that appear in ok_names.
def concolic_find_input(constraint, ok_names, verbose=0):
  ## Invoke Z3, along the lines of:
  ##
  ##     (ok, model) = fork_and_check(constr)
  ##
  ## If Z3 was able to find example inputs that solve this
  ## constraint (i.e., ok == z3.sat), make a new input set
  ## containing the values from Z3's model, and return it.
  (ok, model) = fork_and_check(constraint)
  cv = ConcreteValues()
  if ok == z3.sat:
    sat = True
    res_names = model.keys() if ok_names is None else ok_names
    for k in res_names:
      cv.add(k, model[k])
  else:
    sat = False
  return sat, cv

成功通过 Exercise 4：

然后是 Exercise 5，完成 symex/fuzzy.py 中 concolic_force_branch 的实现：

提前说一下，这个 Exercise 5 的检查非常松，不要以为通过检查就是真的 Pass 了，最好自己再看看代码逻辑是否符合要求…

Exercise 5. A final major component in concolic execution is exploring different branches of execution. Complete the implementation of concolic_force_branch in symex/fuzzy.py and make sure you pass the final test case of symex/check-symex-int.py. Run ./check-symex-int.py or make check to check your solution.

正如前文所说，在遇到分支时我们需要逆转当前分支条件，以探索另一分支，该函数的作用实际上就是逆转 branch_conds 中的第 b 分支的条件，并返回新的约束条件集合，那么我们只需要取出该条件并使用 sym_not() 取反后再用 sym_and() 加上该分支之前所有的条件约束即可

注意这里的参数 b 为分支标号，branch_conds 与 branch_callers 为分支的条件与调用者数组：

# Compute a new constraint by negating the branch condition of the
# b-th branch in branch_conds. This constraint can be used to force
# the concolic execution to explore the other side of branch b.
def concolic_force_branch(b, branch_conds, branch_callers, verbose = 1):
  ## Compute an AST expression for the constraints necessary
  ## to go the other way on branch b.  You can use existing
  ## logical AST combinators like sym_not(), sym_and(), etc.
  ##
  ## Note that some of the AST combinators take separate positional
  ## arguments. In Python, to unpack a list into separate positional
  ## arguments, use the '*' operator documented at
  ## https://docs.python.org/3/tutorial/controlflow.html#unpacking-argument-lists

  constraint = None
  ## Exercise 5 by arttnba3
  ### negating the branch condition of the b-th branch
  b_cond = branch_conds[b]
  if (b_cond != const_bool(True)):
    constraint = sym_not(b_cond)
    for i in range(b):
      constraint = sym_and(constraint, branch_conds[i])
  ### end

  if verbose > 2:
    callers = branch_callers[b]
    print('Trying to branch at %s:%d:' % (callers[0], callers[1]))
    if constraint is not None:
      print(indent(z3expr(constraint).sexpr()))

  if constraint is None:
    return const_bool(True)
  else:
    return constraint

成功通过 Exercise 5：

最后是 Exercise 6， 使用我们在 Exercise 3-5 中涉及的几个函数来完成 concolic_execs()—— 完整的混合执行函数的构建，我们需要完成对 func 中的每一条分支的执行：

Exercise 6. Now implement concolic execution of a function in concolic_execs() in symex/fuzzy.py. The goal is to eventually cause every every branch of functo be executed. Read the comment for a proposed plan of attack for implementing that loop. The functions in the exercises 3-5 should be quite useful.

Run ./check-symex-int.py or make check to check that your concolic_execs() works correctly.

Beware that our check for this exercise is not complete. You may well find that later on something does not work, and you will have to revisit your code for this exercise.

我们先看 concolic_execs() 中已有的逻辑框架：

checked 为已经检查过的约束，outs 为最后求解所得结果，inputs 为待测试输入队列（输入为具体值字典）
由一个大循环持续调用concolic_exec_input() 计算约束
将新的约束解添加到结果中

# Concolic execute func for many different paths and return all
# computed results for those different paths.
def concolic_execs(func, maxiter = 100, verbose = 0):
  ## "checked" is the set of constraints we already sent to Z3 for
  ## checking.  use this to eliminate duplicate paths.
  checked = set()

  ## output values
  outs = []

  ## list of inputs we should try to explore.
  inputs = InputQueue()

  iter = 0
  while iter < maxiter and not inputs.empty():
    iter += 1
    concrete_values = inputs.get()
    (r, branch_conds, branch_callers) = concolic_exec_input(func, concrete_values, verbose)
    if r not in outs:
      outs.append(r)
    
    ## Exercise 6: your code here.

我们的代码需要添加在大循环的后半部分，那么我们先回顾一下在 Exercise 3-5 中我们都获得了哪些可用函数：

concolic_exec_input(testfunc, concrete_values, verbose = 0)：将 concrete_values 参数设为全局字典，之后执行给定的函数 testfunc，返回执行的结果值、分支条件列表、分支调用信息列表
concolic_find_input(constraint, ok_names, verbose=0)：使用 Z3 求解给定约束，返回 ok_names 列表中变量的值
concolic_force_branch(b, branch_conds, branch_callers, verbose = 1)：对给定约束条件 branch_conds 与分支 b，返回走向该分支另一路径的约束

接下来我们看 Lab 给的提示信息：

    ## Exercise 6: your code here.
    ##
    ## Here's a possible plan of attack:
    ##
    ## - Iterate over the set of branches returned by concolic_exec_input.
    ##
    ## - Use concolic_force_branch() to construct a constraint over
    ##   the inputs for taking the other side of that branch.
    ##
    ## - If this constraint is already in the "checked" set, skip
    ##   it (otherwise, add it to prevent further duplicates).
    ##
    ## - Use concolic_find_input() to construct a new input to test,
    ##   based on the above constraint.
    ##
    ## - Since Z3 might not assign values to every variable
    ##   (such as if that variable turns out to be irrelevant to
    ##   the overall constraint), inherit unassigned values from
    ##   the input that we just tried (i.e., concrete_values).
    ##   You can use the inherit() method in ConcreteValues for this.
    ##
    ## - Add the input to the queue for processing, along the lines of:
    ##
    ##     inputs.add(new_values, caller)
    ##
    ##   where caller is the corresponding value from the list of call
    ##   sites returned by concolic_find_input (i.e., branch_callers).

迭代 concolic_exec_input() 所返回的分支集合
使用 concolic_force_branch() 来构建一个分支的另一路径约束
若约束已经在 check 集合中，将其跳过，否则加入集合中
使用 concolic_find_input() 以构建一个基于另一路径约束的新的测试输入
Z3 可能不会为每个变量分配值（例如变量可能与约束无关），我们需要从上次使用的字典继承到 concolic_find_input() 返回的新字典中，将新的字典添加到 input 队列中

依照以上思路，笔者最后在大循环末尾补全代码如下：

    branch_len = len(branch_conds)
    # explore every branch
    for b in range(branch_len):
      # construct new constraint for negative branch
      cur_constraint = concolic_force_branch(b, branch_conds, branch_callers)
      # not in `checked` set, solve out the constraint
      if cur_constraint not in checked:
        checked.add(cur_constraint)
        sat, cur_concrete_values = concolic_find_input(cur_constraint, None)
        # satisfiable, add the dict for next round
        if sat:
          cur_concrete_values.inherit(concrete_values)
          inputs.add(cur_concrete_values, branch_callers[b])