软件安全分析与应用第5章符号执行读书笔记。

  • 符号执行
    • 基本模型
      • 程序语义
      • 符号执行树
    • 动态符号执行技术
      • SAGE
    • 并行符号执行技术
      • SCORE
      • Cloud9
      • SAGEN
    • 选择符号执行技术
    • 符号执行案例

基本模型

使用符号变量代替具体值作为程序或者函数的参数，并模拟执行程序中的指令，各指令的操作都基于符号变量进行，其中操作数的值由符号和常量组成的表达式来表示。

符号执行中的程序语义：

  1. 符号数据对象
  2. 程序语句（变量操作/跳转语句）
  3. 程序执行状态

符号执行树

执行树是用来描述程序执行路径的树形结构。执行树中的一个节点对应程序中的一条语句，程序语句之间的执行顺序或跳转关系对应执行树中节点间的边。

执行树具有以下特点：

  1. 每一个叶节点都有一组对应输入，使得程序执行到该逻辑分支
  2. 不存在两个叶节点存在相同的输入

约束求解

每个叶节点对应的执行路径可以由一组具体输入指导程序运行得到，这一组输入值可以借助约束求解值得到。
现在的主流约束求解器主要基于两种理论模型：

  1. SAT问题（求解由布尔变量集合所构成的布尔函数，检验是否存在变量的一种分布使得该函数的取值为1）
  2. SMT问题（在SAT基础上发展而来，将SAT求解只能解决命题逻辑公式拓展为可以解决一阶逻辑所表达的公式）

在大量的SMT求解器中，最出众的莫过于由微软研究院设计的 Z3 求解器。

动态符号执行技术

动态符号执行的执行过程分为以下步骤：

  1. 使用随机的具体值作为程序初始输入开始实际执行，同时对实际执行路径上的带吗进行符号执行，并从当前执行路径的分支条件语句的谓词中搜集所有符号约束条件机器对应的真值
  2. 根据收集到的符号约束条件，按照一定的路径选择策略，对其中的某个约束条件进行取反，构造新的可行的路径约束
  3. 使用约束求解器求解出新的约束集合对应的具体输入，接着使用符号执行引擎对新输入值进行新一轮的分析

分代搜索算法是 SAGE 的路径搜索算法，也是其技术核心。

并行符号执行技术

并行结束与符号执行技术结合，需要解决的关键问题：

  1. 分布式环境下的路径搜索策略
  2. 分布式环境下的负载均衡策略

选择符号执行

当测试程序执行到测试人员感兴趣的程序片段时，对代码进行符号执行分析，即对遇到的所有路径进行分析。对不感兴趣的外部调用函数，对代码进行大路径具体执行。