8.Symbolic&Concolic Execution
约 196 个字 13 张图片 预计阅读时间 1 分钟
Symbolic execution¶
概述¶
最后生成符号化的表达式，而不一定是具体的值。
path condition：就是表达式的约束条件
应用：
-
将结果表达出来之后，我们可以生成所有情况的test case，这样在测试的时候可以覆盖所有的路径。
-
可以知道哪些路径是不可达的。
- 还可以去作变量之间的依赖关系的识别。
问题：
- 对每条路径都要记录路径约束，开销很大。
- 随着路径越来越深，符号表达式和路径约束都会越来越复杂。
挑战¶
-
Path explosion路径爆炸
-
Modeling program statements程序运行环境的建模
- Constraint solving
Challenge 1: Path Explosion¶
Challenge 2: Complex Code and Environment Dependencies¶
Challenge 3: Constraint Solving - SAT¶
约束求解
KLEE¶
没听……
本文总阅读量次