文章目录
前言
创作开始时间：2022年11月16日18:46:31
如题，学习一下符号执行 Symbolic Execution的相关知识。参考：熊英飞老师2018《软件分析》课件。
正文
符号执行
程序的规约通常表示为前条件和后条件。
形成命题：
- 前条件->后条件
- 命题成立=逆命题不可满足
- 用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