北京航空航天大学学报 ›› 2009, Vol. 35 ›› Issue (6): 687-691.

• 论文 • 上一篇    下一篇

基于懒替换的C符号执行

林梦香1, 陈胤立1, 陈 睿1, 周 刚2   

  1. 1. 北京航空航天大学 软件开发环境国家重点实验室, 北京 100191;
    2. 国家数据交换系统工程技术研究中心, 郑州 450002
  • 收稿日期:2008-05-05 出版日期:2009-06-30 发布日期:2010-09-16
  • 作者简介:林梦香(1968-),女,江苏苏州人,博士生,mxlin@nlsde.buaa.edu.cn.
  • 基金资助:

    国家863计划资助项目(2007AA010301)

Lazy-substitution based symbolic execution for C programs

Lin Mengxiang1, Chen Yinli1, Chen Rui1, Zhou Gang2   

  1. 1. State Key Lab. of Software Development Environment, Beijing University of Aeronautics and Astronautics, Beijing 100191,China;
    2. National Digital Switching Engineering and Technological Research Center, Zhengzhou 450002, China
  • Received:2008-05-05 Online:2009-06-30 Published:2010-09-16

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

Abstract: 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.

中图分类号: 


版权所有 © 《北京航空航天大学学报》编辑部
通讯地址:北京市海淀区学院路37号 北京航空航天大学学报编辑部 邮编:100191 E-mail:jbuaa@buaa.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发