COVERT: Compositional Analysis of Android Inter-Application Vulnerabilities

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.

[Covert picture]

Tool

COVERT tool is implemented in two layers: the back-end that performs analysis on the apps to find potential vulnerabilities, and the front-end that provides an interactive environment intended for use by the end users.
[Covert architecture]

Back-end Tool (Covert Engine). The core components of COVERT tool that analyze the apps to detect security vulnerability issues are implemented in the back-end layer. As depicted in Figure above, this layer consists of two modules: Model Extractor that leverages static analysis techniques to automatically extract an abstract formal model of Android apps, and Formal Analyzer that is intended to use lightweight formal analysis techniques to find vulnerabilities in the extracted app models.

Front-end Tools. In order to facilitate the end-user interactions with COVERT back-end engine, we implemented client applications for different platforms: Desktop Application, which is a stand- alone tool that calls back-end components and visualizes the generated results. Mobile and Web-based applications that work together to analyze the installed apps in a mobile device and show the vulnerability report on web browsers.

Demo

This video demonstrates the main features of COVERT tool.

Download and Installation

COVERT Back-end as well as the desktop Front-end tool for Windows and Mac are available here for download.The user manual is also downloadable from this link.

Empirical Evaluation

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

Publications

More details about COVERT can be found in our publication:

[seal's logo]
[uci's logo]