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 条
  • [31] FORMALIZING DISTRIBUTED SELF-ADAPTIVE SYSTEMS USING HIGH-LEVEL PETRI NETS
    Capra, Lorenzo
    Camilli, Matteo
    [J]. PROCEEDINGS OF THE 2019 SUMMER SIMULATION CONFERENCE (SUMMERSIM '19), 2019,
  • [32] Rapid prototyping of distributed computing systems using high-level Petri nets with objects
    Mikolajczak, B
    [J]. PROCEEDINGS OF THE HIGH-PERFORMANCE COMPUTING (HPC'98), 1998, : 388 - 393
  • [33] Modeling of safe timed Petri nets by two -level (max, plus ) automata
    Komenda, Jan
    Zorzenon, Davide
    Balun, Jiri
    [J]. IFAC PAPERSONLINE, 2022, 55 (28): : 212 - 219
  • [34] PermGuard: A Scalable Framework for Android Malware Detection Using Permission-to-Exploitation Mapping
    Prasad, Arvind
    Chandra, Shalini
    Uddin, Mueen
    Al-Shehari, Taher
    Alsadhan, Nasser A.
    Ullah, Syed Sajid
    [J]. IEEE ACCESS, 2025, 13 : 507 - 528
  • [35] Simulating Train Dispatching Logic with High-Level Petri Nets
    Jeremic, Dusan
    Milinkovic, Sanjin
    Kasalica, Sandra
    [J]. TEHNICKI VJESNIK-TECHNICAL GAZETTE, 2021, 28 (02): : 639 - 648
  • [36] High-Level Petri Nets Modules for Embedded Controllers Design
    Ribeiro, Jose
    Melicio, Fernando
    Gomes, Luis
    [J]. PROCEEDINGS 2015 IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2015, : 876 - 882
  • [37] Modeling, scheduling and simulation of product development process by extended stochastic high-level evaluation Petri nets
    Yan, HS
    Wang, Z
    Jiao, XC
    [J]. ROBOTICS AND COMPUTER-INTEGRATED MANUFACTURING, 2003, 19 (04) : 329 - 342
  • [38] Microscopic Modeling of a Signalized Traffic Intersection Using Timed Petri Nets
    Wang, Jianqiang
    Yan, Jiaxiang
    Li, Lingxi
    [J]. IEEE TRANSACTIONS ON INTELLIGENT TRANSPORTATION SYSTEMS, 2016, 17 (02) : 305 - 312
  • [39] Concurrency bugs in multithreaded software: modeling and analysis using Petri nets
    Liao, Hongwei
    Wang, Yin
    Cho, Hyoun Kyu
    Stanley, Jason
    Kelly, Terence
    Lafortune, Stephane
    Mahlke, Scott
    Reveliotis, Spyros
    [J]. DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2013, 23 (02): : 157 - 195
  • [40] Modeling of Power-supply Subsystems of Microgrid Using Petri Nets
    Khyzhniak, Tetiana
    Kolesnyk, Viktor
    [J]. 2013 IEEE XXXIII INTERNATIONAL SCIENTIFIC CONFERENCE ELECTRONICS AND NANOTECHNOLOGY (ELNANO), 2013, : 391 - 395