Improved typings for probabilistic noninterference in a multi-threaded language

摘要

With the variables of a program classified as L (low, public) or H (high, private), the secure information flow problem is concerned with preventing the program from leaking information from H variables to L variables. In the context of a multi-threaded imperative language with probabilistic scheduling, the goal can be formalized as a probabilistic noninterference property. Previous work identified a type system sufficient to guarantee probabilistic noninterference, but at the cost of severe restrictions to prevent timing leaks - for example, H variables were forbidden in the guards of while loops. Here we present a more permissive type system that allows the running times of threads to depend on the values of H variables, provided that these timing variations cannot affect the values of L variables. The type system gives each command a type of the form τ_1 cmd τ_2; this type says that the command assigns only to variables of level τ_1 (or higher) and has running time that depends only on variables of level τ_2 (or lower). Also it uses types of the form τ cmd n for commands that terminate in exactly n steps. With these typings, timing leaks can be prevented by demanding that no assignment to an L variable may sequentially follow a command whose running time depends on H variables. We prove that well-typed multi-threaded programs satisfy a property that we call weak probabilistic noninterference; it is based on a notion of weak probabilistic bisimulation for Markov chains, allowing two Markov chains to be regarded as equivalent even when one "runs" more slowly than the other. Finally, we show that the language can safely be extended with a fork command that allows new threads to be spawned.