文章目录
前言
创作开始时间: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