Probabilistic Noninterference in a Concurrent Language
Abstract
In previous work [16], 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 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].
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 19, 1999
- Accession Number
- ADA495086
Entities
People
- Dennis Volpano
- Geoffrey B. Smith
Organizations
- Naval Postgraduate School