Secure Information Flow for a Sequential Java Virtual Machine

The Java platform combines static and dynamic mechanisms to enforce innocuity of applications, but these mechanisms fail to guarantee that confidential information will not leak to unauthorized principals. In order to provide stronger guarantees with respect to confidentiality, it is thus necessary to rely on alternative mechanisms, such as static analyses or type systems that enforce non-interference, a high-level security property that guarantees the absence of illicit information flows during a program execution. While Banerjee and Naumann have recently investigated the use of such type systems for the Java language, there lacks a similar study for the Java Virtual Machine (JVM), and more generally for low-level languages that have not received much attention in studies of secure information flow. In this talk, I will propose an information flow type system for a non-trivial fragment of the JVM that includes classes, methods, exceptions and subroutines, and show that it enforces non-interference. Our type system is compatible with the principles of bytecode verification, and could thus be used as the basis of an enhanced bytecode verifier.