Language-based security provides a means to enforce endto- end confidentiality and integrity policies inmobile code scenarios, and is increasingly being contemplated by the smartcard and mobile phone industry as a solution to enforce information flow and resource control policies.

Two threads of work have emerged in research on languagebased 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 bytecode, 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.