计算机科学 ›› 2017, Vol. 44 ›› Issue (2): 209-215.doi: 10.11896/j.issn.1002-137X.2017.02.034

• 软件与数据库技术 • 上一篇    下一篇

形状分析符号执行引擎中的状态合并

邓维,李兆鹏   

  1. 中国科学技术大学计算机科学技术学院 合肥230026 中国科学技术大学先进技术研究院中国科大-国创高可信软件工程中心 合肥230027,中国科学技术大学计算机科学技术学院 合肥230026 中国科学技术大学先进技术研究院中国科大-国创高可信软件工程中心 合肥230027
  • 出版日期:2018-11-13 发布日期:2018-11-13
  • 基金资助:
    本文受国家自然科学基金项目(61229201,8,91318301)资助

State Merging for Symbolic Execution Engine with Shape Analysis

DENG Wei and LI Zhao-peng   

  • Online:2018-11-13 Published:2018-11-13

摘要: 符号执行技术以其良好的精确度控制和代码覆盖率被广泛应用于静态程序分析和高覆盖率测试用例自动生成。 符号执行 在分析程序时,以模拟真实的程序执行过程的方式分析程序的数据流和控制流信息,并检查程序可能出现的所有状态,得到程序的分析结果。高精确度和高覆盖率要求对程序状态描述具体而完备,这会导致符号执行过程中常见的状态爆炸问题。首先提出在不同的执行路径上对具体内存状态进行合并的算法,然后对内存模型进行适度的抽象,扩大状态合并算法的适用范围,最后讨论状态合并所带来的实际效果,并提出了状态合并的优化解决方案。所提出的算法在符号执行引擎ShapeChecker上实现,并取得了良好的实验结果。

关键词: 符号执行,状态合并,求解代价,内存模型,状态抽象

Abstract: Symbolic execution is widely used in static code analysis and automatic test generation for its well controlled precision and code coverage.When applied to analyze a program,symbolic execution traversals all possible states by simulating the execution of the program to analyze the data-flow and control-flow information and get results.High precision and coverage request detailed and complete description of program states,which will lead to the path-explosion problem in almost all implementations of symbolic execution.State merging is an effective way to solve the path-explosion problem.We firstly proposed an algorithm for the merging of states from different paths,then abstracted the states in a proper way to expand the application scope of the algorithm.Finally,we discussed the actual effect of state merging and put forward an optimization scheme.The whole algorithm is deployed in ShapeChecker,which is our symbolic execution tool,and experiments show good results in performance.

Key words: Symbolic execution,State merging,Query cost,Memory model,State abstraction

[3] ZHU L ,LI Z P,LIANG J B,et al.A Specification Language for Precise Shape Analysis of C Program[J].Journal of Chinese Mini-Micro Computer Systems,2016,7(4):653-658.(in Chinese) 朱玲,李兆鹏,梁家彪,等.C程序精确形状分析中的规范语言设计[J].小型微型计算机系统,2016,7(4):653-658.
[4] SOOS M.SMT Competition’14 and STP.http://www.msoos.org/2014/06/smt-competition14-and-stp.
[5] LLVM I R.LLVM Language Reference Manual.http://llvm.org/docs/LangRef.html.
[6] BAUDIN P,CUOQ P,FILLARTE J C,et al.ACSL:ACSL/ISO C Specification Language(Version 1.7)[Z].2009-2013 .
[7] ShapeChecker.http://kyhcs.ustcsz.edu.cn/~shapechecker.
[10] CADAR C,DUNBAR D,ENGLER D.KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs[C]∥Usenix Symposium on Operating Systems Design & Implementation.2008:208-224 .
[11] HOARE C A R.An Axiomatic Basis for Computer Programming[J].Communications of the ACM,1969,12(10):576-580.
[12] Clang Static Analyzer.http://clang-analyzer.llvm.org.
[13] XU Z X,KREMENEK T,ZHANG J.A Memory Model forStatic Analysis of C Programs[C]∥Proceeding of the 4th International Conference on Leveraging Applications of Formal Methods,Verification and Validation.2010.
[14] Coverity.https://coverity.com.
[15] PALIKAREVA H,CADAR C.Multi-solver Support in Symbo-lic Execution[M]∥Computer Aided Verification:Lecture Notes in Computer Science,2013:53-68
[16] CIFUENTES C,SCHOLZ B.Parfait:Designing a Scalable Bug Checker[C]∥IEEE International Working Conference on Source Code Analysis & Manipulation.2008:4-11.

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!