Noninterference with Dynamic Security Domains and Policies

Abstract. 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 h...

• Type: Journal
• Year: 2009
• Where: ASIAN
• Authors: Robert Grabowski, Lennart Beringer
• Keywords: Algorithms, ASIAN 2009, Language-based Information Flow, Proof-carrying Code Scenarios, Runtime Security Types