Language-based information flow control (IFC) aims to provide guarantees about information propagation in computer systems having multiple security levels. Existing IFC systems extend the lattice model of Denning’s, enforcing transitive security policies by tracking information flows along with a partially ordered set of security levels. They yield a transitive noninterference property of either confidentiality or integrity. In this paper, we explore IFC for security policies that are not necessarily transitive. Such nontransitive security policies avoid unwanted or unexpected information flows implied by transitive policies and naturally accommodate high-level coarse-grained security requirements in modern component-based software. We present a novel security type system for enforcing nontransitive security policies. Unlike traditional security type systems that verify information propagation by subtyping security levels of a transitive policy, our type system relaxes strong transitivity by inferring information flow history through security levels and ensuring that they respect the nontransitive policy in effect. Such a type system yields a new nontransitive noninterference property that offers more flexible information flow relations induced by security policies that do not have to be transitive, therefore generalizing the conventional transitive noninterference. This enables us to directly reason about the extent of information flows in the program and restrict interactions between security-sensitive and untrusted components.

We describe our preliminary experience in the design and implementation of a points-to analysis for Java, called EMU, that enables developers to perform pointer-related queries in programs undergoing constant changes in IDEs. EMU achieves fast response times by adopting a modular approach to incrementally updating method summaries upon small code changes: the points-to information in a method is summarised indirectly by CFL reachability rather than directly by points-to sets. Thus, the impact of a small code change made in a method is localised, requiring only its affected part to be re-summarised just to reflect the change. EMU achieves precision by being context-sensitive (for both method invocation and heap abstraction) and field-sensitive. Our evaluation shows that EMU can be promisingly deployed in IDEs where the changes are small.

Representation exposure is a well-known problem in the object-oriented realm. Object encapsulation mechanisms have established a tradition for solving this problem based on a principle of reference containment. This paper proposes a novel type system which is based on a different principle, we call effect encapsulation, which confines side effects, rather than object references, according to an ownership structure. Compared to object encapsulation, effect encapsulation liberates us from the restriction on object referenceability and offers more flexibility. In this paper, we show that effect encapsulation can be statically type checked.