Symbolic Execution

Lab3实现了在Python程序上的符号执行系统，将程序中的分支条件转化为约束求解的constraints，由约束求解器 Z3 solver 进行求解，进而获得程序的执行输入（测试输入），使得程序能沿着特定的分支路线执行，从而发现程序中的Bug。

Z3的基本使用

Exercise 1

使用位运算计算无符号数、有符号数的平均值。限制条件是不能使用超过32位的变量。实现的结果正确与否使用Z3进行判断。测试条件是e = (avg != real_avg)。如果Z3找到了能使测试条件满足（sat）的输入，那么就说明求平均数的实现有错误，即找到了可以复现错误的例子。

两个无符号数的平均数

使用逻辑右移来完成

## Use z3.LShR(x, y) for unsigned (logical) right shift of x by y bits.
u_avg = z3.LShR(a, 1) + z3.LShR(b, 1) + (a & b & 1)  # 看看两个数的最后一位二进制是不是都是1

两个有符号数的平均数

参考 Hacker's Delight

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

Concolic execution for integers

为了实现混合执行，对整数的操作要有记录，fuzzy.py中提供了语法树节点的定义，每次对于整数的操作都会记录成一个操作节点，记录符号值与真实值，便于之后的 concolic execution.

Exercise 2

实现concolic_int的整数乘除法操作，以及语法树上的操作 concolic_int 有两个成员变量，一个是变量的真实值，一个是符号值第一步要实现符号值的乘法,返回符号表示的乘法

class sym_mult(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)

第二步计算乘法的真实值

class concolic_int(int):
  # ...
  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)
  
  def __mul__(self, o):
    if isinstance(o, concolic_int):
      res = self.__v * o.__v
    else:
      res = self.__v * o
    return concolic_int(sym_mult(ast(self), ast(o)), res)

Exercise 3

理解 check-symex-int.py，为了找到一个函数f(x)的输入，使得函数返回1234，比较迷惑人的是test_f中的操作，先使用fuzzy生成了一个全局的int 符号变量并赋值为1，但是这个操作其实发生在 fuzzy.concolic_exec_input 的顺序如下，

concrete_values.mk_global()
v = testfunc()  # testfunc中的mk_int的操作会检查global变量中是否有重名的，如果有，就不再覆盖了

直接用concrete_values中的值来覆盖了原来设定的变量值，即使testfunc中有设定变量值的操作，如果该全局变量已经存在，则直接返回(fuzzy.ConcreteValues.mk_int)。

所以解答中，直接调用ConcreteValues.add 即可设定 'i' 的值:

# symex_exercises.py
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', 7 * 123)
  return concrete_values

Exercise 4

调用z3的solver (wrapped by fork_and_check, timeout版本的solver)，寻找满足constraint的变量的values

def concolic_find_input(constraint, ok_names, verbose=0):
  (ok, model) = fork_and_check(constraint)
  if ok == z3.sat:
    concrete_values = ConcreteValues()
    for (k, v) in model.items():
      if k in ok_names:
        concrete_values.add(k, v)
    return True, concrete_values
  return False, ConcreteValues()

Exercise 5

实现concolic_force_branch，将条件语句中的第b个条件置反，返回新的constraint (用sym_and连接)。注意第b个条件的后面的条件就不用设置了，因为只关注于能否走到b个条件的指定分支。

def concolic_force_branch(b, branch_conds, branch_callers, verbose = 1):
  constraint = None
  temp = branch_conds[:b]  # 只取前b-1个条件
  constraint = sym_and(*temp,sym_not(branch_conds[b]))

  # 这是我原来的实现，但是发现
  # if b < len(branch_callers) and b >= 0:
  #   new_conds = []
  #   for (i, cond) in enumerate(branch_conds):
  #     if i == b:
  #       new_conds.append(sym_not(cond))
  #     else:
  #       new_conds.append(cond)
  #   constraint = sym_and(*new_conds)

  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 6

实现concolic_execs，混合执行符号化输入的待测函数关键函数的作用：

concolic_exec_input: 使用具体的values来执行被测函数，返回执行结果
concolic_find_input: 约束求解，返回满足约束的变量值
concolic_force_branch: 强制执行条件语句，返回约束

找到函数的所有执行可能的路径，返回函数的所有可能返回值

