Deriving an information flow checker and certifying compiler for java

Language-based security provides a means to enforce end-to-end condentiality and integrity policies inmobile code sce-narios, and is increasingly being contemplated by the smart-card and mobile phone industry as a solution to enforce infor-mation ow and resource control policies. Two threads of work have emerged in research on language-based security: work that focuses on enforcing security poli-cies for source code, which is tailored towards developers that want to increase condence in their applications, and work that focuses on eciently verifying similar policies for byte-code, which is tailored to code consumers that want to pro-tect themselves against hostile applications. These lines of work serve dierent purposes|and thus have been developed independently|but connecting them is a key step towards the deployment of language-based security in practical applica-tions. This paper introduces a systematic technique to connect source code and bytecode security type systems. The technique is applied to an information ow type system for a fragment of Java with exceptions, thus confronting challenges in both con-trol and data ow tracking. 1