基于符号执行的能耗错误检测方法

doi:10.3969/j.issn.0372-2112.2016.05.005

电子学报 ›› 2016, Vol. 44 ›› Issue (5): 1040-1050.DOI: 10.3969/j.issn.0372-2112.2016.05.005

基于符号执行的能耗错误检测方法

徐超¹, 陈勇², 葛红美¹, 何炎祥³

1. 南京审计大学, 江苏南京 210029;
2. 中国电子科技集团第十四研究所, 江苏南京 210013;
3. 武汉大学计算机学院, 湖北武汉 430072

收稿日期:2015-09-27 修回日期:2016-01-04 出版日期:2016-05-25
- 通讯作者:
- 陈勇
- 作者简介:
- 徐超男,1980年出生,湖北红安人,博士,副教授,研究方向为可信软件、嵌入式系统和计算机审计.E-mail:xuchao@nau.edu.cn
- 基金资助:
- 国家自然科学基金 (No.61170022); 江苏省高校自然科学研究面上项目 (No.15KJB520019); 江苏省"六大人才"高峰项目资助; 江苏省高校"青蓝工程"优秀青年骨干教师培养对象资助; 江苏高校优势学科建设工程资助项目

Symbolic Execution Based Energy Bug Detecting Method

XU Chao¹, CHEN Yong², GE Hong-mei¹, HE Yan-xiang³

1. Nanjing Audit University, Nanjing, Jiangsu 210029, China;
2. The 14th Research Institute of CETC, Nanjing, Jiangsu 210013, China;
3. Computer School of Wuhan University, Wuhan, Hubei 430072, China

Received:2015-09-27 Revised:2016-01-04 Online:2016-05-25 Published:2016-05-25
- Supported by:
- National Natural Science Foundation of China (No.61170022); Natural Science Research Project of Colleges and Universities in Jiangsu Province (No.15KJB520019); Funded by Six Talents Peaks in Jiangsu Province; Supported by Training Objects of Young Teachers in Blue Project in Jiangsu Province; A Project Funded by the Priority Academic Program Development of Jiangsu Higher Education Institutions

摘要/Abstract

摘要：

能耗是制约便携式智能设备发展的重要瓶颈.随着嵌入式操作系统的广泛应用,因不能合理使用操作系统的API而导致的能耗错误已经成为各种嵌入式应用开发过程中不容忽视的因素.为减少应用中的能耗错误,以符号执行技术为基础,根据禁止休眠类能耗错误的特点,设计了对应的能耗错误检测方法.该方法首先利用过程内分析,获得单个函数的符号执行信息.然后借助过程间分析对单个函数的符号执行信息进行全局综合,得到更为精确的执行开销、锁变量匹配等相关信息,以更好的检测能耗错误.同时,符号执行记录了对应的分支路径信息,利用该信息能够结合约束求解器较为方便的生成出错的测试用例,进而定位错误位置.通过示例和实验,验证了该方法在能耗错误检测方面的可行性和有效性.

关键词: 能耗错误, 符号执行, 错误检测, 过程内分析, 过程间分析

Abstract:

Energy is one important bottleneck to the development of intelligent portable device.With the wide use of embedded operation system, the energy bug caused by unsuitablely using the API of the operation system has become the important factor in the designment of the embedded application.According to the characteristics of the No-Sleeping energy bug, a symbolic execution based energy bug detecting method is proposed to reduce the energy bug.It first uses intraprocedural analysis technology to analyze one function independently to get the energy information of the function.Then, the interprocedural analysis technology is applied to get the globe analysis of the program by the information of intraprocedural analysis which can get more accuate information for energy bug detection.Meanwhile, constraint solver can be combined to obtain the counter-example for locating the position of the error.Example and experiment results verify that the method is feasible and effective in energy bug detection.

Key words: energy bug, symbolic execution, bug detection, intraprocedural analysis, interprocedural analysis

中图分类号:

TP311

徐超, 陈勇, 葛红美, 等. 基于符号执行的能耗错误检测方法[J]. 电子学报, 2016, 44(5): 1040-1050.

XU Chao, CHEN Yong, GE Hong-mei, et al. Symbolic Execution Based Energy Bug Detecting Method[J]. Acta Electronica Sinica, 2016, 44(5): 1040-1050.

参考文献

