View article

We aim to develop a proof-carrying code (PCC) framework to certify compliance of an Android application with a given information flow policy, specified via certain non-interference properties. In the PCC framework, a certified application comes with a statement of an information flow policy and a proof that its execution complies with the given policy. We follow a type-based approach for enforcing non-interference, in which typeable programs are guaranteed to be non-interferrent and typing derivations serve as certificates of non-interference. Our eventual goal is to produce a compiler tool chain that can help developers to develop Android applications that complies with a given policy, and automate the process of generating the final non-interference certificates for Dalvik bytecode. Android apps are typically developed in Java, and go through two stages of compilation. The first one compiles the Java code into JVM bytecode, and the second one compiles the JVM bytecode into the final Android Dalvik bytecode. Non-interference type systems exist for all three languages (Java, JVM and Dalvik), and Barth et. al. have shown that typeability is preserved going from Java source to JVM. To complete the picture, we show here that the compilation from JVM to Dalvik, as implemented in the official Android dx tool, preserves typeability. We then show how such a type-based certification scheme can be implemented, and give details of the certificate encodings in Android apps.