Enhancement and formal verification of the ICC mechanism with a sandbox approach in android system

Jiaqi Yin, Sini Chen, Yixiao Lv, Huibiao Zhu

Research output: Contribution to journalArticlepeer-review

Abstract

Inter-Component Communication (ICC) plays a crucial role in facilitating information exchange and functionality integration within the complex ecosystem of Android systems. However, the security and safety implications arising from ICC interactions pose significant challenges. This paper is an extended work building upon our previously published research that focuses on the verification of safety properties in the ICC mechanism. We address the previously observed issues of data leakage and privilege escalation by incorporating a sandbox mechanism and permission control. The sandbox mechanism provides an isolated and controlled environment in which ICC components can operate while permission control mechanisms are introduced to enforce fine-grained access controls, ensuring that only authorized entities have access to sensitive resources. We further leverage formal methods, specifically communicating sequential processes (CSP), to verify several properties of the enhanced ICC mechanism. By employing CSP, we aim to systematically model and analyze the flow of information, the behavior of components, and the potential vulnerabilities associated with the enhanced ICC mechanism. The verification results highlight the effectiveness of our approach in enhancing the security and reliability of ICC mechanisms, ultimately contributing to the development of safer and more trustworthy Android Systems.

Original languageEnglish
Pages (from-to)1175-1202
Number of pages28
JournalSoftware Quality Journal
Volume32
Issue number3
DOIs
StatePublished - Sep 2024

Keywords

  • Android
  • Communicating Sequential Process (CSP)
  • Inter-App Communication (IAC)
  • Inter-Component Communication (ICC)
  • PAT with C#

Fingerprint

Dive into the research topics of 'Enhancement and formal verification of the ICC mechanism with a sandbox approach in android system'. Together they form a unique fingerprint.

Cite this