广西师范大学学报（自然科学版） ›› 2020, Vol. 38 ›› Issue (2): 29-42.doi: 10.16088/j.issn.1001-6600.2020.02.004

• CTCIS2019 • 上一篇    下一篇

基于Pi演算的Android多线程程序的数据竞争检测

王涛1,2, 马川2*   

  1. 1. 河北科技师范学院工商管理学院,河北秦皇岛066004;
    2. 燕山大学信息科学与工程学院,河北秦皇岛066004
  • 收稿日期:2019-10-08 发布日期:2020-04-02
  • 通讯作者: 马川(1981—),男,河北保定人,燕山大学副教授,博士。E-mail:tianyi_mc@126.com
  • 基金资助:
    河北省社会科学基金(HB18SH012)

Data Race Detection for Multi-threaded Programsin Android Based on Pi Calculus

WANG Tao1,2, MA Chuan2*   

  1. 1. College of Business Administration, Hebei Normal University of Science and Technology, Qinhuangdao Hebei 066004, China;
    2. College of Information Science and Engineering, Yanshan University, Qinhuangdao Hebei 066004, China
  • Received:2019-10-08 Published:2020-04-02

PDF (PC)

239

摘要： 针对事件驱动机制下Android多线程程序的数据竞争问题,构造一个基于Pi演算的并发行为检测模型。利用扩展后的Pi演算对Android生命周期和多线程框架进行建模,得到形式化的行为模型;通过将安全约束抽象为形式化的IF-THEN规则,并利用Pi演算的性质进行进程演算和迁移,构建了检测模型;将动态检测与静态检测以相同的处理方式结合在检测模型中,并给出了并发行为检测算法和数据竞争检测的方法。理论分析和实验表明,本文所提出的方法具有线性的时间和空间复杂度,相比其他方法,在提高检测精确性的同时并没有牺牲检测的效率。

关键词: Android Apps, 数据竞争, 并发行为, 进程代数, 多线程

Abstract: To solve the data race problem in Android multi-threaded programs, a model of concurrent behavior detection based on Pi calculus is proposed in this paper. The extended Pi calculus is used to model Android life cycle and multi-threaded framework, and a formal behavior model is obtained. Moreover, the detection model is constructed by abstracting security constraints into formal IF-THEN rules and using the properties of Pi calculus to perform process calculus and migration. The dynamic detection and static detection are combined in the detection model by the same way, and concurrent behavior detection algorithm and data race detection method are given. The analysis and experiment results show that this method has linear time and space complexity. Compared with other methods, the detection accuracy is improved without sacrificing the detection efficiency.

Key words: Android Apps, data race, concurrent behavior, process algebra, multi-threaded

中图分类号: 

  • TP309
