Type Preserving Android Compilation

This project analyzes the (non-optimized) compilation from JVM into Android bytecode (DEX). We leverage an existing security approach to JVM bytecode and apply it to Android. In particular, we show that a JVM program that is typable w.r.t. a non-interferent type system will also yield a typable DEX bytecode. The theoretical background is contained in the extended paper, and we also provide a prototype for this whole infrastructure. Those who are interested can clone the project contained in http://github.com/H3nd24/TranslationProof