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 条

[41] Concurrency bugs in multithreaded software: modeling and analysis using Petri nets [J].

Hongwei Liao ;

Yin Wang ;

Hyoun Kyu Cho ;

Jason Stanley ;

Terence Kelly ;

Stéphane Lafortune ;

Scott Mahlke ;

Spyros Reveliotis .

Discrete Event Dynamic Systems, 2013, 23 :157-195

[42] Modeling of an automated integral logistics system using colored petri nets [J].

Ochoa, Maria P. ;

Davila, Julian .

INGENIERIA Y COMPETITIVIDAD, 2019, 21 (01) :63-71

[43] Modeling and Analysis of Authentication Protocols. Using Colored Petri Nets [J].

Xu, Yang ;

Xie, Xiaoyao .

PROCEEDINGS OF THE 3RD INTERNATIONAL CONFERENCE ON ANTI-COUNTERFEITING, SECURITY, AND IDENTIFICATION IN COMMUNICATION, 2009, :443-448

[44] Synchronous and asynchronous communications in composable parameterized high-level Petri nets [J].

Devillers, R ;

Klaudel, H .

FUNDAMENTA INFORMATICAE, 2005, 66 (03) :221-257

[45] Management of e-learning processes with high-level Petri nets [J].

Keferstein, Kirsten ;

Mevius, Marco ;

Oberweis, Andreas .

PROCEEDINGS OF THE EIGHTH IASTED INTERNATIONAL CONFERENCE ON COMPUTERS AND ADVANCED TECHNOLOGY IN EDUCATION, 2005, :347-352

[46] OPENET: Ontology-based engine for high-level Petri nets [J].

Vidal, Juan C. ;

Lama, Manuel ;

Bugarin, Alberto .

EXPERT SYSTEMS WITH APPLICATIONS, 2010, 37 (09) :6493-6509

[47] Bounded Model Checking High Level Petri Nets in PIPE plus Verifier [J].

Liu, Su ;

Zeng, Reng ;

Sun, Zhuo ;

He, Xudong .

FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2014, 2014, 8829 :348-363

[48] Bottleneck Detection in Job Shop Production by High-Level Petri Nets [J].

Esmaeeli, Hamid ;

Aleahmad, Matin .

PROCEEDINGS OF 2019 15TH IRAN INTERNATIONAL INDUSTRIAL ENGINEERING CONFERENCE (IIIEC), 2019, :178-183

[49] Using Stochastic Petri Nets for Level-Crossing Collision Risk Assessment [J].

Ghazel, Mohamed .

IEEE TRANSACTIONS ON INTELLIGENT TRANSPORTATION SYSTEMS, 2009, 10 (04) :668-677

[50] Modeling and Analysis of Protein Synthesis and DNA Mutation Using Colored Petri Nets [J].

Yang, Jinliang ;

Pu, Haitao ;

Lian, Jian ;

Gu, Jason ;

Fan, Mingqu .

IEEE ACCESS, 2018, 6 :22386-22400

← 1 2 3 4 5 →