使用共享变量分析和约束求解检测安卓应用数据竞争

作     者：孙全 许蕾 夏昕濛 张卫丰 SUN Quan;XU Lei;XIA Xin-Meng;ZHANG Wei-Feng

作者机构：计算机软件新技术国家重点实验室(南京大学)江苏南京210023 南京大学计算机科学与技术系江苏南京210023 南京邮电大学计算机学院江苏南京210023 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2019年第30卷第11期

页      面：3281-3296页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

基　　金：国家重点基础研究发展计划(973)(2014CB340702) 国家自然科学基金(61272080,91418202,61403187) 江苏省自然科学基金(BK20140611)~~ 

主　　题：安卓应用 数据竞争 事件驱动模型 多线程模型 约束求解 

摘      要：安卓系统在移动端操作系统始终占据主导地位,在增强用户体验和提高程序性能的同时,其特有的事件驱动模型和多线程模型也造成了并发缺陷.并发程序中,线程调度的不确定性和难以再现性是并发缺陷检测困难的原因.现有技术主要在动态生成执行路径的基础上进行发生序(happens-before)分析,进而检测安卓应用的并发缺陷,但仍然存在低覆盖率、误报、漏报等问题.结合共享变量分析和约束求解方法实现了安卓应用数据竞争的检测,并实现了检测工具RaceDetector.该工具首先根据安卓系统的特性和数据竞争的定义,通过静态分析抽取相关信息,并进一步使用安卓共享变量分析来提高准确性和性能,继而进行可疑数据竞争分析,得出可疑的数据竞争集合;接着根据每一个可疑的数据竞争候选者,通过约束求解的方法在所有事件调度和线程调度解空间下识别发生序关系,并最终检测出真正的数据竞争.实验部分是从Google Play等来源收集了15个流行的应用APK文件作为数据集,RaceDetector平均报告了340个数据竞争,误报率为13%(44/340).与现有工具EventRacer(默认产生300随机事件触发应用执行,平均检测2个有害数据竞争)相比,RaceDetector能够解析全部源码,覆盖了所有线程调度和事件调度,平均检测出15个有害数据竞争.