基于懒替换的C符号执行

Lazy-substitution based symbolic execution for C programs

针对传统符号执行中的动态地址计算问题,提出了基于懒替换的符号执行方法.通过引入尽可能替换的策略,基于懒替换的符号执行在无法静态确定变量的地址或符号表达式过长时不做符号替换.首先给出了基于懒替换的符号执行算法,在此基础上,详细分析了C语言主要结构尤其是数组和指针的懒符号执行语义.LazySEC是一个面向C程序的懒符号执行系统原型,初步实验表明,它可以有效地处理含有指针和结构体等涉及动态地址计算的程序语言结构.

Lazy-substitution based symbolic execution was presented in order to address the computed memory location problem in traditional symbolic execution. A form of lazy strategy was introduced into traditional symbolic execution, which substitutes program variables with their symbolic values as much as possible. When the memory locations of variables in a statement can＇t be determined statically or the length of a symbolic expression for substitution is too long, those variables won＇t be replaced with their symbolic values. The lazy substitution algorithm was provided. Moreover, the lazy symbolic execution semantics for most of structures in C programming language were discussed in detail, especially for array and pointer. The prototype of symbolic execution system LazySEC （a lazy symbolic executor for C programs） performs lazy-substitution based symbolic execution for C programs. Preliminary experiment results show that LazySEC can handle program structures involving computed memory locations efficiently.