基于可满足性模理论求解器的程序路径验证方法

doi:10.11772/j.issn.1001-9081.2016.10.2806

计算机应用 ›› 2016, Vol. 36 ›› Issue (10): 2806-2810.DOI: 10.11772/j.issn.1001-9081.2016.10.2806

基于可满足性模理论求解器的程序路径验证方法

任胜兵, 吴斌, 张健威, 王志健

中南大学软件学院, 长沙 410005

收稿日期:2016-05-03 修回日期:2016-06-02 出版日期:2016-10-10 发布日期:2016-10-10
通讯作者: 任胜兵,E-mail:rsb@csu.edu.cn
作者简介:任胜兵(1969—),男,湖南岳阳人,副教授,博士,CCF会员,主要研究方向:软件工程、嵌入式系统、数字图像处理;吴斌(1991—),男,湖南岳阳人,硕士研究生,主要研究方向:嵌入式可信软件;张健威(1992—),男,内蒙古包头人,硕士研究生,主要研究方向:嵌入式可信软件;王志健(1992—),女,山东烟台人,硕士研究生,主要研究方向:嵌入式可信软件。
基金资助:
国家自然科学基金资助项目（61272151）；中南大学研究生自主探索创新项目（2016zzts374）。

Method of program path validation based on satisfiability modulo theory solver

REN Shengbing, WU Bin, ZHANG Jianwei, WANG Zhijian

School of Software, Central South University, Changsha Hunan 410005, China

Received:2016-05-03 Revised:2016-06-02 Online:2016-10-10 Published:2016-10-10
Supported by:
BackgroundThis work is partially supported by the National Natural Science Foundation of China (61272151), the Exploration and Innovation Project for Graduate Students of Central South University (2016zzts374).

摘要/Abstract

摘要： 针对程序中因存在路径条数过多或复杂循环路径而导致路径验证时的路径搜索空间过大，直接影响验证的效率和准确率的问题，提出一种基于可满足性模理论（SMT）求解器的程序路径验证方法。首先利用决策树的方法对复杂循环路径提取不变式，构造无循环控制流图（NLCFG）；然后通过基本路径法对控制流图（CFG）进行遍历，提取基本路径信息；最后利用SMT求解器作为约束求解器，将路径验证问题转化为约束求解问题来进行处理。与同样基于SMT求解器的路径验证工具CBMC和FSoft-SMT相比，该方法在对测试集程序的验证时间上比CBMC降低了25%以上，比FSoft-SMT降低了15%以上；在验证精度上，该方法有明显的提升。实验结果表明，方法可以有效解决路径搜索空间过大的问题，同时提高路径验证的效率和准确率。

关键词: 路径验证, 控制流图, 决策树, 基本路径, 可满足性模理论求解器

Abstract: In programs, the path search space is too large because there are too many paths or complicated cycle paths, which directly affect the efficiency and accuracy for path validation. To resolve the above problem, a new program path validation method based on the Satisfiability Modulo Theory (SMT) solver was proposed. Firstly, loop invariants were extracted from the complicated cycle paths by using the method of decision tree, then the No-Loop Control Flow Graph (NLCFG) was constructed. Secondly, the information for basic paths was extracted via traversing Control Flow Graph (CFG) by using basic path method. Finally, the problem of path validation was converted into the problem of constraint solving by using a SMT solver as a constraint solver. Compared with CBMC and FSoft-SMT which were also based on SMT solver, the proposed method reduced validation time on test programs by more than 25% and 15% respectively. As for verification accuracy, the proposed method had significantly improvement. Experimental results show that this method can efficiently resolve the problem with too large path search space, and improve the efficiency and accuracy of path validation.

Key words: path validation, Control Flow Graph (CFG), decision tree, basic path, Satisfiability Modulo Theory (SMT) solver

中图分类号:

TP311.5

任胜兵, 吴斌, 张健威, 王志健. 基于可满足性模理论求解器的程序路径验证方法[J]. 计算机应用, 2016, 36(10): 2806-2810.

