Non-termination 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 paper we study a simple imperative language with random assignments. As a thought experiment, we propose a 'stripping' operation on programs, which eliminates all 'high computation', and prove the fundamental property that stripping cannot decrease the probability of any low outcome. To prove this property, we first introduce a new notion of fast probabilistic simulation on Markov chains and show that it implies a key reachability property. Viewing the stripping function as a binary relation, we then prove that stripping is a fast simulation. As an application, we prove that, under the Denning restrictions, well-typed probabilistic programs are guaranteed to satisfy an approximate probabilistic non-interference property, provided that their probability of non-termination is small.