Abstract
In previous work (Smith and Volpano, Proceedings 25th Symposium on Principles of Programming Languages, San Diego, CA, 1998, pp. 355–364), 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 (Kozen, Journal of Computer and System Sciences 22 (1981), 328–350).
This material is based upon activities supported by DARPA and by the National Science Foundation under Agreement Nos. CCR-9612176 and CCR-9612345.
Get full access to this article
View all access options for this article.