计算机科学技术学报 ›› 2019,Vol. 34 ›› Issue (4): 901-923.doi: 10.1007/s11390-019-1949-1

所属专题： Computer Architecture and Systems

• • 上一篇    下一篇

对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
  • 收稿日期:2018-08-29 修回日期:2019-04-15 出版日期:2019-07-11 发布日期:2019-07-11
  • 通讯作者: Xin-Yu Feng E-mail:xyfeng@nju.edu.cn
  • 作者简介:Zi-Peng Zhang is a senior engineer of Huawei Technologies Co.,Ltd.,Shanghai.He received his Bachelor's and Ph.D.degrees in computer science from University of Science and Technology of China,Hefei,in 2010 and 2018 respectively.His research interests include program analysis,formal verification,and information flow control.
  • 基金资助:
    This work was supported in part by the National Natural Science Foundation of China under Grant No. 61632005.

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.

PDF (PC)

233

补充材料

1

进程间通信为应用程序间的信息交换提供了一种消息传递机制。长久以来，人们一直认为，IPC可能被恶意软件的开发者滥用，特别使用两个或更多的应用程序发起合谋泄露。在隐私保护方面，很多工作都集中在对单个应用程序造成的信息泄漏的检测上，而缺少有效的方法来防止这种由于进程间通信造成的的合谋泄漏。我们提出了一种基于信息流控制的混合方法来阻止这种合谋泄露。我们的方法结合了静态信息流分析技术和动态运行时检查技术。静态的信息流控制技术，可以防止单个进程导致的信息泄漏，运行检查可以阻止由于进程间通信导致的合谋泄露。这种组合的方法可以有效地减少纯动态检查带来的运行时开销，并且减少纯静态分析中的误报。我们基于一个抽象和简化的编程模型来说明这种方法，并且定义了一个新的无泄露性质作为我们的安全目标。我们使用基于Simulation的证明技术来证明本文方法的可靠性，即通过检查的程序一定满足无泄露性质。所有的证明都在Coq中进行了形式化，并生成了机器可检查证明。

关键词: 验证, 信息流控制, 安全保护, 静态分析

Abstract: 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] 陈金池, 秦逸, 王慧妍, 许畅. 上下文感知系统输入验证方法在模拟环境与物理环境中的对比[J]. 计算机科学技术学报, 2022, 37(1): 83-105.
[2] Zhi Ma, Lei Qiao, Meng-Fei Yang, Shao-Feng Li, Jin-Kun Zhang. 基于SPARCv8的实时嵌入式操作系统的异常管理验证[J]. 计算机科学技术学报, 2021, 36(6): 1367-1387.
[3] Jingwen Xu, Yanhong Huang, Jianqi Shi, Shengchao Qin. 面向队列系统决策建模与验证的多智能体空间逻辑[J]. 计算机科学技术学报, 2021, 36(6): 1231-1247.
[4] Zhao-Hui Li, Xin-Yu Feng. 对涉及所有权转移的上下文精化关系的验证[J]. 计算机科学技术学报, 2021, 36(6): 1342-1366.
[5] Gen Zhang, Peng-Fei Wang, Tai Yue, Xu Zhou, Kai Lu. MEBS：挖掘操作系统内核中的内存生命周期漏洞[J]. 计算机科学技术学报, 2021, 36(6): 1248-1268.
[6] Jung-Been Lee, Taek Lee, Hoh Peter In. 基于主题建模的软件资源库变更集预警优先级排序[J]. 计算机科学技术学报, 2020, 35(6): 1461-1479.
[7] Jun-Peng Zha, Xin-Yu Feng, Lei Qiao. SPARCv8代码的模块化验证[J]. 计算机科学技术学报, 2020, 35(6): 1382-1405.
[8] Feng-Juan Gao, Yu Wang, Lin-Zhang Wang, Zijiang Yang, Xuan-Dong Li. 缓冲区溢出静态警报的自动确认[J]. 计算机科学技术学报, 2020, 35(6): 1406-1427.
[9] Jia-Qi Yin, Hui-Biao Zhu, Yuan Fei. 利用TLA+规约和验证Zab协议[J]. 计算机科学技术学报, 2020, 35(6): 1312-1323.
[10] Qian-Qian Lin, Shu-Ling Wang, Bo-Hua Zhan, Bin Gu. 基于Uppaal和Simulink/Stateflow的RTPS协议的建模和验证[J]. 计算机科学技术学报, 2020, 35(6): 1324-1342.
[11] Hui-Na Chao, Hua-Wei Li, Xiaoyu Song, Tian-Cheng Wang, Xiao-Wei Li. 基于缺失场景的硬件属性评估和约束[J]. 计算机科学技术学报, 2020, 35(5): 1198-1216.
[12] Gökçer Peynirci, Mete Eminaǧaoǧlu, Korhan Karabulut. 基于IDF值差异的用于Android平台恶意软件检测的特征选择[J]. 计算机科学技术学报, 2020, 35(4): 946-962.
[13] Ling-Yun Situ, Student Member, CCF, Lin-Zhang Wang, Distinguished Member, CCF, Yang Liu, Member, ACM, IEEE, Bing Mao, Xuan-Dong Li, Fellow, CCF. 验证缺失的自动化检测与修复推荐[J]. 计算机科学技术学报, 2019, 34(5): 972-992.
[14] Ming-Zhe Zhang, Yun-Zhan Gong, Ya-Wen Wang, Da-Hai Jin. 使用规则导向的符号执行进行面向C语言的单元测试数据生成[J]. 计算机科学技术学报, 2019, 34(3): 670-689.
[15] Gianna Reggio, Maurizio Leotta, Filippo Ricca, Diego Clerissi. DUSM:一种基于严格用例和屏幕模型的需求规范和细化的方法[J]. 计算机科学技术学报, 2018, 33(5): 918-939.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] C.Y.Chung; 华宣仁;. A Chinese Information Processing System[J]. , 1986, 1(2): 15 -24 .
[2] 章萃; 赵沁平; 徐家福;. Kernel Language KLND[J]. , 1986, 1(3): 65 -79 .
[3] 黄学东; 蔡莲红; 方棣棠; 迟边进; 周立; 蒋力;. A Computer System for Chinese Character Speech Input[J]. , 1986, 1(4): 75 -83 .
[4] 唐同诰; 招兆铿;. Stack Method in Program Semantics[J]. , 1987, 2(1): 51 -63 .
[5] 夏培肃; 方信我; 王玉祥; 严开明; 张廷军; 刘玉兰; 赵春英; 孙继忠;. Design of Array Processor Systems[J]. , 1987, 2(3): 163 -173 .
[6] 孙永强; 陆汝占; 黄小戎;. Termination Preserving Problem in the Transformation of Applicative Programs[J]. , 1987, 2(3): 191 -201 .
[7] 林琦; 夏培肃;. The Design and Implementation of a Very Fast Experimental Pipelining Computer[J]. , 1988, 3(1): 1 -6 .
[8] 谢立; 陈珮珮; 杨培根; 孙钟秀;. The Design and Implementation of an OA System ZGL1[J]. , 1988, 3(1): 75 -80 .
[9] 罗银芳;. Algorithm and Implementation of Parallel Multiplication in a Mixed Number System[J]. , 1988, 3(3): 203 -213 .
[10] 陈国良;. A Partitioning Selection Algorithm on Multiprocessors[J]. , 1988, 3(4): 241 -250 .
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持：support@magtech.com.cn
总访问量：