An Object-Sensitive Type-Based Information-Flow Analysis for Android Applications


Mobile devices are used to store a wide variety of highly personal data, 
such as the user's pictures, personal contacts, calendar entries, text 
messages, and call history. A natural concern is whether this data remains 
confidential. Studies have shown that, in fact, applications installed 
on mobile devices reveal sensitive information, either on purpose or due 
to the carelessness of the developer.

Cassandra is an app store for Android, the most widely used mobile 
operating system, that enables a user to ensure before installing an 
application that it does not reveal information he considers to be 
private. However, the security analysis implemented in Cassandra so 
far lacks object sensitivity. As we demonstrate, this can cause the 
analysis to be imprecise and hence fail to certify that an application 
adheres to a user’s security requirements, even if this is in fact the 
case.

To address this problem, we have developed a format of object-sensitive 
security policies and a security property that formalizes whether an 
Android application is secure with respect to a given policy. Furthermore, 
we provide a security type system for statically certifying the security 
of applications. We have proven that the analysis is sound, i.e., that 
all certifiable applications are in fact secure. We have implemented 
our analysis in Cassandra and have experimentally evaluated it on 
example applications.

This talk presents some highlights of our results.