Fast probabilistic simulation, nontermination, and secure information flow

In secure information flow analysis, the classic Denning restrictions allow a program’s termination to be affected by the values of its H variables, resulting in potential information leaks. In an effort to quantify such leaks, in this work we study a simple imperative language with random assignments. We consider a “stripping” operation on programs and establish a fundamental relationship between the behavior of a well-typed program and of its stripped version; to prove this relationship, we introduce a new notion of fast probabilistic simulation on Markov chains. As an application, we prove that, under the Denning restrictions, well-typed probabilistic programs are guaranteed to satisfy an approximate probabilistic noninterference property, provided that their probability of nontermination is small