【软件分析第13讲-学习笔记】符号执行 Symbolic Execution

前言

创作开始时间：2022年11月16日18:46:31

如题，学习一下符号执行 Symbolic Execution的相关知识。参考：熊英飞老师2018《软件分析》课件。

正文

符号执行

程序的规约通常表示为前条件和后条件。

形成命题：

1. 前条件->后条件
2. 命题成立=逆命题不可满足
3. 用SMT solver可求解

用符号执行发现：

• 缓冲区溢出
• 除零错
• 路径可行性

基于霍尔逻辑的符号执行

霍尔三元组：{前条件}语句{后条件}

霍尔逻辑表示三者之间的推导关系。又称为公理语义

霍尔逻辑规则：

• 空语句(Empty statement axiom schema)
• 赋值语句(Assignment axiom schema)
• 合成规则(Rule of composition)
• 条件规则(Conditional rule)
• 推导规则(Consequence rule)
• 循环规则(While rule)

可参考：

• 霍尔逻辑Hoare Logic https://blog.csdn.net/Campsisgrandiflora/article/details/111410348
  这篇博客讲的挺详细的。
  
  大概了解了这个证明过程。

谓词转换计算

最弱前条件计算：给定后条件和语句，求能形成霍尔三元组的最弱前条件
最强后条件计算：给定前条件和语句，求能形成霍尔三元组的最强后条件

基于谓词转换的符号执行：

• 给定输入需要满足的条件 P ，代码 c ，输出需要满足的条件Q
• 前向符号执行：基于P、c计算最强后条件Q’，验证Q’->Q
• 后向符号执行：基于Q、c计算最弱前条件P’，验证P->P’

最弱前置条件

参考：

• weakest-precondition https://www.cs.umd.edu/~mvz/handouts/weakest-precondition.pdf
• Weakest Precondition Calculus https://comp.anu.edu.au/courses/comp2600/Lectures/19wp1.pdf

Starting with a post-assertion, what is the weakest pre-condition that makes the assertion true?
In other words, what must be true before to make the assertion true after?

如果A->B，但是B不->A。那么B比A更弱。（相当于B包含了A）

赋值语句的示例：

还是比较好理解的。

更多的例子就不一一列出，可访问原参考链接。

动态符号执行

• 混合程序的真实执行和符号执行
• 在约束求解无法进行的时候，用真实值代替符号值
• 代表工作：Concolic Testing,Execution Generated Testing

看了下案例：

好处应该就是可以根据具体的状态（Concrete state）求解能够探索新路径的值。可以不断迭代，从而遍历所有路径。

符号执行：进一步探究

参考：

• Symbolic execution https://courses.cs.washington.edu/courses/cse403/16au/lectures/L16.pdf

符号执行可以生成一个具体的输入，使得程序出错（不符合规约）。但是不能证明程序没错。

用自动定理证明器（如SAT、SMT求解器）来求解是否存在使程序出错的具体输入值。

小结

大概明白了符号执行。后续再补充完善。

创作结束时间：2022年11月16日20:20:44

参考文献