基于程序局部性引导的有界模型检测优化方法

doi:10.11959/j.issn.1000-436x.2018050

通信学报 ›› 2018, Vol. 39 ›› Issue (3): 181-190.doi: 10.11959/j.issn.1000-436x.2018050

基于程序局部性引导的有界模型检测优化方法

王舜,杜晔,韩臻,刘吉强

北京交通大学智能交通数据安全与隐私保护技术北京市重点实验室，北京 100044

修回日期:2018-01-11 出版日期:2018-03-01 发布日期:2018-04-02
作者简介:王舜（1988-），男，陕西西安人，北京交通大学博士生，主要研究方向为形式化方法、程序分析技术、信息安全等。|杜晔（1978-），男，黑龙江哈尔滨人，博士，北京交通大学副教授、博士生导师，主要研究方向为网络安全、态势感知、软件可靠性分析与评估等。|韩臻（1962-），男，浙江宁波人，北京交通大学教授、博士生导师，主要研究方向为可信计算、系统安全、保密技术等。|刘吉强（1973-），男，山东海阳人，北京交通大学教授、博士生导师，主要研究方向为密码学、可信计算、隐私保护技术等。
基金资助:
北京高校青年英才计划基金资助项目(YETP0548);国家自然科学基金资助项目(61672092)

Locality-guided based optimization method for bounded model checker

Shun WANG,Ye DU,Zhen HAN,Jiqiang LIU

Beijing Key Laboratory of Security and Privacy in Intelligent Transportation,Beijing Jiaotong University,Beijing 100044,China

Revised:2018-01-11 Online:2018-03-01 Published:2018-04-02
Supported by:
Beijing Higher Education Young Elite Teacher Project(YETP0548)

摘要/Abstract

摘要：

基于多种模型检测方法组合的复合检测方式是当前软件模型检测领域开展研究的热点之一。在当前的研究中，提高检测的规模和检测的对象复杂程度的关键在于如何有效处理抽象的扩张和收缩。证明通过对程序模式或验证信息的利用可以加快状态空间的探索速度。面向有界模型检测（BMC）加速方法展开研究，使用程序中额外的信息和知识对其处理以协助检测器删除冗余和无效的状态。在对程序局部性进行定义的基础上，对其加速性进行讨论，提出一种加速有界检测的方法和一种改进策略，对算法进行了详细描述，并通过实验验证了方法在检测效率和性能上的优越性。

关键词: 模型检测, BMC, 软件检测, 局部性, 优化

Abstract:

For software model checking,approaches that combine with different kind of verification methods are now under research.The key to improve scale and complexity of verifiable software is handling the method for abstraction widening and strengthening wisely and precisely.To archive that,using extra knowledge that extracted from programming pattern or learned through verifying procedure to help eliminate the redundant state has been proved effective.Definition of program locality was given.It took the important role in accelerating software verification,then the strategy was raised and an algorithm was implemented to take advantage of program locality.This method exploits the features of modern BMC (bounded model checker) and scales up the capability of its power in large scale and comprehensive software modules.

Key words: model checking, BMC, software verification, locality,optimization

中图分类号:

TP311.1

王舜,杜晔,韩臻,刘吉强. 基于程序局部性引导的有界模型检测优化方法[J]. 通信学报, 2018, 39(3): 181-190.

Shun WANG,Ye DU,Zhen HAN,Jiqiang LIU. Locality-guided based optimization method for bounded model checker[J]. Journal on Communications, 2018, 39(3): 181-190.

图/表 3

参考文献 34

