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