concolic_bool每次都会把遇到的条件加入到全局的global_constraint，作为当前执行路径下的条件约束集合

问题：怎么确定初始的concrete_values？发现check-symes-int中的test_f已经把i注册到全局的concrete_values中了

InputQueue 保存待运行的值

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)

    # my implementation
    for i in range(0, len(branch_conds)):  # iterate through every condition
      and_constr = sym_and(*branch_conds[:i+1])
      if and_constr in checked:
        continue
      checked.add(and_constr)
      (ok , vals) = concolic_find_input(and_constr, concrete_values.var_names(), verbose)
      if ok:
        # vals.inherit(concrete_values)
        inputs.add(vals, branch_callers[i])
        concrete_values.inherit(vals)

      neg_constr = concolic_force_branch(i, branch_conds, branch_callers, verbose) # force branch
      checked.add(neg_constr)
      (ok, vals) = concolic_find_input(neg_constr, concrete_values.var_names(), verbose)
      if ok:
        # vals.inherit(concrete_values) # inherit from base concrete_values
        inputs.add(vals, branch_callers[i])  # add to inputs
        concrete_values.inherit(vals)
      
    # my old implementation, forget the positive branches condition
    # for i in range(0, len(branch_conds)):  # iterate through every condition
    #   constr = concolic_force_branch(i, branch_conds, branch_callers, verbose) # force branch
    #   if constr in checked:
    #     continue
    #   checked.add(constr)
    #   (ok, vals) = concolic_find_input(constr, list(concrete_values.var_names()), verbose)
    #   if ok:
    #     vals.inherit(concrete_values) # inherit from base concrete_values
    #     inputs.add(vals, branch_callers[i])  # add to inputs
    #   else:
    #     if verbose > 0:
    #       print('canot find the proper constraint')

  if verbose > 0:
    print('Stopping after', iter, 'iterations')

  return outs

Concolic execution for strings

Exercise 7

实现 __len__ 和__contains__，注意要返回concolic的wrapper

class concolic_str(str):
  # ...
  def __len__(self):
    return concolic_int(sym_length(ast(self)), len(self.__v))

  def __contains__(self, item):
    if isinstance(item, concolic_str):
      res = item.__v in self.__v
    else:
      res = item in self.__v
    return concolic_bool(sym_contains(ast(self), ast(item)), res)

但是发现 check_symex-str.py不能找到 len(s) > 30的输入

Exercise 8

包装sqlalchemy.orm.query.Query.get函数，new_get函数接受的primary_key参数是符号执行的concolic_value

问题： row = query.get(primary_key.__v) # todo: cannot access the private field

解决： select *，再来跟concolic_str比较判断选取的row是否包含要查询的primarykey，通过比较==运算符比较concolic_str，进而构造constraints

def newget(query, primary_key):
  rows = query.all()
  for row in rows:
    pk_name = row.__table__.primary_key.columns.keys()[0]
    if getattr(row, pk_name) == primary_key:
      return row
  return None

Concolic execution for zoobars

Exercise 9

invariant checks

zoobars代表了转账的金额

mismatch找到了，从数据库中query，计算完成response后的余额总和

  balance2 = sum([p.zoobars for p in pdb.query(zoobar.zoodb.Person).all()])
  if balance1 != balance2:
    report_balance_mismatch()

查看每个用户的最终账户余额是否和交易记录一致

  # ...
  # record the initial balances of each user
  balances ={}
  for p in pdb.query(zoobar.zoodb.Person).all():
      balances[p.username]=p.zoobars

  environ = {}
  # ...

# 在Transfer表中查找是否存在sender
  final_balances = balances.copy()
  for t in tdb.query(zoobar.zoodb.Transfer).all():
    final_balances[t.sender] -= t.amount
    final_balances[t.recipient] += t.amount

  for p in pdb.query(zoobar.zoodb.Person).all():
    balances[p.username] = p.zoobars

  for k, v in final_balances.items():
    if v != balances[k]:
      report_zoobar_theft()

Exercise 10

判断了recipient是否为空之后，只会出现theft了

增加判断 sender 是否和 recipient是同一个人

if recipientp.username == senderp.username:
        raise ValueError()

todo:发现bob的balance没有变过

Sugar's Blog