Probabilistic Noninterference in a Concurrent Language
NAVAL POSTGRADUATE SCHOOL MONTEREY CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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 Kozens work in the denotational semantics of probabilistic programs 11.
- Computer Programming and Software
- Computer Systems Management and Standards