Language-based security on Android

In this paper, we initiate a formal study of security on Android: Google’s new open-source platform for mobile devices. Specifically, we present a core typed language to describe Android applications, and to reason about their dataflow security properties. Our operational semantics and type system provide some necessary foundations to help both users and developers of Android applications deal with their security concerns. Categories and Subject Descriptors D.4.6 [Operating Systems]: Security and Protection—Access controls, Verification; D.3.3 [Programming Languages]: Language Constructs and Features—Control constructs General Terms Security, Languages, Verification Keywords data-flow security, hybrid type system, mobile code, certified compilation

• Type: Conference
• Year: 2009
• Where: PLDI
• Authors: Avik Chaudhuri
• Keywords: Android Applications, Dataflow Security Properties, PLDI 2009, Programming Languages, Security