Probabilistic noninterference through weak probabilistic bisimulation

To be practical, systems for ensuring secure information flow must be as permissive as possible. To this end, the author recently proposed a type system for multi-threaded programs running under a uniform probabilistic scheduler; it 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. But these timing variations preclude a proof of the soundness of the type system using the framework of probabilistic bisimulation, because probabilistic bisimulation is too strict regarding time. To address this difficulty, this paper proposes a notion of weak probabilistic bisimulation for Markov chains, allowing two Markov chains to be regarded as equivalent even when one "runs" more slowly that the other. The paper applies weak probabilistic bisimulation to prove that the type system guarantees the probabilistic noninterference property. Finally, the paper shows that the language can safely be extended with a fork command that allows new threads to be spawned.