[1] Pathak A,Hu Y C,Zhang M.Bootstrapping energy debugging on smartphones:a first look at energy bugs in mobile devices[A].Proceedings of the 10th ACM Workshop on Hot Topics in Networks[C].Cambridge,USA:ACM;2011.5-10.
[2] Pathak A,Hu Y C,Zhang M.Where is the energy spent inside my app?:fine grained energy accounting on smartphones with eprof[A].Proceedings of the 7th ACM european conference on Computer Systems[C].Bern,Switzerland:ACM;2012.29-42.
[3] Pathak A,Jindal A,Hu Y C,et al.What is keeping my phone awake:characterizing and detecting no-sleep energy bugs in smartphone apps[A].Proceedings of the 10th international conference on Mobile systems,applications,and services[C].Ambleside,United Kingdom:ACM;2012.267-280.
[4] Vekris P,Jhala R,Lerner S,et al.Towards verifying android apps for the absence of no-sleep energy bugs[A].Proceedings of the 2012 USENIX conference on Power-Aware Computing and Systems[C].New York,USA:USENIX Association;2012.3-13.
[5] Oliner A J,Iyer A,Lagerspetz E,et al.Collaborative energy debugging for mobile devices[A].Proceedings of the Eighth USENIX conference on Hot Topics in System Dependability[C].Berkeley,CA,USA:USENIX Association;2012.6-6.
[6] Jindal A,Pathak A,Hu Y C,et al.Hypnos:understanding and treating sleep conflicts in smartphones[A].Proceedings of the 8th ACM European Conference on Computer Systems[C].Prague,Czech Republic:ACM;2013.253-266.
[7] King J C.Symbolic execution and program testing[J].Communications of the ACM,1976,19(7):385-394.
[8] Boyer R S,Elspas B,Levitt K N.SELECT-a formal system for testing and debugging programs by symbolic execution[J].Acm Sigplan Notices,1975,10(6):234-245.
[9] Khurshid S,P?s?reanu C S,Visser W.Generalized Symbolic Execution for Model Checking and Testing[M].Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2003.553-568.
[10] P Godefroid,N Klarlund,K Sen.DART:Directed Automated Random Testing[A].Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation[C].Chicago,USA;2005.213-223.
[11] Majumdar R,Sen K.Hybrid concolic testing[A].29th International Conference on Software Engineering[C].Minneapolis,USA:IEEE;2007.416-426.
[12] Burnim J,Sen K.Heuristics for Scalable Dynamic Test Generation[J].IEEE Computer Society,2008(8):443-446.
[13] Anand S,Godefroid P,Tillmann N.Demand-Driven Compositional Symbolic Execution[M].Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2008.367-381.
[14] Staats M,Pǎsǎreanu C.Parallel symbolic execution for structural test generation[A].Proceedings of the 19th international symposium on Software testing and analysis[C].Trento,Italy:ACM;2010.183-194.
[15] Anand S,P?s?reanu C S,Visser W.JPF-SE:A Symbolic Execution Extension to Java Pathfinder[M].Springer Berlin Heidelberg,Tools and Algorithms for the Construction and Analysis of Systems,2007:134-138.
[16] Cadar C,Dunbar D,Engler D R.KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs[A].OSDI[C].Berkeley,USA;2008.209-224.
[17] Cadar C,Ganesh V,Pawlowski P M,et al.EXE:automatically generating inputs of death[J].ACM Transactions on Information and System Security (TISSEC),2008,12(2):10-20.
[18] Sen K,Marinov D,Agha G.CUTE:A Concolic Unit Testing Engine for C[M].ACM,2005.50-60.
[19] 梅宏,王千祥,张路,等.软件分析技术进展[J].计算机学报,2009,32(9):1697-1710. MEI Hong,WANG Qian-Xiang,ZHANG Lu,et al.Software Analysis:A road map[J].Chinese Journal of Computers,2009,32(9):1697-1710.(in Chinese)
[20] 范文庆.分段符号执行模型及其环境交互问题研究[D].北京:北京邮电大学,2010.40-50. Fan Wenqing.Research on the implementation model of the sub symbolic execution model and its environment interaction[D].Beijing:Beijing University of Posts and Telecommunications,2010.40-50.(in Chinese)
[21] Boonstoppel P,Cadar C,Engler D.RWset:Attacking Path Explosion in Constraint-Based Test Generation[M].Springer Berlin Heidelberg,Tools and Algorithms for the Construction and Analysis of Systems,2008.351-366.
[22] Schwartz E J,Avgerinos T,Brumley D.All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask)[A].2010 IEEE Symposium on Security and Privacy[C].Oakland,California;2010.317-331.
[23] 林梦香,陈胤立,陈睿,等.基于懒替换的C符号执行[J].北京航空航天大学学报,2009,06(6):687-691. Lin Mengxiang,Chen Yinli,Chen Rui,et al.Execution of C symbols based on lazy replacement[J].Journal of BeiJing University of Aeronautics and Astronautics,2009,06(6):687-691.(in Chinese)

基于符号执行的能耗错误检测方法

Symbolic Execution Based Energy Bug Detecting Method

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 7

编辑推荐

Metrics

[1]	汪孙律, 杨秋松, 李明树. 一种针对格式文件的符号执行优化方法[J]. 电子学报, 2020, 48(12): 2417-2424.
[2]	杨超, 郭云飞, 扈红超, 刘文彦, 霍树民, 王亚文. 基于符号执行的软件缓存侧信道脆弱性检测技术[J]. 电子学报, 2019, 47(6): 1194-1200.
[3]	郭曦, 王盼. 基于依赖条件重构的程序符号值分析方法[J]. 电子学报, 2019, 47(3): 630-635.
[4]	赵祖威, 冯世宁, 汤恩义, 陈鑫, 李宣东, 潘敏学, 赵晨. 一种符号执行制导的循环内界分析方法[J]. 电子学报, 2017, 45(11): 2582-2592.
[5]	黄浩, 徐海华, 王羡慧, 吾守尔·斯拉木. 自动发音错误检测中基于最大化F1值准则的区分性特征补偿训练算法[J]. 电子学报, 2015, 43(7): 1294-1299.
[6]	王志, 贾春福, 刘伟杰, 王晓初, 张海宁, 于晓旭, 陈喆. 一种抵抗符号执行的路径分支混淆技术[J]. 电子学报, 2015, 43(5): 870-878.
[7]	万勇兵, 徐中伟, 梅萌. 一种符号化执行的实时系统一致性测试生成方法[J]. 电子学报, 2013, 41(11): 2276-2284.