Journal of Computer Science and Technology ›› 2019, Vol. 34 ›› Issue (4): 901-923.doi: 10.1007/s11390-019-1949-1

Special Issue: Computer Architecture and Systems

• Regular Paper • Previous Articles     Next Articles

A Lightweight Dynamic Enforcement of Privacy Protection for Android

Zi-Peng Zhang1, Ming Fu2, Xin-Yu Feng3,*, Member, CCF, ACM   

  1. 1 School of Computer Science and Technology, University of Science and Technology of China, Hefei 230026, China;
    2 OS Kernel Laboratory, Huawei Technologies Co., Ltd., Shanghai 200135, China;
    3 State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210023, China
  • Received:2018-08-29 Revised:2019-04-15 Online:2019-07-11 Published:2019-07-11
  • Contact: Xin-Yu Feng E-mail:xyfeng@nju.edu.cn
  • Supported by:
    This work was supported in part by the National Natural Science Foundation of China under Grant No. 61632005.

Inter-process communication (IPC) provides a message passing mechanism for information exchange between applications. It has been long believed that IPCs can be abused by malware writers to launch collusive information leak using two or more applications. Much work on privacy protection focuses on the simple information leak caused by the individual applications and lacks effective approaches to preventing the collusive information leak caused by IPCs between multiple processes. In this paper, we propose a hybrid approach to prevent the collusive information leak based on information flow control. Our approach combines static information flow analysis and dynamic runtime checking together. Information leak caused by individual processes is prevented through static information flow control, and dynamic checking is done at runtime to prevent the collusive information leak. Such a combination may effectively reduce the runtime overhead of pure dynamic checking, and reduce false-alarms in pure static analysis. We develop this approach based on an abstract and simplified programming model, and formalize a novel definition of the leak-freedom property as our target security property. A simulation-based proof technique is used to prove that our approach is able to guarantee leak-freedom. All proofs are mechanized in Coq.

Key words: privacy protection, dynamic runtime checking, static information flow control, Android, verification

