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

doi:10.16088/j.issn.1001-6600.2020.02.004

Abstract

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

CLC Number:

TP309

WANG Tao, MA Chuan. Data Race Detection for Multi-threaded Programsin Android Based on Pi Calculus[J].Journal of Guangxi Normal University(Natural Science Edition), 2020, 38(2): 29-42.

References

[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.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

Comments

Recommended 10

[1]	HUANG Wen,TAN Huili. Effect of Cardiac Memory on Spiral Wave[J]. Journal of Guangxi Normal University(Natural Science Edition), 2017, 35(2): 1 -8 .
[2]	CHEN Dingxin, LIU Daizhi, MENG Liang, LI Yihong, YANG Xiaojun. Applications of Spatiotemporal Kriging in Local Geomagnetic Field Analysis[J]. Journal of Guangxi Normal University(Natural Science Edition), 2016, 34(1): 38 -44 .
[3]	XU Lun-hui, LIU Jing-ning, ZHU Qun-qiang, WANG Qing, XIE Yan, SUO Sheng-chao. Path Deviation Control of Automatic Guided Vehicle[J]. Journal of Guangxi Normal University(Natural Science Edition), 2015, 33(1): 1 -6 .
[4]	KUANG Xian-yan, WU Yun, CAO Wei-hua, WU Yin-feng. Cellular Automata Simulation Model for Urban MixedNon-motor Vehicle Flow[J]. Journal of Guangxi Normal University(Natural Science Edition), 2015, 33(1): 7 -14 .
[5]	XIAO Rui-jie, LIU Ye, XIU Xiao-ming, KONG Ling-jiang. State Transfer of Two Mechanical Oscillators in Coupled CavityOptomechanical System[J]. Journal of Guangxi Normal University(Natural Science Edition), 2015, 33(1): 15 -19 .
[6]	HUANG Hui-qiong, QIN Yun-mei. Overtaking Model Based on Drivers’ Characteristics[J]. Journal of Guangxi Normal University(Natural Science Edition), 2015, 33(1): 20 -26 .
[7]	YUAN Le-ping, SUN Rui-shan. Probabilistic Safety Assessment of Air Traffic Conflict Resolution[J]. Journal of Guangxi Normal University(Natural Science Edition), 2015, 33(1): 27 -31 .
[8]	YANG Pan-pan, ZHU Long-ji, CAO Meng-jie. TSC Type of Reactive Power Compensation Control SystemBased on STM32[J]. Journal of Guangxi Normal University(Natural Science Edition), 2015, 33(1): 32 -37 .
[9]	ZHANG Mei-yue. Some New Results for the Electron Beams Focusing System Model[J]. Journal of Guangxi Normal University(Natural Science Edition), 2015, 33(1): 38 -44 .
[10]	HOU Xiao-dong, CAI Bin-bin, JIN Wei-dong, DUAN Wang-wang. A New Weighted Evidence Fusion Algorithm Based on Evidence Distanceand Fuzzy Entropy Theory[J]. Journal of Guangxi Normal University(Natural Science Edition), 2015, 33(1): 45 -51 .

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

PDF (PC)

Abstract

Cite this article

share this article

References

Related Articles 7

Metrics

Comments

Recommended 10

[1]	GE Lina, LIU Jinhui. Privacy Preserving Method Based on k-isomorphism and Local Randomization [J]. Journal of Guangxi Normal University(Natural Science Edition), 2016, 34(4): 1-8.
[2]	TAN Hong-jian, YANG Ya-hui, DONG Ming-gang. Optimum Software Release Based on G-O Model and VaR Constraint [J]. Journal of Guangxi Normal University(Natural Science Edition), 2014, 32(2): 48-54.
[3]	HOU You-li, YANG Xiong. Technology Research about Two-stage Encryption Key of DatabaseSecurity Based on DES Encryption Algorithm [J]. Journal of Guangxi Normal University(Natural Science Edition), 2011, 29(3): 125-130.
[4]	HUANG Tian-qiang, LI Kai, ZHENG Zhi. Algorithm of Supervised Learning on Outlier Manifold [J]. Journal of Guangxi Normal University(Natural Science Edition), 2011, 29(3): 131-135.
[5]	WANG Han, WANG Xu’an, ZHOU Neng, LIU Yudong. Blockchain-based Public Verifiable Scheme for Sharing Data [J]. Journal of Guangxi Normal University(Natural Science Edition), 2020, 38(2): 1-7.
[6]	ZHANG Yongsheng, ZHU Wenjun, SHI Ruoqi, DU Zhenhua, ZHANG Rui, WANG Zhi. A Confidence-guided Hybrid Android Malware DetectionSystem with Multiple Heterogeneous Algorithms [J]. Journal of Guangxi Normal University(Natural Science Edition), 2020, 38(2): 19-28.
[7]	ZHOU Yan-yan, FENG Jia-li. Algorithm of Digital Audio Watermarking Based on Qualitative Mapping [J]. Journal of Guangxi Normal University(Natural Science Edition), 2011, 29(2): 200-204.