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.
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 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.
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.