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