Noninterference for Dynamic Security Environments
Robert Grabowski and Lennart Beringer (Princeton University)

Noninterference specifies that a program transfers data between
objects of different confidentiality levels in manner that respects a
given information flow policy. A technique to statically analyse
programs with respect to this property are type systems. However, few
existing analyses consider mobile code executed in varying security
environments where the confidentiality levels and flow policies are
only known at runtime.

In this talk, we present a suitable generalisation of noninterference
for Java/JVM-style mobile code. Dynamic policy dependency is supported
by a language construct to query the security levels and policies at
runtime and to guard operations that induce potentially insecure
information flows. We present type systems for Java and bytecode that
provide guarantees that programs execute securely in any
environment. We also outline a type-preserving compilation that
produces a certificate of dynamic noninterference, making the approach
suitable for proof carrying code scenarios.