HeyGap's_Blog

Be a positive learner

0%

Symbolic Execution Leaning Note (1) -- Basis

发表于 更新于 分类于
迈向自动化的第一步——

0x00 基本模型

  • 概述 
    1
    2
    3
    4
    5
    6
    1  void sum(a,b){
    2    int x = a;
    3    int y = b;
    4    int z = x + y;
    5    return z;
    6  }
    调用$sum(1,2)$，学过C语言的都知道会发生什么事情
    但如果我调用$sum(a1,a2)$，并且我在这之前并未声明a1，a2呢？
    先不要用C语言的思路来考虑了，我们称这种情况为符号执行(Symbolic Execution)，具体会发生什么我们接着往下看

  • 基本思想

    1. 使用符号变量代替具体值作为程序或函数的参数，并模拟执行程序中的指令，各指令的操作都基于符号变量进行，其中操作数的值由符号和常量组成的表达式来表示
      1. 符号变量是什么？
        1. 读者可以将符号执行视为程序具体执行的自然扩展，符号变量使得程序执行变得不确定，当我们给一系列符号赋一个确定的值时，符号执行就成为了程序具体执行（i.e. 程序的一次具体执行可以视为符号执行的一次实例）
      2. 操作数是什么？
    2. 对于任意程序，其执行流程是由执行序列的执行语义控制的
      1. 执行语义：
        1. 变量定义语句对数据对象的描述 int a;
        2. 声明语句对程序数据对象的修改 a = 10;
        3. 条件语句对程序执行流程的控制
    3. 当程序的输入参数确定时，其指令序列被固定，因此程序执行语义和控制流也被固定

  • 程序语言定义

    1. James C. King在提出符号执行技术的同时，也为其限定了理想的适用场景：
      1. 理想模型中程序只处理“有符号整数”
      2. 程序“执行数”规模有限
      3. 可以处理程序内所有if条件语句的约束表达式
    2. 基于符号执行技术的理想场景，对程序语言做如下定义
      1. 程序变量类型：只包含“有符号整数”
      2. 程序语句类型
        1. 简单声明语句，如a = 3
        2. if条件语句(包括then 和 else)
        3. 无条件跳转语句，如goto语句
        4. 变量操作语句：如read函数、基本整数运算操作（+、-、*）
      3. 程序语义
        1. 简单声明语句、无条件跳转语句和变量操作语句，只是将程序中的具体值替换为了符号
        2. 而if条件语句中，将具体值替换为了符号，所以我们无法判断if语句中的真值，就不能确定条件分支的走向，这是符号执行技术对程序执行语义的最大改变，也是符号执行与具体执行的关键区别

  • 程序执行状态

    • PC
      1. 为了解决“分支走向不确定”的问题，King为程序状态新添加了一个变量：路径约束条件 pc(path constraint)，在每个if条件语句处并没有实际决定程序执行哪个分支，这就需要符号执行引擎主动选择执行分支并记录整个执行过程，pc就辅助完成了这项工作
      2. Simply，pc就是符号执行过程中对路径上条件分支走向的选择情况
      3. 来看一段示例
        1
        2
        3
        if1: a1 >= 0
        if2: a1+2*a2 >= 0
        if3: a3>= 0
      4. 假设上述三个分支中选择了if1:true if2:true if3:false，pc表示为pc = (a1 >= 0 && a1+2*a2 >= 0 && ~(a3 >= 0))，由此可见，pc是一个bool表达式
    • 符号执行引擎
      • 当符号执行到 if(q) 时，pc 有可能包含q（1），也可能包含 ~q（2），如果符号执行引擎选择进入then分支，则 pc 表现为（1）的形式，如果符号执行引擎选择进入else分支， 则 pc 表现为（2）的形式
      • 而我们希望两条分支都被测试，所以符号执行引擎执行到if条件语句时，符号执行需要创建两个“并行”的执行过程
      • 每个和符号变量相关的if条件语句都会为pc贡献一个决定程序执行走向的表达式，最后要确定pc对应路径的程序输入参数，只需要用约束求解器对pc进行求解

  • 符号执行树

    1. 定义：用来描述程序执行路径的树形结构
    2. 内容：一个节点对应程序中的一条语句，还可以包含指令计数、PC、变量值等程序执行状态信息(没找到合适的图，就先放一张不带C代码的)

  • 约束求解

    1. 定义：
      1. 给定一个三元组,其中：
        1. V: 变量的有限集合
        2. D: 变量的论域，变量可能取值的有限集合
        3. C: 有限约束集合，某个约束关系$C_i$包含V中一个或多个变量，若$C_i$包含k个变量，则称其为在这k个变量集合上的k元约束
      2. 约束求解就是找到约束问题的一个解，该解对变量集合中所有变量都赋一个取自其论域的值，并且这些变量的值满足该问题的所有约束条件
      3. 对于约束问题$P = $，若P至少存在一个解，则称P为可满足的，否则称其为不可满足的
    2. 分类:
      1. SAT(The Satisfiability problem, 可满足性问题)
        1. 定义：求解由布尔变量集合所构成的布尔函数，是否存在变量的一种分布使得该函数的取值为1
        2. 缺陷：①只能解决命题逻辑公式问题，很多实际问题转化不成命题逻辑问题②必须用布尔变量来表示，将实际问题转化为布尔函数开销大，转换后的函数也极其复杂
      2. SMT(Satisfiability Modulo Theories, 可满足性模理论)
        1. 定义：将SAT只能求解命题逻辑公式问题扩展为可以解决一阶逻辑所表达的公式。包含多种理论。
          1. 什么是一阶逻辑

  • 回到开始的函数

