前言
这几天的学习将第五章符号执行给写完了，不过内容有点多，打算分两天的博客将学习的内容写完。
符号执行
符号执行基本模型
-
软件正确性测试原则：选择合适的测试用例对程序运行状态进行测试，如果对于提供的输入都能产生正常的结果输出，则认为程序是可靠的。
-
测试的方法：一种是以模糊测试为代表的随机性测试；另一种是以模型检测为代表的形式化证明方法。
-
符号执行的缘由：希望在无法获取程序特性说明等信息的情况下，仍旧能够对其进行快速全面的自动化安全性检测。
-
符号执行的基本思想：使用符号变量代替具体值作为程序或函数的参数，并模拟程序执行中的指令，各指令的操作都基于符号变量进行，其中操作数的值由符号和常量组成的表达式来表示。
-
程序语句类型：其中最重要的就是if条件语句，也可以扩展一点说成条件跳转语句。
简单的声明语句；
if条件语句；
无条件跳转语句；
变量操作语句
-
条件跳转语句中符号执行与具体执行的关键区别：符号变量的引入使得程序执行到路径分支时无法确定程序的走向。
-
路径约束条件pc（path constraint）:符号执行过程中对路径上条件分支走向的选择情况，根据状态中的pc变量就可以确定一次符号执行的完整路径。
假设ifn处的表达式为R》0，R是一个与符号变量相关的多项表达式，把R》0称为q，则程序执行到ifn处时pc可能会表现为下面两种形式之一。
（1）pc包含q；
（2）pc包含┐q。
如果符号执行引擎选择进入then分支，则R》0的真值为true，pc表现为（1）的形式；如果选择else分支，则R》0的真值为false，pc表现为2形式
在程序逻辑中，当执行到if条件语句处时，符号执行需要创建两个“并行”的执行过程：一个进入if语句的then分支，生成then分支对应的pc；另一个进入else分支，同样生成对应的pc。两个符号执行过程在if分支之后相互独立，同有各自的执行状态。
约束求解
-
约束求解问题可以形式化表示为一个三元组<V,D,C>，其中的3个要素分别为：变量V，变量的论域D和约束条件C。若Ci包含k个变量，则称Ci为在这k个变量集合上的k元约束。
-
约束求解就是找到约束问题的一个解，该解对变量集合中所有变量都赋一个取自其论域的值，并且这些变量的取值满足该问题所有的约束条件。
-
SAT问题（可满足性问题），是指求解由布尔变量集合所构成的布尔函数，是否存在变量的一种分布使得该函数的取值为1.
缺点：SAT求解只能解决命题逻辑公式问题，使得许多实际应用问题无法直接转换为SAT问题来求解。
- SMT（可满足性模理论）是在可满足性问题的基础上扩展而来的，它将SAT求解从只能解决命题逻辑公式扩展为可以解决一阶逻辑所表达的公式。。
Z3求解器
-
Z3求解器是一种SMT求解器，由微软研究院主持设计。
-
Z3求解器共包括5大模块构成
化简模块：Z3处理器首先会对表达式进行化简处理。
编译模块：将经过初步简化处理的表达式转换为特定的语法树和数据结构。
核心模块：调用理论求解器和SAT求解器处理经过编译的表达式，并实现了两个求解模块的数据共享。
理论求解模块：其中包含了SMT求解器常用的基本理论。
SAT求解模块：该模块使用的是经典SAT求解技术。