[1]	JHALA R , MAJUMDAR R . Software model checking[J]. ACM Computing Surveys, 2009,41(4): 1-54.
[2]	BJORNER N , MCMILLAN K , RYBALCHENKO A . On solving universally quantified horn clauses[C]// The International Symposium on Static Analysis. 2013: 105-125.
[3]	CLARKE E , KROENING D , LERDA F . A tool for checking ansi-c programs[C]// The 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2004: 168-176.
[4]	CORDEIRO L , LISCHER B , MARQUES S J . SMT-based bounded model checking for embedded ANSIC software[J]. IEEE Transactions on Software Engineering, 2012,38(4): 137-148.
[5]	YANG Z , GANAI M K , GUPTA A ,et al. Efficient SAT-based bounded model checking for software verification[J]. Theoretical Computer Science, 2008,404(3): 256-274.
[6]	MERZ F , FALKE S , SINZ C . LLBMC:bounded model checking of C and C++ programs using a compiler IR[C]// The International Conference on Verified Software:Theories,Tools,Experiments. 2012: 146-161.
[7]	MORSE J , CORDEIRO D , NICOLE D ,et al. Handling unbounded loops with ESBMC 1.20[C]// The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2013: 619-622.
[8]	DAVIS M , LOGEMANN G , LOVELAND D . A machine program for theorem-proving[J]. Communications of the ACM, 1967,5(5): 394-397.
[9]	HOOKER J N , VINAY V . Branching rules for satisfiability[J]. Journal of Automated Reasoning, 1995,15(3): 359-383.
[10]	LI C M , ANBULAGAN A . Heuristics based on unit propagation for satisfiability problems[C]// The 15th International Joint Conference on Artificial Intelligence. 1997: 366-371.
[11]	MOURA D , BJORNER N . Z3:an efficient SMT solver[C]// The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2008: 337-340.
[12]	LIU L , KONG W , ANDO T . A survey of acceleration techniques for SMT-based bounded model checking[C]// The International Conference on Computer Sciences and Applications. 2013: 554-559.
[13]	HENZINGER T A , JHALA R , MAJUMDAR R ,et al. Abstractions from proofs[J]. ACM SIGPLAN Notices, 2004,39(1): 232-244.
[14]	JHALA R , MCMILLAN K L . Array abstractions from proofs[C]// The International Conference on Computer Aided Verification. 2004: 232-244.
[15]	MCMILLAN K L , . Lazy abstraction with interpolants[C]// The International Conference on Computer Aided Verification. 123-136.
[16]	GULAVANI B S , RAJAMANI S K . Counterexample driven refinement for abstract interpretation[C]// The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2006: 474-488.
[17]	FLANAGAN C , QADEER S . Predicate abstraction for software verification[J]. ACM SIGPLAN Notices, 2002,37(1): 191-202.
[18]	KOMURAVELLI A , GURFINKEL A , CHAKI S . Automatic abstraction in SMT-based unbounded software model checking[C]// The International Conference on Computer Aided Verification. 2013: 846-862.
[19]	APEL S , BEYER D , FRIEDBERGER K . Domain types:abstract- domain selection based on variable usage[C]// The International Conference on Hardware and Software:Verification and Testing. 2013: 262-278.
[20]	BEYER D , HENZINGER T A , THEODULOZ G . Lazy shape analysis[C]// International Conference on Computer Aided Verification. 2006: 532-546.
[21]	HENZINGER T A , JHALA R , MAJUMDAR R ,et al. Lazy abstraction[J]. ACM SIGPLAN Notices, 2002,37(1): 58-70.
[22]	BRADLEY A R , . SAT-based model checking without unrolling[C]// The International Conference on Verification,Model Checking,and Abstract Interpretation. 2011: 70-87.
[23]	RRADLEY A R , MANNA Z . Checking safety by inductive generalization of counterexamples to induction[C]// The International Conference on Formal Methods in Computer Aided Design. 2007: 173-180.
[24]	CHAKI S , CLARKE E M , GROCE A ,et al. Modular verification of software components in C[J]. IEEE Transactions on Software Engineering, 2004,30(6): 388-402.
[25]	BEYER D , KEREMOGLU M E . CPAchecker:a tool for configurable software verification[C]// The International Conference on Computer Aided Verification. 2011: 184-190.
[26]	BEYER D , LEMBERGER T . Symbolic execution with CEGAR[M]// Leveraging Applications of Formal Methods,Verification and Validation: Foundational Techniques.Springer International Publishing, 2016.
[27]	BEYER D , DANGL M , WENDLER P . Boosting K-induction with Continuously-refined Invariants[M]// Computer Aided Verification. Springer International Publishing, 2015: 622-640.
[28]	BEYER D , LOWE S . Interpolation for value analysis[J]. Software-Engineering and Management, 2015: 73-74.
[29]	BEYER D , WENDLER P . Reuse of verification results[C]// The International Symposium on Model Checking Software. 2013: 1-17.
[30]	BEYER D , LOWE S . Explicit-State software model checking based on CEGAR and interpolation[C]// The International Conference on Fundamental Approaches to Software Engineering. 2013: 146-162.
[31]	ALBARGHOUTHI A , GURFINKEL A , CHECHIK M . From Under-Approximations to Over-Approximations and Back[C]// The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2012: 157-172.
[32]	KROENING D , STRICHMAN O . Decision procedures:an algorithmic point of view[M]. Springer Publishing Company, 2008.
[33]	SINZ C , MERZ F , FALKE S . LLBMC:a bounded model checker for LLVM’s intermediate representation[C]// The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2012: 542-544.
[34]	BEYER D , . Status report on software verification[C]// The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2014: 373-388.

