Noninterference with dynamic security domains and policies

Language-based information flow analysis is used to statically examine a program for information flows between objects of different security domains, and to verify these flows follow a given policy. When the program is distributed as mobile code, it may access resources whose domains depend on the client environment, or may face different security policies. In proof-carrying code scenarios, it is desirable to give a single proof that the program executes securely in any of these situations. This paper presents an object-oriented, Java-like language with runtime security types that can be inspected to ensure that flows between accessed objects are actually allowed before operations inducing these flows are performed. A type system is used to statically prove that the flow tests included in the program are sufficient, such that a noninterference property for the program is ensured regardless of the domains of objects and the effective security policy. Also, the paper outlines how the concepts of the type system are transferred to a bytecode language.