Run-Time Enforcement of Information-Flow Properties on Android (CMU-CyLab-12-015)

Recent years have seen a dramatic increase in the number and importance in daily life of smartphones and similar mobile devices. The security properties that these devices provide to their applications, however, are inadequate to protect against many undesired behaviors. A broad class of such behaviors is violations of simple information-flow properties.

This paper proposes an enforcement system that permits Android applications to be concisely annotated with information-flow policies, which the system enforces at run time. Information-flow constraints are enforced both between applications and between components within applications, aiding developers in implementing least privilege. We develop a detailed model of our enforcement system using a process calculus, and use the model to prove noninterference. Our system and model have a number of useful or novel features, including support for Android’s single- and multiple-instance components, floating labels, declassification and endorsement capabilities, and support for legacy applications. Our system design fits the Android programming model and runtime cleanly enough that we have developed a fully functional prototype on Android 4.0.4. We have tested our prototype on a Nexus S phone, verifying that it can enforce practically useful policies that can be implemented with minimal modification to off-the-shelf applications.