为什么需要符号执行：

符号执行基本模型

符号执行的基本思想

符号模型的执行语义

1、符号数据对象：

2、程序语句：

程序执行状态

路径约束条件pc

约束求解：

符号执行实例：

动态符号执行：

动态符号执行的基本思想

动态符号执行的执行过程

并行符号执行技术

如何有效避免各节点对程序执行路径的重复搜索是并行系统需要解决的首要问题。

分布式环境下的负载均衡策略

选择符号执行技术

选择符号执行技术的基本思想

具体执行至符号执行的转换

符号执行到具体执行的转换

为什么需要符号执行：

20世纪70年代软件正确性测试方法主要分为两类：
以模糊测试为代表的随机性测试方法
但其具有的盲目性和随机性使其无法提供完整可靠的测试结果。
以模型检测为代表的形式化证明方法
通过归纳法来证明程序是否具有期望的性质，但证明过程的复杂性使其在面对大规模程序时几乎不可用。

在此背景下，1976年Jame C. King提出了符号执行技术，可以将其看作是上述两种方法的折中。
King希望在无法获取程序特性说明等信息的情况下，仍然能够对其进行快速全面的自动化安全性检测。

符号执行基本模型

符号执行的基本思想

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

对于任意程序，其执行流程是由指令序列的执行语义控制的。
执行语义包括：
变量定义语句对数据对象的描述；
声明语句对程序数据对象的修改；
条件语句对程序执行流程的控制。
当程序的输入参数确定时，其指令序列也被固定下来，因此，程序执行语义和控制流也得到确定。
若不使用具体数值，而是用符号值作为程序的输入参数，则指令序列的操作对象就从具体数值变为符号值，相应地，程序的执行语义和控制流也变成与符号变量相关的符号表达式。

符号执行可以视为程序具体执行的自然扩展
符号变量使得程序执行语义变得不确定，也使得符号执行技术在理想情况下可以遍历程序执行树的所有路径。
同时，程序的一次具体执行也可以视为符号执行的一个实例
当需要对某条程序路径进行遍历分析时，只需要根据符号执行方法对该路径的分析结果，即可引导控制流遍历该路径的程序输入。

符号模型的执行语义

虽然程序语义因为符号变量的加入而发生变化，但无论是程序语法还是程序语句的操作流程均不会因为符号变量的存在而发生变化，从而保证了符号执行技术的有效性。
程序执行语义在符号执行模式下会发生变化，主要涉及
1、符号数据对象
2、程序语句
3、程序执行状态

1、符号数据对象：

为了简化描述，假设每次程序需要新的输入时，均从符号列表{a1, a2, a3, …}中选取。
程序输入参数中的符号变量通过变量声明、数学运算操作等方式传递至程序中的变量。
在理想模型中，程序使用的每个符号变量均应该是一个有符号整数。

2、程序语句：

程序语句中有如下几类语句：
变量操作语句：
数学运算符数据读写操作；
无条件跳转语句；
声明语句及条件跳转语句；

数学运算符：

程序具体执行时，数学运算操作可以描述成操作符、圆括号和整数变量构成的多项式表达式。
例如，a = 1 + (2 * 4)。
符号执行模式下同样可以进行类似的描述，只需要将表达式中的整数替换成符号值集合即可。
例如，a = a1 + (a2 * a3)。
可见，符号值的引入并未修改数学运算符的操作语义，仅将运算结果由整数多项式变成了符号多项式。

数据读写操作

以读操作read(addr)为例，
当addr中的值为具体值时，read(addr)返回具体值；
若addr中的值为符号值，则返回符号值。
可见，符号执行并没有影响读写操作的语义。

无条件跳转语句

goto语句称为无条件跳转语句，其一般格式为
goto 语句标号
其中，语句标号是按照程序标识符规范书写的符号，放在某一语句行前面，标号后需要添加冒号(:)，起到标识语句的作用，与goto语句配合使用。
语句标号为loop的示例
goto loop:
……
loop: while (x < 7);
符号执行模式中，goto语句与具体执行中的语义是完全一致的。

声明语句及条件跳转语句

具体执行时，无论是条件跳转语句还是声明语句，语句内表达式的取值均是具体值。
例如，if (a < 0)，表达式a < 0的真值在语句执行完成后即可计算得到，由于a的取值是已知的，因而可以根据真值决定条件分支的跳转。
符号执行时，if语句的语义没有变化，同样是根据a < 0的计算结果进行跳转，但此时a为符号变量，无法计算出a < 0的真值，因而改变了程序的执行语义。
因此，符号执行与具体执行的关键区别在于：
符号变量的引入使得程序执行到路径分支时无法确定程序的走向。

程序执行状态

具体执行时，程序状态中通常包括程序变量的具体值、程序指令计数等描述信息，使用这些信息即可描述程序执行的控制流向。
符号执行时，因为符号变量的引入导致分支走向不确定，仅凭原有的信息已经无法完整描述符号执行的状态。
因此，King为程序状态增加了变量：
路径约束条件，以pc(path constraint)表示。

路径约束条件pc