REN Shengbing, WU Bin, ZHANG Jianwei, WANG Zhijian. Method of program path validation based on satisfiability modulo theory solver[J]. Journal of Computer Applications, 2016, 36(10): 2806-2810.

参考文献

[1] STAVNYCHA M, YIN H, RÖMER T. A large-scale survey on the effects of selected development practices on software correctness[C]//Proceedings of the 2015 International Conference on Software and SystemProcess. New York: ACM, 2015: 117-121.
[2] McDONALD J T, TRIGG T H, ROBERTS C E, et al. Security in agile development: pedagogic lessons from an undergraduate software engineering case study[C]//CSS 2015: Proceedings of the Second International Symposium on Cyber Security. Berlin: Springer, 2015: 127-141.
[3] D'SILVA V, KROENING D, WEISSENBACHER G. A survey of automated techniques for formal software verification[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2008, 27(7): 1165-1178.
[4] 郭曦, 王盼, 王建勇, 等.基于k近邻最弱前置条件的程序多路径验证方法[J]. 计算机学报, 2015, 33(11):2203-2214.(GUO X, WANG P, WANG J Y, et al. Program multiple execution paths verification based on k proximity weakest precondition[J]. Chinese Journal of Computers, 2015, 33(11):2203-2214.)
[5] YANG G, DWYER M B, ROTHERMEL G. Regression model checking[C]//ICSM 2009: Proceedings of the 2009 IEEE International Conference on Software Maintenance. Piscataway, NJ: IEEE, 2009: 115-124.
[6] HARRIS W R, SANKARANARAYANAN S, IVANCIC F, et al. Program analysis via satisfiability modulo path programs[C]//POPL 2010: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York: ACM, 2010: 71-82.
[7] MUDDULURU R, RAMANATHAN M K. Efficient incremental static analysis using path abstraction[M]//Fundamental Approaches to Software Engineering. Berlin: Springer, 2014: 125-139.
[8] HENRY J. Static analysis by path focusing[D]. Grenoble: Grenoble INP, 2011:15-41.
[9] 何炎祥, 吴伟, 陈勇, 等.基于SMT求解器的路径敏感程序验证[J]. 软件学报, 2012, 23(10):2655-2664.(HE Y X, WU W, CHEN Y, et al. Path sensitive program verification based on SMT solvers[J]. Journal of Software, 2012, 23(10):2655-2664.)
[10] GARG P, NEIDER D, MADHUSUDAN P, et al. Learning invariants using decision trees and implication counterexamples[C]//Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York: ACM, 2016: 499-512.
[11] FLOYD R W. Assigning meanings to programs[C]//Proceedings of Symposia in Applied Mathematics. Providence: American Mathematical Society, 1967:19-32.
[12] DIJKSTRA E W. A Discipline of Programming[M]. Englewood Cliffs: Prentice-hall, 1976:7-40.
[13] COUSOT P, COUSOT R, MAUBORGNE L. Theories, solvers and static analysis by abstract interpretation[J]. Journal of the ACM, 2012, 59(6): 31.
[14] KRISHNA S, PUHRSCH C, WIES T. Learning invariants using decision trees[EB/OL]. [2015-10-10]. http://arxiv.org/abs/1501.04725.
[15] SCHRÖDER M S, GUSENLEITNER D, QUACKENBUSH J, et al. RamiGO: an R/Bioconductor package providing an AmiGO visualize interface[J]. Bioinformatics, 2013, 29(5):666-668.
[16] 姜冶, 管仁初, 梁艳春.整合Dmoz和Yahoo标签的BNF文法及其实现[J]. 计算机工程与设计, 2009, 30(19):4520-4523.(JIANG Y, GUAN R C, LIANG Y C. BNF syntax unifying Dmoz and Yahoo syntax and its implementation[J]. Computer Engineering and Design, 2009, 30(19):4520-4523.)
[17] CADAR C, SEN K. Symbolic execution for software testing: three decades later[J]. Communications of the ACM, 2013, 56(2): 82-90.
[18] 季晓慧, 张健.约束问题求解[J]. 自动化学报, 2007, 33(2):125-131.(JI X H, ZHANG J. Constraint processing[J]. Acta Automatica Sinica, 2007, 33(2):125-131.)
[19] 康文涛.符号执行工具KLEE约束求解优化设计与实现[D]. 成都:电子科技大学, 2014:25-59.(KANG W T. Optimization of constraint solver for KLEE, a dynamic symbolic execution tool[D]. Chengdu: University of Electronic Science and Technology of China, 2014:25-59.)
[20] KROENING D, TAUTSCHNIG M. CBMC-C bounded model checker[M]//Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2014: 389-391.
[21] ARMANDO A, MANTOVANI J, PLATANIA L. Bounded model checking of software using SMT solvers instead of SAT solvers[J]. International Journal on Software Tools for Technology Transfer, 2009, 11(1):69-83.
[22] SNU real-time benchmarks[EB/OL]. [2015-10-10]. http://www.cprover.org/goto-cc/examples/snu.html.

