  Android is an operating system that has been used in a majority of mobile
devices. Each application in Android runs in an instance of the Dalvik virtual
machine, which is a register-based virtual machine (VM). Most applications for
Android are developed using Java, compiled to Java bytecode and then translated
to DEX bytecode using the dx tool in the Android SDK. In this work, we aim to
develop a type-based method for certifying non-interference properties of DEX
bytecode, following a methodology that has been developed for Java bytecode
certification by Barthe et al. To this end, we develop a formal operational
semantics of the Dalvik VM, a type system for DEX bytecode, and prove the
soundness of the type system with respect to a notion of non-interference. We
then study the translation process from Java bytecode to DEX bytecode, as
implemented in the dx tool in the Android SDK. We show that an abstracted
version of the translation from Java bytecode to DEX bytecode preserves the
non-interference property. More precisely, we show that if the Java bytecode is
typable in Barthe et al's type system (which guarantees non-interference) then
its translation is typable in our type system. This result opens up the
possibility to leverage existing bytecode verifiers for Java to certify
non-interference properties of Android bytecode.