简单地说，pc是符号执行过程中对路径上条件分支走向的选择情况，根据状态中的pc变量即可确定一次符号执行的完整路径。
在符号执行过程中，在每个if条件语句处没有实际值决定程序执行哪条分支，从而需要符号执行引擎主动选择执行分支并记录整个执行过程，pc可以辅助完成该项工作。
例如，假设符号执行过程中经过3个与符号变量相关的if条件语句if1、if2和if3，每个条件语句处的表达式如下所示：
if1: a1 ≥ 0
if2: a1 + 2 * a2 ≥ 0
if3: a3 ≥ 0
假设引擎在3个if条件分支处分别选择的是if1: true，if2: true，if3: false，则pc表示为
pc=(a_1≥0∧a_1+2∗a_2≥0∧¬(a_3≥0))

pc是一个bool表达式，由符号执行路径上涉及的if条件语句中的表达式及表达式的真值选择拼接而成。

pc的初始值为true。

当选择then分支时，假设输入变量是满足q的，该过程可以描述为pc=pc∧q。

类似地，当选择else分支时，该过程可以描述为
pc=pc∧¬q。

由于根据pc的内容即可确定一条唯一的程序执行路径，因而，pc被称为条件路径

约束求解：

符号执行过程中，执行树中每个叶节点对应的pc会被输入约束求解器进行求解。
若pc表达式有解，则求解器会输出满足pc的一组符号变量的具体值；
若pc表达式无解，则说明该叶节点对应的执行路径是不可达的。

约束求解问题可以形式化表示为一个三元组<V, D, C>，
其中变量V是变量的有限集合，表示为V = {v1, v2, …, vn}；
变量的论域D是变量可能取值的有限集合，变量vi只能在其论域Di中取值；
约束C是一个有限约束集合，某个约束关系Ci包含V中一个或多个变量，若Ci包含k个变量，则称Ci为在这k个变量集合上的k元约束。

约束求解就是找到约束问题的一个解，该解对变量集合中所有变量都赋一个取自其论域的值，且这些变量的取值满足该问题所有的约束条件。

符号执行实例：

用类PL/1语言的语法编写的计算三数之和的代码。
1: SUM: PROCEDURE(A, B, C);
2: X ← A + B;
3: Y ← B + C;
4: Z ← X + Y – B;
5: RETURN(Z);
6: END

SUM函数在具体执行过程中各变量的变化

函数的初始输入为1，3，5，程序输出为9。

在符号执行过程中，以A、B、C代表3个整数时各变量的变化

语句1是函数的入口，符号执行引擎将三个输入参数符号化为

符号执行（静态执行、动态执行、并行执行、选择执行相关推荐

Linux之bash脚本编程---选择执行
编程风格过程式编程,目的解决问题指令组织数据,指令的堆砌为了完成复杂的任务顺序执行:遍历的方式执行,逐个运行选择执行:有一种选择标准,结果只能有一种选择,只执行某些代码片段循环执行:对一 ...
浅析php-fpm静态和动态执行方式的比较
这篇文章主要介绍了php-fpm静态和动态执行方式的比较,较为详细的分析了php-fpm静态和动态执行方式的原理.参数功能与相关使用技巧,需要的朋友可以参考下本文实例讲述了php-fpm静态和动态执 ...
X86汇编语言从实模式到保护模式13：保护模式程序的动态加载和执行
目录 1. 引入保护模式对程序加载与执行的影响 1.1 对应用程序的影响 1.2 对操作系统的影响 1.3 本章程序总体结构 2. MBR加载内核过程分析 2.1 内核头部段分析 2.1.1 内核总长 ...
存储过程中执行动态Sql语句
MSSQL为我们提供了两种动态执行SQL语句的命令,分别是EXEC和sp_executesql;通常,sp_executesql则更具有优势,它提供了输入输出接口,而EXEC没有.还有一个最大的好处就 ...
【转】Oracle 执行动态语句
1．静态SQLSQL与动态SQL Oracle编译PL/SQL程序块分为两个种:其一为前期联编(early binding),即SQL语句在程序编译期间就已经确定,大多数的编译情况属于这种类型:另外一 ...
mysql存储过参数拼接_mysql 存储过程动态拼接sql并执行赋值
CREATE DEFINER = CURRENT_USER PROCEDURE `NewProc`(in _xnb varchar(50)) BEGIN ## 定义变量 DECLARE _num FL ...
SQL Server-聚焦sp_executesql执行动态SQL查询性能真的比exec好？
前言之前我们已经讨论过动态SQL查询呢?这里为何再来探讨一番呢?因为其中还是存在一定问题,如标题所言,很多面试题也好或者有些博客也好都在说在执行动态SQL查询时sp_executesql的性能比ex ...
oracle中执行动态sql语句吗,oracle中有没有可动态执行sql语句的函数
oracle中有没有可动态执行sql语句的函数关注:233 答案:2 手机版解决时间 2021-03-05 15:53 提问者祗剩寂寞 2021-03-04 22:38 oracle中有没有可 ...
程序实现switch语句判断年龄_【回顾】（选择执行语句if else和switch）乐创DIY C语言讲义——3.8节（4）...
文 | Edward 4 选择执行语句有些时候,我们希望程序既不顺序执行,也不只做单一的判断(代码运行还是不运行),很多时候,我们往往只希望对某一个条件的不同状态分别执行不同的语句,这样就 ...

符号执行（静态执行、动态执行、并行执行、选择执行

为什么需要符号执行：

符号执行基本模型

符号执行的基本思想

符号模型的执行语义

1、符号数据对象：

2、程序语句：

程序执行状态

路径约束条件pc

约束求解：

符号执行实例：

符号执行（静态执行、动态执行、并行执行、选择执行相关推荐

最新文章

热门文章