A New Type System for Secure Information Flow

Abstract: With the variables of a program classified as L (low, public) or H (high, private), we wish to prevent the program from leaking information about H variables into L variables. Given a multi-threaded imperative language with probabilistic scheduling, the goal can be formalized as a property called probabilistic noninterference. Previous work identified a type system sufficient to guarantee probabilistic noninterference, but at the cost of severe restrictions: to prevent timing leaks, H variables were disallowed from the guards of while loops. Here we present a new type system that gives each command a type of the form \tau_1 cmd \tau_2; this type says that the command assigns only to variables of level \tau_1 (or higher) and has running time that depends only on variables of level \tau_2 (or lower). Also we use types of the form \tau cmd n for commands that terminate in exactly n steps. With these typings, we can prevent timing leaks by demanding that no assignment to an L variable may sequentially follow a command whose running time depends on H variables. As a result, we can use H variables more flexibly; for example, under the new system a thread that involves only H variables is always well typed. The soundness of the type system is proved using the notion of probabilistic bisimulation.