Probabilistic Noninterference in a Concurrent Language
Abstract
In, 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1998
- Accession Number
- ADA484466
Entities
People
- Dennis Volpano
- Geoffrey B. Smith
Organizations
- Naval Postgraduate School