Robert Grabowski: Verification of Universal Noninterference for JVM-like Bytecode
Language-based information flow security focuses on the analysis of software to determine information flows between data resources of different security levels, and to verify that these flows follow a given policy. In mobile code scenarios, a program is typically distributed in bytecode form and executed on devices where the flow policies or security levels should be user-adjustable. Both the bytecode level and the dynamic aspect of the security environment pose a challenge for existing static analysis approaches.
To certify information flows in the presence of dynamic environments, I have developed a Java-like high-level language and a JVM-like bytecode language, which are both extended with facilities to inspect security levels and policies at runtime. This enables the creation of software that is secure for arbitrary environments. The resulting property is formalised as "universal noninterference", and statically verified by type systems for the high-level and the low-level language.
In this talk, I will give an overview of the entire verification framework, summarize the type system for the high-level language, and focus in particular on the bytecode aspects. I will illustrate the problems that arise when analysing arbitrary unstructured bytecode instructions, and show how it can nonetheless be verified by transforming the code into a stackless intermediate representation and by inserting pseudo-instructions to indicate confluence points. The analysis can be performed either directly on the mobile device, or by the code producer that distributes the type derivation as an easily verifiable certificate, following the proof-carrying code paradigm.