[1] Arzt S, Rasthofer S, Fritz C, Bodden E, Bartel A, Klein J, le Traon Y, Octeau D, McDaniel P. FlowDroid:Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps. In Proc. the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2014, pp.259-269.
[2] Enck W, Gilbert P, Chun B G, Cox L P, Jung J, McDaniel P, Sheth A N. TaintDroid:An information-flow tracking system for realtime privacy monitoring on smartphones. In Proc. the 9th USENIX Conference on Operating Systems Design and Implementation, October 2010, pp.393-407.
[3] Gibler C, Crussell J, Erickson J, Chen H. AndroidLeaks:Automatically detecting potential privacy leaks in Android applications on a large scale. In Proc. the 5th International Conference on Trust and Trustworthy Computing, June 2012, pp.291-307.
[4] Sakamoto S, Okuda K, Nakatsuka R, Yamauchi T. DroidTrack:Tracking information diffusion and preventing information leakage on Android. In Proc. the 2013 Multimedia and Ubiquitous Engineering, May 2013, pp.243-251.
[5] Sun M, Wei T, Lui J C S. TaintART:A practical multilevel information-flow tracking system for Android runtime. In Proc. the 2016 ACM SIGSAC Conference on Computer and Communications Security, October 2016, pp.331-342.
[6] Xia M, Gong L, Lyu Y, Qi Z, Liu X. Effective real-time Android application auditing. In Proc. the 2015 IEEE Symposium on Security and Privacy, May 2015, pp.899-914.
[7] Yang Z, Yang M, Zhang Y, Gu G, Ning P, Wang X S. AppIntent:Analyzing sensitive data transmission in Android for privacy leakage detection. In Proc. the 2013 ACM SIGSAC Conference on Computer and Communications Security, November 2013, pp.1043-1054.
[8] Zhao Z, Colon O F C. "TrustDroidTM":Preventing the use of SmartPhones for information leaking in corporate networks through the used of static analysis taint tracking. In Proc. the 7th International Conference on Malicious and Unwanted Software, October 2012, pp.135-143.
[9] Octeau D, McDaniel P, Jha S, Bartel A, Bodden E, Klein J, le Traon Y. Effective inter-component communication mapping in Android with Epicc:An essential step towards holistic security analysis. In Proc. the 22nd USENIX Conference on Security, August 2013, pp.543-558.
[10] Volpano D M, Smith G. Probabilistic noninterference in a concurrent language. In Proc. the 11th IEEE Computer Security Foundations Workshop, June 1998, pp.34-43.
[11] Smith G, Volpano D M. Secure information flow in a multi-threaded imperative language. In Proc. the 25th ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 1998, pp.355-364.
[12] Sabelfeld A, Sands D. Probabilistic noninterference for multi-threaded programs. In Proc. the 13th IEEE Computer Security Foundations Workshop, July 2000, pp.200-214.
[13] Zdancewic S, Myers A C. Observational determinism for concurrent program security. In Proc. the 16th IEEE Computer Security Foundations Workshop, June 2003, pp.29-43.
[14] Mantel H, Sudbrock H. Flexible scheduler-independent security. In Proc. the 15th European Symposium on Research in Computer Security, September 2010, pp.116-133.
[15] Mantel H, Sands D, Sudbrock H. Assumptions and guarantees for compositional noninterference. In Proc. the 24th IEEE Computer Security Foundations Symposium, June 2011, pp.218-232.
[16] Goguen J A, Meseguer J. Security policies and security models. In Proc. the 1982 IEEE Symposium on Security and Privacy, April 1982, pp.11-20.
[17] Goguen J A, Meseguer J. Unwinding and inference control. In Proc. the 1984 IEEE Symposium on Security and Privacy, April 1984, pp.75-87.
[18] Liang H, Feng X, Fu M. A rely-guarantee-based simulation for verifying concurrent program transformations. In Proc. the 39th ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2012, pp.455-468.
[19] Liang H, Feng X. Modular verification of linearizability with non-fixed linearization points. In Proc. the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2013, pp.459-470.
[20] Zhang Z, Feng X. AndroidLeaker:A hybrid checker for collusive leak in Android applications. In Proc. the 3rd International Symposium on Dependable Software Engineering Theories, Tools, and Applications, October 2017, pp.164-180.
[21] Xiao X, Tillmann N, Fähndrich M, de Halleux J, Moskal M. User-aware privacy control via extended static-informationflow analysis. In Proc. the 2012 IEEE/ACM International Conference on Automated Software Engineering, September 2012, pp.80-89.
[22] Mann C, Starostin A. A framework for static detection of privacy leaks in Android applications. In Proc. the 27th Annual ACM Symposium on Applied Computing, March 2012, pp.1457-1462.
[23] Kim J, Yoon Y, Yi K, Shin J. ScanDal:Static analyzer for detecting privacy leaks in Android applications. In Proc. the 2012 Mobile Security Technologies, May 2012.
[24] Lu L, Li Z, Wu Z, Lee W, Jiang G. CHEX:Statically vetting Android apps for component hijacking vulnerabilities. In Proc. the 2012 ACM Conference on Computer and Communications Security, October 2012, pp.229-240.
[25] Xu R, Saïdi H, Anderson R. Aurasium:Practical policy enforcement for Android applications. In Proc. the 21st USENIX Conference on Security Symposium, August 2012, pp.539-552.
[26] Yang Z, Yang M. LeakMiner:Detect information leakage on Android with static taint analysis. In Proc. the 3rd World Congress on Software Engineering, November 2012, pp.101-104.
[27] Chin E, Felt A P, Greenwood K, Wagner D. Analyzing inter-application communication in Android. In Proc. the 9th International Conference on Mobile Systems, Applications, and Services, June 2011, pp. 239-252.
[28] Nadkarni A, Enck W. Preventing accidental data disclosure in modern operating systems. In Proc. the 2013 ACM Conference on Computer and Communications Security, November 2013, pp.1029-1042.
[29] Felt A P, Wang H J, Moshchuk A, Hanna S, Chin E. Permission re-delegation:Attacks and defenses. In Proc. the 20th USENIX Conference on Security, August 2011, Article No. 22.
[30] Chaudhuri A. Language-based security on Android. In Proc. the 2009 Workshop on Programming Languages and Analysis for Security, June 2009, pp.1-7.
[31] Russo A, Sabelfeld A. Securing interaction between threads and the scheduler. In Proc. the 19th IEEE Computer Security Foundations Workshop, July 2006, pp.177-189.
[32] Russo A, Sabelfeld A. Securing interaction between threads and the scheduler in the presence of synchronization. The Journal of Logic and Algebraic Programming, 2009, 78(7):593-618.
[33] Askarov A, Chong S, Mantel H. Hybrid monitors for concurrent noninterference. In Proc. the 28th IEEE Computer Security Foundations Symposium, July 2015, pp.137-151.
[34] Russo A, Sabelfeld A. Security for multithreaded programs under cooperative scheduling. In Proc. the 6th International Andrei Ershov Memorial Conference on Perspectives of Systems Informatics, June 2006, pp.474-480.
[35] Costanzo D, Shao Z, Gu R. End-to-end verification of information-flow security for C and assembly programs. In Proc. the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2016, pp.648-664.
[1] Jun-Peng Zha, Xin-Yu Feng, Lei Qiao. Modular Verification of SPARCv8 Code [J]. Journal of Computer Science and Technology, 2020, 35(6): 1382-1405.
[2] Jia-Qi Yin, Hui-Biao Zhu, Yuan Fei. Specification and Verification of the Zab Protocol with TLA+ [J]. Journal of Computer Science and Technology, 2020, 35(6): 1312-1323.
[3] Qian-Qian Lin, Shu-Ling Wang, Bo-Hua Zhan, Bin Gu. Modelling and Verification of Real-Time Publish and Subscribe Protocol Using UPPAAL and Simulink/Stateflow [J]. Journal of Computer Science and Technology, 2020, 35(6): 1324-1342.
[4] Hui-Na Chao, Hua-Wei Li, Xiaoyu Song, Tian-Cheng Wang, Xiao-Wei Li. Evaluating and Constraining Hardware Assertions with Absent Scenarios [J]. Journal of Computer Science and Technology, 2020, 35(5): 1198-1216.
[5] Gökçer Peynirci, Mete Eminaǧaoǧlu, Korhan Karabulut. Feature Selection for Malware Detection on the Android Platform Based on Differences of IDF Values [J]. Journal of Computer Science and Technology, 2020, 35(4): 946-962.
[6] Chong Wang, Nasro Min-Allah, Bei Guan, Yu-Qi Lin, Jing-Zheng Wu, Yong-Ji Wang. An Efficient Approach for Mitigating Covert Storage Channel Attacks in Virtual Machines by the Anti-Detection Criterion [J]. Journal of Computer Science and Technology, 2019, 34(6): 1351-1365.
[7] Lei Cui, Youyang Qu, Mohammad Reza Nosouhi, Shui Yu, Jian-Wei Niu, Gang Xie. Improving Data Utility Through Game Theory in Personalized Differential Privacy [J]. Journal of Computer Science and Technology, 2019, 34(2): 272-286.
[8] Li Li, Tegawendé F. Bissyandé, Hao-Yu Wang, Jacques Klein. On Identifying and Explaining Similarities in Android Apps [J]. Journal of Computer Science and Technology, 2019, 34(2): 437-455.
[9] Yifan Wu, Fan Yang, Yong Xu, Haibin Ling. Privacy-Protective-GAN for Privacy Preserving Face De-Identification [J]. Journal of Computer Science and Technology, 2019, 34(1): 47-60.
[10] Seilendria A. Hadiwardoyo, Subhadeep Patra, Carlos T. Calafate, Juan-Carlos Cano, Pietro Manzoni. An Intelligent Transportation System Application for Smartphones Based on Vehicle Position Advertising and Route Sharing in Vehicular Ad-Hoc Networks [J]. , 2018, 33(2): 249-262.
[11] Yu-Tao Liu, Dong Du, Yu-Bin Xia, Hai-Bo Chen, Bin-Yu Zang, Zhenkai Liang. SplitPass: A Mutually Distrusting Two-Party Password Manager [J]. , 2018, 33(1): 98-115.
[12] Li Li, Daoyuan Li, Tegawendé F. Bissyandé, Jacques Klein, Haipeng Cai, David Lo, Yves Le Traon. On Locating Malicious Code in Piggybacked Android Apps [J]. , 2017, 32(6): 1108-1124.
[13] An Liu, Zhi-Xu Li, Guan-Feng Liu, Kai Zheng, Min Zhang, Qing Li, Xiangliang Zhang. Privacy-preserving Task Assignment in Spatial Crowdsourcing [J]. , 2017, 32(5): 905-918.
[14] Wen-Min Li, Xue-Lei Li, Qiao-Yan Wen, Shuo Zhang, Hua Zhang. Flexible CP-ABE Based Access Control on Encrypted Data for Mobile Users in Hybrid Cloud System [J]. , 2017, 32(5): 974-990.
[15] Peng-Yi Hao, Yang Xia, Xiao-Xin Li, Sei-ichiro Kamata, Sheng-Yong Chen. Discriminative Histogram Intersection Metric Learning and Its Applications [J]. , 2017, 32(3): 507-519.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] Liu Mingye; Hong Enyu;. Some Covering Problems and Their Solutions in Automatic Logic Synthesis Systems[J]. , 1986, 1(2): 83 -92 .
[2] Shen Li; Stephen Y.H.Su;. Generalized Parallel Signature Analyzers with External Exclusive-OR Gates[J]. , 1986, 1(4): 49 -61 .
[3] Gong Zhenhe;. On Conceptual Model Specification and Verification[J]. , 1987, 2(1): 35 -50 .
[4] Xia Peisu; Fang Xinwo; Wang Yuxiang; Yan Kaiming; Zhang Tingjun; Liu Yulan; Zhao Chunying; Sun Jizhong;. Design of Array Processor Systems[J]. , 1987, 2(3): 163 -173 .
[5] Wang Yongcheng;. Automatic Extraction of Words from Chinese Textual Data[J]. , 1987, 2(4): 287 -291 .
[6] Li Renwei;. Soundness and Completeness of Kung s Reasoning Procedure[J]. , 1988, 3(1): 7 -15 .
[7] Bao Feng;. On the Condition for FSM Being a Scrambler[J]. , 1988, 3(1): 70 -74 .
[8] Zhang Yan; He Jichao;. Data Dependencies in Database with Incomplete Information[J]. , 1988, 3(2): 131 -138 .
[9] Chen Haibo; Ci Yungui;. Optimization for the Parallel Execution of Non-DO Loops under Leading Iteration Model[J]. , 1988, 3(4): 263 -272 .
[10] Lian Lin; Zhang Yili; Tang Changjie;. A Non-Recursive Algorithm Computing Set Expressions[J]. , 1988, 3(4): 310 -316 .

ISSN 1000-9000(Print)

         1860-4749(Online)
CN 11-2296/TP

Home
Editorial Board
Author Guidelines
Subscription
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
Tel.:86-10-62610746
E-mail: jcst@ict.ac.cn
 
  Copyright ©2015 JCST, All Rights Reserved