A Timed-Permission Access Control Profile Within MARTE
Android applications often interact through inter-component communication (ICC), which can be exploited for privilege escalation attacks. Traditional permission-based access control (PBAC) mechanisms lack the ability to express temporal constraints, making them insufficient for preventing time-sensitive threats. This paper introduces a novel methodology based on the MARTE-TPAM profile, which extends PBAC with explicit temporal semantics and conforms to ISO/IEC 29146:2016 access management standards. We define a structured TPAM domain model, develop a UML-based profile for semi-formal modeling, and propose a Z-based formal verification workflow. Through detailed modeling and formal analysis of an Android news recommendation scenario, we demonstrate that our method enables rigorous detection of unauthorized privilege flows that violate both permission and timing policies. The proposed approach supports early-stage access policy validation and provides a mathematically grounded foundation for Android security assurance. Compared to existing permission-based models, our approach offers enhanced expressiveness and early-stage validation capability by explicitly capturing temporal constraints in both graphical and formal specifications.
Authors
- Xinwen Hu (ORCID: https://orcid.org/0000-0001-9566-5424)
Institutions
- Hunan Normal University (CN)
Publication Details
- Journal
- IEEE Access
- Published
- 2025-01-01
- DOI
- https://doi.org/10.1109/access.2025.3596928
- Primary Topic
- Radiation Effects in Electronics
- Type
- article
- Field-Weighted Citation Impact
- 0.00