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.

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.