A type and effect system for activation flow of components in Android programs

被引：11

作者：

Choi, Kwanghoon ^{[1
]}

Chang, Byeong-Mo ^{[2
]}

机构：

[1] Yonsei Univ, Wonju, South Korea

[2] Sookmyung Womens Univ, Seoul, South Korea

来源：

INFORMATION PROCESSING LETTERS | 2014年 / 114卷 / 11期

基金：

新加坡国家研究基金会;

关键词：

Android; !text type='Java']Java[!/text; Program analysis; Control flow; Formal semantics; !text type='JAVA']JAVA[!/text;

D O I：

10.1016/j.ipl.2014.05.011

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

This paper proposes a type and effect system for analyzing activation flow between components through intents in Android programs. The activation flow information is necessary for all Android analyses such as a secure information flow analysis for Android programs. We first design a formal semantics for a core of featherweight Android/Java, which can address interaction between components through intents. Based on the formal semantics, we design a type and effect system for analyzing activation flow between components and demonstrate the soundness of the system. (C) 2014 Elsevier B.V. All rights reserved.

引用

页码：620 / 627

页数：8

共 10 条

[1] [Anonymous], 1999, TYPE EFFECT SYSTEMS
[2] [Anonymous], 2011, P 9 ANN INT C MOB SY
[3] [Anonymous], 2009, Technical Report CS-TR-4991
[4] [Anonymous], 2012, MOBILE SECURITY TECH
[5] Verifying Pointer and String Analyses with Region Type Systems
Beringer, Lennart
Grabowski, Robert
Hofmann, Martin
[J]. LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING (LPAR-16), 2010, 6355 : 82 - 102
[6] Choi K., 2014, TRMAR20141 YONS U
[7] Christensen AS, 2003, LECT NOTES COMPUT SC, V2694, P1
[8] Featherweight Java']Java: A minimal core calculus for Java']Java and GJ
Igarashi, A
Pierce, BC
Wadler, P
[J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001, 23 (03): : 396 - 450
[9] Parameterized object sensitivity for points-to analysis for Java']Java
Milanova, A
Rountev, A
Ryder, BG
[J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2005, 14 (01) : 1 - 41
[10] Octeau D., 2013, 22 USENIX SEC S, P543

← 1 →