Probabilistic Noninterference in a Concurrent Language

In previous work [16], we give a type system that guarantees that well-typed multithreaded 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 guard containing high variables executes atomically. The proof uses the notion of a probabilistic state of a computation from Kozen's work in the denotational semantics of probabilistic programs [11].1

• Type: Conference
• Year: 1998
• Where: CSFW
• Authors: Dennis M. Volpano, Geoffrey Smith
• Keywords: CSFW 1998, Probabilistic Timing Channels, Security Privacy, Well-typed Concurrent Programs, Well-typed Multithreaded Programs