样本平均数	算法时间消耗/s
样本平均数	LLBMC	基础算法	改进算法
533	611	735	708
729	971	832	820
1 002	3 613	3 570	3 439
1 291	N/A	3 902	3 219
1 347	N/A	6 037	5 791

基于程序局部性引导的有界模型检测优化方法

Locality-guided based optimization method for bounded model checker

在线阅读

PDF下载

可视化

摘要/Abstract

引用本文

使用本文

图/表 3

参考文献 34

相关文章 15

Metrics

推荐阅读 0

样本类型	成功检测数量
样本类型	LLBMC	基础算法	改进算法
简单程序	39	44	45
条件程序	21	27	27
循环程序	17	23	23
内存操作程序	19	20	20

[1]	李竟博, 马礼, 李阳, 傅颖勋, 马东超. 感传算协同工业互联网优化设计[J]. 通信学报, 2023, 44(6): 12-22.
[2]	张平, 戴金晟, 张育铭, 王思贤, 秦晓琦, 牛凯. 面向语义通信的非线性变换编码[J]. 通信学报, 2023, 44(4): 1-14.
[3]	蒋丽, 谢胜利, 田辉. 面向数字孪生边缘网络的区块链分片及资源自适应优化机制[J]. 通信学报, 2023, 44(3): 12-23.
[4]	余雪勇, 邱礼翔, 宋家宁, 朱洪波. 无人机辅助边缘计算中安全通信与能效优化策略[J]. 通信学报, 2023, 44(3): 45-54.
[5]	张雷, 王玉, 田建杰, 张琳, 章天骄. 基于IRS辅助的MIMO车联网系统联合波束成形设计[J]. 通信学报, 2023, 44(2): 59-69.
[6]	赵庶旭, 韦萍, 王小龙. 多任务并发边缘计算环境中最优联盟结构生成策略[J]. 通信学报, 2023, 44(2): 172-184.
[7]	王彬, 任露, 王晓帆, 曹雅娟. 基于协方差分析的合作协同进化差分进化算法[J]. 通信学报, 2023, 44(1): 189-199.
[8]	胡强, 田雨晴, 綦浩泉, 吴鹏, 刘庆雪. 基于改进人工蜂群算法的云制造服务组合优化方法[J]. 通信学报, 2023, 44(1): 200-210.
[9]	聂宏蕊, 李绍胜, 刘勇. 时间敏感网络中基于IEEE 802.1Qch标准的优化调度机制[J]. 通信学报, 2022, 43(9): 12-26.
[10]	杨震, 冯璇, 吕斌. 智能反射面辅助的两跳中继无线供电通信网络吞吐量最大化研究[J]. 通信学报, 2022, 43(9): 90-99.
[11]	许文俊, 吴思雷, 王凤玉, 林兰, 李国军, 张治. 基于多智能体强化学习的大规模灾后用户分布式覆盖优化[J]. 通信学报, 2022, 43(8): 1-16.
[12]	郭海燕, 杨震, 邹玉龙, 吕斌, 冯蕴天, 赵玉娟. 基于主被动波束成形联合优化的双RIS辅助抗干扰通信方法[J]. 通信学报, 2022, 43(7): 21-30.
[13]	何世文, 袁军, 安振宇, 张敏, 黄永明, 张尧学. 基于图神经网络的联合用户调度与波束成形优化算法[J]. 通信学报, 2022, 43(7): 73-84.
[14]	朱思峰, 蔡江昊, 柴争义, 孙恩林. 车联网云边协同计算场景下的多目标优化卸载决策[J]. 通信学报, 2022, 43(6): 223-234.
[15]	李翠然, 王雪洁, 谢健骊, 吕安琪. 基于改进PSO的铁路监测线性无线传感器网络路由算法[J]. 通信学报, 2022, 43(5): 155-165.