Title: Certifying the Security of Android Applications with Cassandra


Modern mobile devices store and process an abundance of data. Although
many users consider some of this data to be private, they do not yet
obtain satisfactory support for controlling what applications might do
with their data. In fact, many Android applications reveal private 
data of users to untrusted third parties without their consent.

Our Certifying App Store for Android, Cassandra, enables users of
Android mobile devices to check whether applications comply with their
personal privacy requirements before installing the applications.

Cassandra implements a type-based information flow analysis of Dalvik
bytecode. This analysis is semantically justified: The notion of 
security is specified as a noninterference-like security condition 
that is defined in terms of a formal semantics of Dalvik bytecode. We 
have proven that the analysis is sound. To the best of our knowledge, 
Cassandra is the first information flow analysis tool for Android with 
a soundness result.

Cassandra allows end users of mobile devices to create security 
policies that capture their individual privacy requirements. To make 
this possible also for non-experts, Cassandra provides a policy editor 
that allows users to create security policies in terms of intuitively 
comprehensible categories of data. Cassandra displays the flows of 
information in apps graphically in terms of these categories. This 
allows users to make informed decisions about whether they want to 
install a certain app.