Modeling and Analyzing the Android Permission Framework using High Level Petri Nets

被引:2
作者
He, Xudong [1 ]
机构
[1] Florida Int Univ, Sch Comp & Informat Sci, Miami, FL 33199 USA
来源
2017 IEEE INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS) | 2017年
关键词
Android permission; security; formal methods; high level Petri nets; modeling; verification and validation;
D O I
10.1109/QRS.2017.34
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Android permission framework is a part of Android OS to enforce secure cross application communication. However the android permission framework is very complex, and its descriptions are scattered in dozens of webpages. It is very difficult to understand the relationships among multiple permission levels and their potential vulnerabilities. This paper presents a formal model of the Android permission framework using high level Petri nets. The model precisely defines the complex relationships among different levels of permissions. The model is constructed incrementally and thus is easily adaptable to future changes. The model building process is supported by our tool environment PIPE+, which further provides several analysis techniques. Simulation results for several scenarios that obey and violate the permission requirements are discussed.
引用
收藏
页码:232 / 239
页数:8
相关论文
共 50 条
[21]   General composition for high level Petri nets and its properties [J].
Petko, Ivan ;
Hudak, Stefan .
OPEN COMPUTER SCIENCE, 2012, 2 (03) :222-235
[22]   Development of an international standard for high-level Petri nets [J].
Billington, J .
THIRD IEEE INTERNATIONAL SOFTWARE ENGINEERING STANDARDS SYMPOSIUM AND FORUM (ISESS 97) - EMERGING INTERNATIONAL STANDARDS, PROCEEDINGS, 1997, :155-162
[23]   PUTTING HIGH-LEVEL PETRI NETS TO WORK IN INDUSTRY [J].
VANDERAALST, WMP .
COMPUTERS IN INDUSTRY, 1994, 25 (01) :45-54
[24]   Petri Nets Based Max-flow/Min-cut Modeling and Analyzing [J].
Zou, Zheng ;
Liu, Shi-Jian ;
Pan, Jeng-Shyang .
JOURNAL OF INTERNET TECHNOLOGY, 2020, 21 (04) :919-928
[25]   Modeling of a transmission network protection system using Petri nets [J].
Tang, JX ;
Wang, FM .
ELECTRIC POWER SYSTEMS RESEARCH, 1998, 44 (03) :175-181
[26]   Modeling resource management in cellular systems using Petri nets [J].
JaimesRomero, FJ ;
MunozRodriguez, D ;
Molina, C ;
Tawfik, H .
IEEE TRANSACTIONS ON VEHICULAR TECHNOLOGY, 1997, 46 (02) :298-312
[27]   Hybrid modeling of power system using hybrid Petri nets [J].
Paruchuri, VK ;
Davari, A ;
Feliachi, A .
PROCEEDINGS OF THE THIRTY-SEVENTH SOUTHEASTERN SYMPOSIUM ON SYSTEM THEORY, 2005, :221-224
[28]   Modeling and recognition of hand gesture using colored Petri nets [J].
Nam, Y ;
Wohn, K ;
Lee-Kwang, H .
IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 1999, 29 (05) :514-521
[29]   Modeling and Analysis of a Telesurgery Environment Using Stochastic Petri Nets [J].
Rocha Jr, Vamberto ;
Araujo, Jean ;
Nogueira, Bruno ;
Andrade, Ermeson .
IEEE LATIN AMERICA TRANSACTIONS, 2023, 21 (10) :1073-1080
[30]   Modeling and simulation of products' life cycles using petri nets [J].
Murayama, T ;
Hatakenaka, S ;
Namito, M ;
Shu, LH .
INTERNATIONAL JOURNAL OF THE JAPAN SOCIETY FOR PRECISION ENGINEERING, 1999, 33 (04) :373-375