Probabilistic Noninterference in a Concurrent Language

Abstract

In (15) we give a type system that guarantees that well typed multi threaded programs are possibilistically noninterfering If thread scheduling is probabilistic , however, then well typed programs may have probabilistic timing channels We describe how they can be eliminated without making the type system more restrictive We show that well typed concurrent programs are probabilistically noninterfering if every total command with a high guard executes atomically The proof uses the concept of a probabilistic state of a computation following the work of Kozen [10]1.