基于可满足性模理论求解器的程序路径验证方法

Method of program path validation based on satisfiability modulo theory solver

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	王雅辉, 钱宇华, 刘郭庆. 基于模糊优势互补互信息的有序决策树算法[J]. 计算机应用, 2021, 41(10): 2785-2792.
[2]	周翔, 翟俊海, 黄雅婕, 申瑞彩, 侯璎真. 基于随机森林和投票机制的大数据样例选择算法[J]. 计算机应用, 2021, 41(1): 74-80.
[3]	赵一, 段兴, 谢仕义, 梁春林. 面向特定目标自识别的交通图像语义检索方法[J]. 计算机应用, 2020, 40(2): 553-560.
[4]	王伟, 谢耀滨, 尹青. 针对不平衡数据的决策树改进方法[J]. 计算机应用, 2019, 39(3): 623-628.
[5]	莫赞, 盖彦蓉, 樊冠龙. 基于GAN-AdaBoost-DT不平衡分类算法的信用卡欺诈分类[J]. 计算机应用, 2019, 39(2): 618-622.
[6]	郭冰楠, 吴广潮. 基于改进的代价敏感决策树的网络贷款分类[J]. 计算机应用, 2019, 39(10): 2888-2892.
[7]	颜宏文, 盛成功. 基于层次聚类和极限学习机的母线短期负荷预测[J]. 计算机应用, 2018, 38(8): 2437-2441.
[8]	折蓉蓉, 张丽萍, 侯敏, 闫盛. 基于决策树推荐克隆重构的方法[J]. 计算机应用, 2018, 38(7): 2037-2043.
[9]	徐光宪, 赵越, 赖俊宁. 基于网络编码的确定性逐层构造算法[J]. 计算机应用, 2018, 38(3): 769-775.
[10]	段大高, 盖新新, 韩忠明, 刘冰心. 基于梯度提升决策树的微博虚假消息检测[J]. 计算机应用, 2018, 38(2): 410-414.
[11]	黄宇扬, 董明刚, 敬超. 面向K最近邻分类的遗传实例选择算法[J]. 计算机应用, 2018, 38(11): 3112-3118.
[12]	王婷, 王祺, 黄越圻, 殷亦超, 高炬. 基于症状构成成分的上下位关系自动抽取方法[J]. 计算机应用, 2017, 37(10): 2999-3005.
[13]	陈环环, 陈小红, 阮彤, 高大启, 王昊奋. 知识驱动的游戏攻略自动标注算法[J]. 计算机应用, 2017, 37(1): 278-283.
[14]	丁要军. 基于改进的旋转森林算法的不平衡网络流量分类方法[J]. 计算机应用, 2015, 35(12): 3348-3351.
[15]	陈丽芳, 王云, 张奉. 粗决策树动态规则提取算法研究及应用[J]. 计算机应用, 2015, 35(11): 3222-3226.