You are here

Run-Time Enforcement Of Information-Flow Properties On Android


Speaker Info:

Limin Jia
Assistant Research Professor
Carnegie-Mellon University


I will talk about improving Android's permission system to prevent confused-deputy attacks and information leakage. Android's system permits Android applications to be concisely annotated with information-flow policies by either the programmers or security analysts. 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. 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.

Speaker Bio:

Limin Jia is an Assistant Research Professor in ECE and INI. She received her B.E. in Computer Science and Engineering from the University of Science and Technology of China and her Ph.D. in Computer Science from Princeton University. Her research interests include language-based security, programming languages, logic, and program verification. Dr. Jia's research focuses on formal aspects of security. She is particularly interested in applying language-based security techniques as well as formal logic to model and verify security properties of software systems.