Towards Precise Treatment of Inter-Procedural Implicit
Information Flow in Android Applications


Cassandra is a Security-Certifying App Store for Android and
aims to provide a way for users to verify whether an Android
app leaks private data. So far, Cassandra does not certify
the security of apps that contain method calls in a high
security environment, i.e., at program points whose execution
depends on a secret. This is due to the possibility of the
called method having an observable side-effect on the heap
and thus creating an implicit information flow. As a result of
this restrictive approach, the security of apps containing a
method call in a high security environment cannot be certified,
even if those apps do not leak private data.

To improve the precision of Cassandra in this regard we
annotate a method with whether an attacker can observe the
effects of executing the method. We adapt the security type
system and type inference of Cassandra in a manner that uses
this annotation to decide whether a method call can leak
information. We modify the architecture of Cassandra to allow
denoting the effects of a method call in a format that depends
on the analysis module in use, and implement our new security
analysis as an additional analysis module. We argue for the
faithfulness of our definitions and evaluate our implementation
using Dalvik bytecode test programs.