Probabilistic Noninterference through Weak Probabilistic Bisimulation

13 years 8 months ago
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 than 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 ...
Geoffrey Smith
Added 04 Jul 2010
Updated 04 Jul 2010
Type Conference
Year 2003
Where CSFW
Authors Geoffrey Smith
Comments (0)