The Android application framework has a pervasive presence. In early 2021, Android has over 70 % share of the operating system mobile market (according to GlobalStats). Components are the main building blocks of Android Applications. These blocks communicate via a rich Inter-Component Communication (ICC) model rather than the traditional inter-process communication model. Intents, Intent-filters, and their Intents resolution (matching) algorithm are main elements of the ICC. However, the Intent resolution algorithm is not robust enough and has flaws that can lead to security breaches. In this paper, we present DLAIR, as an enrichment of the Intent resolution algorithm to overcome its security issues. To this end, we start by presenting a formal model to express and validate the ICC semantics. This includes defining key properties guaranteeing consistent and realistic semantic states. We then demonstrate how the semantics can be used to formally validate ICC aspects and to express and check ICC system updates. We verified our proposed model and all its lemmas and theorems in the Coq Proof Assistant, a machine-assisted verification tool. We extend our semantics to develop DLAIR which is assisted by a heuristic, and lightweight tool, LekInt. This tool identifies suspicious execution paths responsible for intent based sensitive user-information leakage. On a dataset of 2000 real-world apps, we evaluated LekInt against Flowdroid, a state-of-the-art information leakage analysis tool. Experiments show that LekInt is more effective and efficient than Flowdroid which has a higher false-negative rate and lower false-positive rate than LekInt. Considering the dynamic context in which LekInt is designed to work, the advantage of efficiency overcomes the disadvantage of higher false-negative.

Deduplication is a widely used technology to reduce the storage and communication cost for cloud storage services. For any cloud infrastructure, data confidentiality is one of the primary concerns. Data confidentiality can be achieved via user-side encryption. However, conventional encryption mechanism is at odds with deduplication. Developing a user-side encryption mechanism with deduplication is a vital research topic. Existing state-of-the-art solutions in security of deduplication are vulnerable to dictionary attacks and tag inconsistency anomaly. In this paper, we present SPARK, a novel approach for secure pseudorandom key-based encryption for deduplicated storage. SPARK achieves semantic security along with deduplication. Security analysis proves that SPARK is secure against dictionary attacks and tag inconsistency anomaly. As a proof of concept, we implement SPARK in realistic environment and demonstrate its efficiency and effectiveness.