Information flow inference for free

Abstract

This paper shows how to systematically extend an arbitrary type system with dependency information, and how soundness and non-interference proofs for the new system may rely upon, rather than duplicate, the soundness proof of the original system. This allows enriching virtually any of the type systems known today with information flow analysis, while requiring only a minimal proof effort. Our approach is based on an untyped operational semantics for a labelled calculus akin to core ML. Thus, it is simple, and should be applicable to other computing paradigms, such as object or process calculi. The paper also discusses access control, and shows it may be viewed as entirely independent of information flow control. Letting the two mechanisms coexist, without interacting, yields a simple and expressive type system, which allows, in particular, `selective' declassification.