引用本文:孙全,许蕾,夏昕濛,张卫丰.使用共享变量分析和约束求解检测安卓应用数据竞争.软件学报,2019,30(11):3281-3296
【打印本页】   【下载PDF全文】   查看/发表评论  【EndNote】   【RefMan】   【BibTex】
←前一篇|后一篇→ 过刊浏览    高级检索
本文已被:浏览 2576次   下载 6241 本文二维码信息
码上扫一扫!
分享到: 微信 更多
使用共享变量分析和约束求解检测安卓应用数据竞争
孙全1,2, 许蕾1,2, 夏昕濛1,2, 张卫丰3
1.计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;2.南京大学 计算机科学与技术系, 江苏 南京 210023;3.南京邮电大学 计算机学院, 江苏 南京 210023
摘要:
安卓系统在移动端操作系统始终占据主导地位,在增强用户体验和提高程序性能的同时,其特有的事件驱动模型和多线程模型也造成了并发缺陷.并发程序中,线程调度的不确定性和难以再现性是并发缺陷检测困难的原因.现有技术主要在动态生成执行路径的基础上进行发生序(happens-before)分析,进而检测安卓应用的并发缺陷,但仍然存在低覆盖率、误报、漏报等问题.结合共享变量分析和约束求解方法实现了安卓应用数据竞争的检测,并实现了检测工具RaceDetector.该工具首先根据安卓系统的特性和数据竞争的定义,通过静态分析抽取相关信息,并进一步使用安卓共享变量分析来提高准确性和性能,继而进行可疑数据竞争分析,得出可疑的数据竞争集合;接着根据每一个可疑的数据竞争候选者,通过约束求解的方法在所有事件调度和线程调度解空间下识别发生序关系,并最终检测出真正的数据竞争.实验部分是从Google Play等来源收集了15个流行的应用APK文件作为数据集,RaceDetector平均报告了340个数据竞争,误报率为13%(44/340).与现有工具EventRacer(默认产生300随机事件触发应用执行,平均检测2个有害数据竞争)相比,RaceDetector能够解析全部源码,覆盖了所有线程调度和事件调度,平均检测出15个有害数据竞争.
关键词:  安卓应用  数据竞争  事件驱动模型  多线程模型  约束求解
DOI:10.13328/j.cnki.jos.005582
分类号:TP311
基金项目:国家重点基础研究发展计划(973)(2014CB340702);国家自然科学基金(61272080,91418202,61403187);江苏省自然科学基金(BK20140611)
Detecting Data Races in Android Applications Based on Shared Variable Analysis and Constraint Solver
SUN Quan1,2, XU Lei1,2, XIA Xin-Meng1,2, ZHANG Wei-Feng3
1.State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China;2.Department of Computer Science and Technology, Nanjing University, Nanjing 210023, China;3.School of Computer Science, Nanjing University of Postsand Telecommunications, Nanjing 210023, China
Abstract:
The Android system has always dominated the mobile operating system. Its unique event-driven model and multi-threaded model also cause concurrency defects while enhancing the user experience and improving the program performance. In concurrent programs, the non-determinism of thread scheduling and the complexity of its reproducibility are the reasons for the difficulty of concurrency bug detection. The existing technologies mainly focus on the analysis of happens-before relationships based on the dynamic analysis, and then detect the concurrency bugs of Andriod applications (App for short). Nevertheless, there are still some problems of low coverage and high false positive (FP) due to the shortage of dynamic method. In this study, data races in Android applications are detected by the shared variable analysis and the constraint solving method, and detection tool, namely RaceDetector, is implemented. The tool firstly extracts the relevant information according to the characteristics of Android system and the definition of data race, and further expands the shared variable analysis to improve the accuracy and performance, and then it obtains a suspicious data race set with suspicious data race analyzing. Next, it identifies the feasible implementation of the path and the order of happens-before relationships according to every suspicious data race candidate through the method of constraint solving and finally detects the real data races. In experimental part, 15 popular applications with APK files are collected from Google Play and other sourcesas data sets. RaceDetector reports 340 data races on average, include 13% (44/340) of FP. Compared to existing tool, EventRacer, which triggers data races with 300 random events and reports 2 harmful data races on average, RaceDetector covers all thread schedules and event schedules, and it reports 15 harmful data races on average.
Key words:  Android application  data race  event driven model  multi-thread model  constraint solver

引用本文:
【打印本页】   【下载PDF全文】   查看/发表评论  【EndNote】   【RefMan】   【BibTex】
←前一篇|后一篇→ 过刊浏览    高级检索
本文已被:浏览次   下载  
分享到: 微信 更多
摘要:
关键词:  
DOI:
分类号:
基金项目:
Abstract:
Key words: