Compositional Analysis of Android Inter-Application Vulnerabilities (COVERT)

COVERT is a tool for compositional verification of Android inter-application vulnerabilities. It automatically identifies vulnerabilities that occur due to the interaction of apps comprising a system. Subsequently, it determines whether it is safe for a bundle of apps, requiring certain permissions and potentially interacting with each other, to be installed together. 


Approach Overview

COVERT consists of two components: (1) Model Extractor that uses static code analysis techniques to elicit formal specifications (models) of the apps comprising a system as well as the phone configuration; and (2) Formal Analyzer that is intended to use lightweight formal analysis techniques to verify certain properties (e.g., known security vulnerability patterns) in the extracted specifications.


Empirical Evaluation

Our experimental subjects are a set of Android apps drawn from three different app repositories:

  1. Popular: A snapshot of the top 80 popular free apps, available on the Google Play in late November 2013. (Extracted Models | Alloy Results | ICC Results)
  2. Open Source: More than 100 apps collected from the F-Droid open source repository. (List of appsExtracted Models | Alloy Results | ICC Results)
  3. Malicious: A collection of 44 malicious apps identified by the MalGenome project.

Tool

COVERT Tool is publicly available from the Tool page.