Deriving an information flow checker and certifying compiler for Java

Language-based security provides a means to enforce end-to-end confidentiality and integrity policies in mobile code scenarios, and is increasingly being contemplated by the smart-card and mobile phone industry as a solution to enforce information flow and resource control policies. Two threads of work have emerged in research on language-based security: work that focuses on enforcing security policies for source code, which is tailored towards developers that want to increase confidence in their applications, and work that focuses on efficiently verifying similar policies for byte-code, which is tailored to code consumers that want to protect themselves against hostile applications. These lines of work serve different purposes - and thus have been developed independently - but connecting them is a key step towards the deployment of language-based security in practical applications. This paper introduces a systematic technique to connect source code and bytecode security type systems. The technique is applied to an information flow type system for a fragment of Java with exceptions, thus confronting challenges in both control and data flow tracking