一种符号执行制导的循环内界分析方法

doi:10.3969/j.issn.0372-2112.2017.11.003

电子学报 ›› 2017, Vol. 45 ›› Issue (11): 2582-2592.DOI: 10.3969/j.issn.0372-2112.2017.11.003

一种符号执行制导的循环内界分析方法

赵祖威^1,2, 冯世宁^3,4, 汤恩义^1,2, 陈鑫¹, 李宣东^1,2, 潘敏学^1,2, 赵晨^1,2

1. 南京大学软件新技术国家重点实验室, 江苏南京 210023;
2. 南京大学软件学院, 江苏南京 210093;
3. 南瑞集团公司(国网电力科学研究院), 江苏南京 211106;
4. 国电南瑞科技股份有限公司, 江苏南京 211106

收稿日期:2016-07-25 修回日期:2016-12-16 出版日期:2017-11-25
- 通讯作者:
- 汤恩义
- 作者简介:
- 赵祖威,男,1992年10月出生,江苏南通人.2015年本科毕业于南京大学软件学院.现为南京大学软件学院硕士研究生,主要研究方向为静态程序分析,软件测试;冯世宁,女,1986年11月出生,江苏南京人.2008年、2011年分别在东南大学、国网电力科学研究院获学士、硕士学位.现为南瑞集团(国网电力科学研究院)工程师,从事系统仿真,电力电子自动化等领域的研究.
- 基金资助:
- 国家自然科学基金 (No.61402222，No.61632015）; 国家重点研发计划 (No.2016YFB1000802）; 教育部高等学校博士学科点专项科研基金 (No.20110091120058）; 江苏省产学研项目 (No.BY2014126-03）

A Symbolic Execution Guided Inner Loop Bound Analysis

ZHAO Zu-wei^1,2, FENG Shi-ning^3,4, TANG En-yi^1,2, CHEN Xin¹, LI Xuan-dong^1,2, PAN Min-xue^1,2, ZHAO Chen^1,2

1. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, Jiangsu 210023, China;
2. Software Institute, Nanjing University, Nanjing, Jiangsu 210093, China;
3. NARI Group Corporation(State Grid Electric Power Research Institute), Nanjing, Jiangsu 211106, China;
4. NARI Technology Co., Ltd., Nanjing, Jiangsu 211106

Received:2016-07-25 Revised:2016-12-16 Online:2017-11-25 Published:2017-11-25
- Supported by:
- National Natural Science Foundation of China (No.61402222, No.61632015); National Key Research and Development Program of China (No.2016YFB1000802); Research Fund for the Doctoral Program of Higher Education of Ministry of Education of China (No.20110091120058); Industry-University-research Project of Jiangsu Province (No.BY2014126-03)

摘要/Abstract

摘要： 循环是计算机中重要的复杂程序结构.很多应用场景要求静态分析循环可能达到的最大迭代次数，即循环边界（Loop Bound）.对应技术在文献中被称为循环边界分析（Loop Bound Analysis）.现有的循环边界分析均使用保守方式进行外界分析，即产生略高于循环边界的近似值.基于这一现状，本文提出了一种自动地循环内界分析方法，产生略低于循环边界的近似值.当用户综合利用外界与内界分析，能将循环边界值约束到一个统计区间，从而能对分析结果获得更为完整的认识.本文基于循环条件制导的符号执行（Symbolic Execution）技术实现了循环内界分析，该技术的本质在于它能够利用符号执行符号化推导程序执行约束的特点，准确求解循环在程序所有合法输入条件下的边界值，并由生成的测试用例来保证该边界值一定可达（即保证是循环内界）.本文对符号执行制导技术进行了优化，并在多组已有研究采用的基准用例集上进行了实例评估，实验结果表明，本文的循环内界分析方法具备准确性和高效性，可以满足应用需求.

关键词: 循环边界分析, 符号执行, 软件测试

Abstract: Loop is an important program structure in computer.Many applications need to estimate the maximum iteration number of loops in programs by loop bound analysis.Existing loop bound analysis uses conservative methods to derive outer loop bounds,which estimates the bounds higher than the real ones.In this paper,we propose an automatic inner bound analysis,which generates bounds slightly lower than the real ones.When users combine the inner bound analysis with traditional outer bound analysis,they can restrict every real loop bound in an interval and get more information about the loops.We implement the inner bound analysis by a scope-condition guided symbolic execution.The insight of our technique is that when symbolic execution substitutes program inputs by symbols in its derivation,it generates loop bounds for all valid inputs and generates corresponding test cases that make the inner bounds feasible.We optimize the technique and evaluate it on several benchmarks.The results show that the analysis is precise and efficient.

Key words: loop bound analysis, symbolic execution, software testing

中图分类号:

TP311.5

赵祖威, 冯世宁, 汤恩义, 等. 一种符号执行制导的循环内界分析方法[J]. 电子学报, 2017, 45(11): 2582-2592.

ZHAO Zu-wei, FENG Shi-ning, TANG En-yi, et al. A Symbolic Execution Guided Inner Loop Bound Analysis[J]. Acta Electronica Sinica, 2017, 45(11): 2582-2592.

参考文献

[1] Michiel M D,Bonenfant A,Casse H,et al.Static loop bound analysis of C programs based on flow analysis and abstract interpretation[A].Proceedings of the 14th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications[C].Taiwan:IEEE Computer Society,2008.161-166.
[2] Gustafsson J,Ermedahl A,Sandberg C,et al.Automatic derivation of loop bounds and infeasible paths for WCET analysis using abstract execution[A].Proceedings of the 27th IEEE International Real-Time Systems Symposium[C].Rio de Janeiro:IEEE,2006.57-66.
[3] Knoop J,Kovacs L,et al.Symbolic loop bound computation for WCET analysis[A].Proceedings of the 8th International Conference on Perspectives of System Informatics[C].Berlin:Springer Verlag,2011.227-242.
[4] Wilhelm R,Engblom J,Ermedahl A,et al.The worst-case execution-time problem-overview of methods and survey of tools[J].ACM Transactions in Embedded Computing Systems,2008,7(3):1-53.
[5] Cadar C,Godefroid P,Khurshid S,et al.Symbolic execution for software testing in practice[A].Proceedings of the 33rd International Conference on Software Engineering[C].New York:ACM,2011.1066-1071.
[6] King J C.Symbolic execution and program testing[J].Communications of the ACM,1976,19(7):385-394.
[7] Xiao X,Li S,Xie T,et al.Characteristic studies of loop problems for structural test generation via symbolic execution[A].Proceedings of the 28th International Conference on Automated Software Engineering[C].California,IEEE,2013.246-256.
[8] Anand S,Pǒsǒreanu C S,Visser W.JPF-SE:A symbolic execution extension to java path finder[A].Proceedings of the 13th International Conferrence on Tools and Algorithms for the Construction and Analysis of Systems[C].Berlin:Springer-Verlag,2007.134-138.
[9] Cadar C,Dunbar D,Engler D.KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs[A].Proceedings of the 8th USENIX Conference on Operating systems design and implementation[C].California:USENIX Association,2008.209-224.
[10] Boonstoppel P,Cadar C,Engler D.RWset:Attacking path explosion in constraint-based test generation[A].Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems[C].Berlin:Springer-Verlag,2008.351-366.
[11] Cadar C,Ganesh V,Pawlowski P M,et al.EXE:automatically generating inputs of death[A].Proceedings of the 13th ACM conference on Computer and communications security[C].New York:ACM,2006.322-335.
[12] Godefroid P,Levin M Y,Molnar D.Automated whitebox fuzz testing[A].Proceedings of the 16th Annual Network and Distributed System Security Symposium[C].California:Internet Society,2008.
[13] Majumdar R,Sen K.Hybrid concolic testing[A].Proceedings of the 29th International Conference on Software Engineering[C].Washington DC:IEEE Computer Society,2007.416-426.
[14] Xie T,Tillmann N,Halleux J D,et al.Fitness-guided path exploration in dynamic symbolic execution[A].Proceedings of IEEE/IFIP International Conference on Dependable Systems and Networks[C].Lisbon:IEEE,2009.359-368.
[15] Gustafsson J,Betts A,Ermedahl A,et al.The mälardalen WCET benchmarks:Past,present and future[A].Proceedings of the 10th International Workshop on Worst-Case Execution Time Analysis[C].Dagstuhl:Schloss Dagstuhl——Leibniz-Zentrum fuer Informatik,2010.136-146.
[16] Holsti N,Gustafsson J,Bernat G,et al.WCET 2008-Report from the Tool Challenge 2008-8th Intl.workshop on worst-case execution time (WCET) analysis[A].Proceedings of the 8th International Workshop on Worst-Case Execution Time Analysis[C].Dagstuhl:Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik,2008.1-23
[17] Pozo R,Miller B.SciMark:A numerical benchmark for Java and C/C++[J/OL].http://math.nist.gov/scimark2/,2004-03-31.
[18] Kuitunen J,Drolshagen G,Mcdonnell J,et al.DEBIE-first standard in-situ debris monitoring instrument[A].Proceedings of the Third European Conference on Space Debris[C].Netherlands:ESA Publications Division,2001.185-190.
[19] Quinlan D.ROSE:Compiler support for object-oriented frameworks[J].Parallel Processing Letters,2000,10(0):215-226.
[20] Prantl A,Knoop J,Schordan M,et al.Constraint solving for high-level WCET analysis[R].Udine:Computing Research Repository,2009.77-89.
[21] Healy C,Sjodin M,Rustagi V,et al.Supporting timing analysis by automatic bounding of loopIterations[J].Real-Time Systems,2000,18(2):129-156.
[22] Gulwani S,Mehra K K,Chilimbi T,et al.Speed:Precise and efficient static estimation of program computational complexity[A].Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages[C].New York:ACM,2009.127-139.
[23] Gulwani S,Zuleger F.The reachability-bound problem[A].Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation[C].New York:ACM,2010.292-304.
[24] Henzinger T A,Hottelier T,Kovács L.Valigator:A verification tool with bound and invariant generation[A].Proceedings of the 15th International Conference on Logic for Programming,Artificial Intelligence,and Reasoning[C].Berlin:Springer-Verlag,2008.333-342.
[25] Godefroid P.Compositional dynamic test generation[A].Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Aymposium on Principles of Programming Languages[C].New York:ACM,2007.47-54.
[26] Li Y,Su Z,Wang L,et al.Steering symbolic execution to less traveled paths[A].Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages and Applications[C].New York:ACM,2013.19-32.
[27] Godefroid P,Luchaup D.Automatic partial loop summarization in dynamic test generation[A].Proceedings of the 2011 International Symposium on Software Testing and Analysis[C].New York:ACM,2011.23-33.
[28] Saxena P,Poosankam P,Mccamant S,et al.Loop-extended symbolic execution on binary programs[A].Proceedings of the Eighteenth International Symposium on Software Testing and Analysis[C].New York:ACM,2009.225-236.
[29] Xie X,Liu Y,Le W,et al.S-looper:automatic summarization for multipath string loops[A].Proceedings of the 2015 International Symposium on Software Testing and Analysis[C].New York:ACM,2015.188-198.

一种符号执行制导的循环内界分析方法

A Symbolic Execution Guided Inner Loop Bound Analysis

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	李志博, 李清宝, 兰明敬, 孙剑帆. 基于镜像选择序优化的MART算法[J]. 电子学报, 2022, 50(2): 314-325.
[2]	张笑宇, 沈超, 蔺琛皓, 李前, 王骞, 李琦, 管晓宏. 面向机器学习模型安全的测试与修复[J]. 电子学报, 2022, 50(12): 2884-2918.
[3]	范书平, 张岩, 马宝英, 万里, 姚念民, 宋妍. 基于均衡优化理论的路径覆盖测试数据进化生成[J]. 电子学报, 2020, 48(7): 1303-1310.
[4]	汪孙律, 杨秋松, 李明树. 一种针对格式文件的符号执行优化方法[J]. 电子学报, 2020, 48(12): 2417-2424.
[5]	杨超, 郭云飞, 扈红超, 刘文彦, 霍树民, 王亚文. 基于符号执行的软件缓存侧信道脆弱性检测技术[J]. 电子学报, 2019, 47(6): 1194-1200.
[6]	郭曦, 王盼. 基于依赖条件重构的程序符号值分析方法[J]. 电子学报, 2019, 47(3): 630-635.
[7]	夏春艳, 张岩, 万里, 宋妍, 肖楠, 郭冰. 基于否定选择遗传算法的路径覆盖测试数据生成[J]. 电子学报, 2019, 47(12): 2630-2638.
[8]	巩敦卫, 秦备, 田甜. 基于语句重要度的变异测试对象选择方法[J]. 电子学报, 2017, 45(6): 1518-1522.
[9]	廖伟志. 基于路径自动分割的测试数据生成方法[J]. 电子学报, 2016, 44(9): 2254-2261.
[10]	徐超, 陈勇, 葛红美, 何炎祥. 基于符号执行的能耗错误检测方法[J]. 电子学报, 2016, 44(5): 1040-1050.
[11]	王红阳, 姜淑娟, 王兴亚, 鞠小林, 张艳梅. 基于子路径扩展的不可达路径检测方法[J]. 电子学报, 2015, 43(8): 1555-1560.
[12]	王志, 贾春福, 刘伟杰, 王晓初, 张海宁, 于晓旭, 陈喆. 一种抵抗符号执行的路径分支混淆技术[J]. 电子学报, 2015, 43(5): 870-878.
[13]	聂楚江, 刘海峰, 苏璞睿, 冯登国. 一种面向程序动态分析的循环摘要生成方法[J]. 电子学报, 2014, 42(6): 1110-1117.
[14]	万勇兵, 徐中伟, 梅萌. 一种符号化执行的实时系统一致性测试生成方法[J]. 电子学报, 2013, 41(11): 2276-2284.
[15]	张岩;巩敦卫. 基于搜索空间自动缩减的路径覆盖测试数据进化生成[J]. 电子学报, 2012, 40(5): 1011-1016.