1
2
3
4
5
6
1  void sum(a,b){
2    int x = a;
3    int y = b;
4    int z = x + y;
5    return z;
6  }

我们将其写为类PL/1语言

1
2
3
4
5
6
1  SUM: PROCEDURE(A,B);
2    X<-A;
3    Y<-B;
4    Z<-X+Y;
5    RETURN(Z);
6  END;

我们在调用$sum(1,2)$后，可以列一个表格来观察程序流

Line 5是return 3 (Katex不支持合并单元格，理解万岁)

我们在调用$sum(a1,a2)$后，就是把具体值换成了对应的符号

Line 5是return (a1+a2)

既然符号执行与具体值执行最大的区别是if条件语句，那么我们写一个带有if语句的程序来看一下

1
2
3
4
5
6
7
8
9
10
11
12
13
 1: POWER: PROCEDURE(X, Y);
 2:     Z = 1;
 3:     J = 1;
 4:
 5: LAB: IF Y >= J THEN
 6:         DO;
 7:             Z = Z * X;
 8:             J = J + 1;
 9:             GO TO LAB;
10:         END;
11:
12:     RETURN(Z);
13: END POWER;

这个函数转化为C就是

1
2
3
4
5
6
7
8
9
int power(int X, int Y) {
    int Z = 1;
    int J = 1;
    while (Y >= J) {
        Z *= X;
        J++;
    }
    return Z;
}

我们继续用表格的格式来看

前三行都很正常，直到第五行进行判断

  1. 处理判断语句 Y>=J 得到约束条件 a2>=1
  2. 生成两个分支的路径约束条件：
    • (a2>=1) $\subset$ true
    • ~(a2>=1) $\subset$ true
  3. 两个路径约束都可满足，分别对两个路径进行探索

对于分支: ~(a2>=1) $\subset$ true

然后马上在Line 12处得到(return 1 when a2<1)，探索完成

对于分支: (a2>=1) $\subset$ true

然后因为Line 9，程序会跳回第四行继续判断语句，会产生两个新的分支，就陷入了无限循环，这不是我们想要的。

可是循环在一个程序中经常出现，该怎么解决这一问题？我们接着往后看

0x01 动态符号执行技术(DSE)

  • 基本思想

    1. 以具体的数值作为输入，执行程序代码，在程序实际执行路径的基础上：
      1. 用符号执行技术对路径进行分析
      2. 提取路径的约束表达式
      3. 根据路径搜索策略(深度、广度)对约束表达式进行变形
      4. 求解变形后的表达式并生成新的测试用例
      5. 不断迭代上述过程，直到完全遍历程序的所有执行路径
    2. DSE的出现是为了解决静态SE①执行效率低②系统开销大③误报率高的问题

  • 实现细节(以函数为例)

    1. 场景：void func(int a,int b),调用func(X,Y)
    2. Step1: 生成一组随机输入，开始”实际执行”
    3. Step2: 同时符号引擎开始符号执行，按照“实际执行”的“执行路径”上的分支条件语句的“谓词”，搜集所有符号约束条件及其对应真值
    4. Step3: 根据收集到的符号约束条件，按照一定路径选择策略，构造出一条新的可行路径约束
      • 举个例子：深度优先策略
      • 如果pc = p1 ∩ p2 ∩ p3, 深度优先就是将最后一个谓词(对不起jo太郎😭离散没学好忘了这个p3叫啥了)取非，变为p1 ∩ p2 ∩ ~p3
    5. Step4: 使用约束求解器求解出新约束集合对应的具体输入
    6. Step5: 重复上述过程，直到遍历全部路径

  • DSE工具SAGE

    1. 原理粗略地过了一遍，大段大段的看不懂😭这里就不花时间总结了
    2. SAGE基于x86的机器码进行符号执行，原因如下：
      1. 屏蔽不同编程语言、编译器及编译平台对分析过程的影响，具有更强的复用性
      2. 忽略编译器”代码优化””代码混淆””基本块转换”等使代码语义发生变化的操作，有利于确定程序实际存在的漏洞
      3. 闭源分析yyds

  • 关键问题

    1. 外部函数调用
    2. 循环问题：路径爆炸

这一段也不仔细读了…用到再学

0x02 并行符号执行技术(PSE)

  • 基本思想
    1. 很多情况下符号执行引擎无法继续运行的原因是内存不足，所以我们希望通过计算集群可无穷扩展的内存空间和CPU来缓解路径爆炸问题
    2. 分布式…这我就先不看了

0x03 参考文献

1《软件安全分析与应用》

-------------文章就到这里啦！感谢您的阅读XD-------------