[1] SAVAGE S, BURROWS M, NELSON G, et al. Eraser: A dynamic data race detector for multi-threaded programs[J]. ACM Trans on Computer Systems, 1997,15(4):391-411.
[2] WANG L Q, STOLLER S D. Runtime analysis of atomicity for multi-threaded programs[J]. IEEE Trans on Software Engineering, 2006, 32(2):93-110.
[3] 蒋炎岩,许畅,马晓星,等. 获取访存依赖:并发程序动态分析基础技术综述[J].软件学报,2017,28(4):747-763.
[4] DUESTERWALD E, SOFFA M L. Concurrency analysis in the presence of procedures using a data-flow framework[C]//Proceedings of the Symposium on Testing, Analysis, and Verification. New York, NY:ACM, 1991: 36-48.
[5] ENGLER D, ASHCRAFT K. RacerX: effective, static detection of race conditions and deadlocks[C] //ACM SIGOPS Operating Systems Review. New York, NY: ACM, 2003, 37(5): 237-252.
[6] NAIK M, AIKEN A, WHALEY J. Effective static race detection for Java[C]//Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI′06). New York, NY: ACM, 2006:308-319.
[7] PRATIKAKIS P, FOSTER J S, HICKS M. LOCKSMITH: context-sensitive correlation analysis for race detection[J]. ACM SIGPLAN Notices, 2006, 41(6): 320-331.
[8] VOUNG J W, JHALA R, LERNER S. RELAY: static race detection on millions of lines of code[C]//Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering. New York, NY: ACM, 2007: 205-214.
[9] HUANG J, RAJAGOPALAN A K. Precise and maximal race detection from incomplete traces[J]. ACM SIGPLAN Notices, 2016, 51(10): 462-476.
[10]孔德光,谭小彬,奚宏生,等.多线程程序时序分析的隐Markov模型[J].软件学报,2010,21(3): 461-472.
[11]LIN Y, RADOI C, DIG D. Retrofitting concurrency for android applications through refactoring[C]//Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering. New York, NY: ACM, 2014: 341-352.
[12]SAFI G, SHAHBAZIAN A, HALFOND W G J, et al. Detecting event anomalies in event-based systems[C]//Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering. New York, NY: ACM, 2015: 25-37.
[13]SUN Q, XU L, CHEN L, et al. Replaying harmful data races in android apps[C]//2016 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). Piscataway, NJ: IEEE, 2016: 160-166.
[14]HU Y, NEAMTIU I. Static detection of event-based races in android apps[C] //Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems. New York, NY:ACM, 2018: 257-270.
[15]FU X, LEE D, JUNG C. nAdroid: statically detecting ordering violations in Android applications[C]//Proceedings of the 2018 International Symposium on Code Generation and Optimization. New York, NY:ACM, 2018: 62-74.
[16]WU D, LIU J, SUI Y, et al. Precise static happens-before analysis for detecting UAF order violations in Android[C]//2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST). Piscataway, NJ: IEEE, 2019: 276-287.
[17]MAIYA P, KANADE A, MAJUMDAR R. Race detection for Android applications[J].ACM SIGPLAN Notices, 2014, 49(6): 316-325.
[18]BIELIK P, RAYCHEV V, VECHEV M. Scalable race detection for android applications[J]//ACM SIGPLAN Notices, 2015, 50(10): 332-348.
[19]HOARE C A R. Communicating sequential processes[M]. New York:Springer, 1978.
[20]MILNER R. A calculus of communicating systems[M]. Berlin: Springer-Verlag, 1980.
[21]MILNER R. Communicating and mobile systems: the pi calculus[M]. Cambridge:Cambridge University Press, 1999.
[22]Google. Android documentation: Activity [EB/OL]. [2019-05-04].http://develop er.android.com/reference/android/app/Activity.html.
[23]ARZT S, RASTHOFER S, FRITZ C, et al. Flowdroid: Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for android apps[J]. Acm Sigplan Notices, 2014, 49(6): 259-269.
[24]LAM P, BODDEN E, LHOTÁK O, et al. The soot framework for Java program analysis: a retrospective[C]//Cetus Users and Compiler Infastructure Workshop (CETUS 2011). Galveston Island: Purdue University Press, 2011: 35.
[1] 葛丽娜. 基于k-同构和局部随机化的隐私保护方法[J]. 广西师范大学学报（自然科学版）, 2016, 34(4): 1-8.
[2] 谭鸿健, 杨雅惠, 董明刚. 基于改进G-O费用模型的软件最优发布研究[J]. 广西师范大学学报（自然科学版）, 2014, 32(2): 48-54.
[3] 侯有利, 杨雄. 基于DES加密算法的数据库二级加密密钥技术[J]. 广西师范大学学报（自然科学版）, 2011, 29(3): 125-130.
[4] 黄添强, 李凯, 郑之. 有监督的噪音流形学习算法[J]. 广西师范大学学报（自然科学版）, 2011, 29(3): 131-135.
[5] 王涵, 王绪安, 周能, 柳玉东. 基于区块链的可审计数据分享方案[J]. 广西师范大学学报（自然科学版）, 2020, 38(2): 1-7.
[6] 张永生, 朱文焌, 史若琪, 杜振华, 张瑞, 王志. 基于可信度的Android恶意代码多模型协同检测方法[J]. 广西师范大学学报（自然科学版）, 2020, 38(2): 19-28.
[7] 周炎岩, 冯嘉礼. 基于定性映射的数字音频水印算法[J]. 广西师范大学学报（自然科学版）, 2011, 29(2): 200-204.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] 黄雯, 谭惠丽. 心脏记忆对螺旋波动力学的影响[J]. 广西师范大学学报（自然科学版）, 2017, 35(2): 1 -8 .
[2] 陈鼎新, 刘代志, 孟亮, 李义红, 杨晓君. 时空Kriging在局域地磁场分析中的应用[J]. 广西师范大学学报（自然科学版）, 2016, 34(1): 38 -44 .
[3] 许伦辉, 刘景柠, 朱群强, 王晴, 谢岩, 索圣超. 自动引导车路径偏差的控制研究[J]. 广西师范大学学报（自然科学版）, 2015, 33(1): 1 -6 .
[4] 邝先验, 吴赟, 曹韦华, 吴银凤. 城市混合非机动车流的元胞自动机仿真模型[J]. 广西师范大学学报（自然科学版）, 2015, 33(1): 7 -14 .
[5] 肖瑞杰, 刘野, 修晓明, 孔令江. 耦合腔光机械系统中两个机械振子的态交换[J]. 广西师范大学学报（自然科学版）, 2015, 33(1): 15 -19 .
[6] 黄慧琼, 覃运梅. 考虑驾驶员性格特性的超车模型研究[J]. 广西师范大学学报（自然科学版）, 2015, 33(1): 20 -26 .
[7] 袁乐平, 孙瑞山. 飞行冲突调配概率安全评估方法研究[J]. 广西师范大学学报（自然科学版）, 2015, 33(1): 27 -31 .
[8] 杨盼盼, 祝龙记, 操孟杰. 基于STM32的TSC型无功补偿控制系统的研究[J]. 广西师范大学学报（自然科学版）, 2015, 33(1): 32 -37 .
[9] 章美月. 关于电子束聚焦系统模型的一些新结果[J]. 广西师范大学学报（自然科学版）, 2015, 33(1): 38 -44 .
[10] 侯晓东, 蔡斌斌, 金炜东, 段旺旺. 基于证据距离和模糊熵的加权证据融合新方法[J]. 广西师范大学学报（自然科学版）, 2015, 33(1): 45 -51 .
版权所有 © 广西师范大学学报（自然科学版）编辑部
地址：广西桂林市三里店育才路15号　邮编：541004
电话：0773-5857325　E-mail: gxsdzkb@mailbox.gxnu.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发